1ページちょっと使っているのは、

(a, b) = (c, d) ⇔ a = c ∧ b = d

のほうでした。

なぜ、順序対を

(a, b) := {{a}, {a, b}}

と定義すると厳密になるのでしょうか？