English
Let s be a finite set. Then |s| = 2 if and only if there exist distinct x and y with s = {x, y}.
Русский
Пусть s — конечное множество. Тогда |s| = 2 эквивалентно существованию попарно различных x и y таких, что s = {x, y}.
LaTeX
$$$|s| = 2 \\iff \\exists x \\exists y\\,(x \\neq y) \\land s = \\{ x, y \\}$$$
Lean4
theorem card_eq_two : #s = 2 ↔ ∃ x y, x ≠ y ∧ s = { x, y } :=
by
constructor
· rw [card_eq_succ]
grind [card_eq_one]
· grind