English
There exist a, b, c in s with a, b, c pairwise distinct.
Русский
Существуют элементы a, b, c в s такие, что они попарно различны.
LaTeX
$$$2 < |s| \\iff \\exists a \\in s, \\exists b \\in s, \\exists c \\in s\\, (a \\neq b) \\land (a \\neq c) \\land (b \\neq c)$$$
Lean4
theorem two_lt_card_iff : 2 < #s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c := by
classical
simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_three, ← exists_and_left,
exists_comm (α := Finset α)]
constructor
· rintro ⟨a, b, c, t, hsub, hab, hac, hbc, rfl⟩
exact ⟨a, b, c, by simp_all [insert_subset_iff]⟩
· rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩
exact ⟨a, b, c, { a, b, c }, by simp_all [insert_subset_iff]⟩
