True ↔ ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (a t : ℕ), IsGreatest {k | ∃ A ⊆ G.edgeFinset, A.card = k ∧ ∀ (x y z : Fin n), G.Adj x y → G.Adj y z → G.Adj x z → ({s(x, y), s(y, z), s(x, z)} ∩ A).card ≤ 1} a → IsLeast {k | ∃ T ⊆ G.edgeFinset, T.card = k ∧ ∀ (x y z : Fin n), G.Adj x y → G.Adj y z → G.Adj x z → (T ∩ {s(x, y), s(y, z), s(x, z)}).Nonempty} t → 4 * (a + t) ≤ n ^ 2