let A be 2 -element set ; for a, b being Element of A st a <> b holds
A = {a,b}
let a, b be Element of A; ( a <> b implies A = {a,b} )
assume A0:
a <> b
; A = {a,b}
card A = 2
by CARD_1:def 7;
then consider c, d being object such that
A1:
( c <> d & A = {c,d} )
by CARD_2:60;
( a = c or a = d )
by TARSKI:def 2, A1;
hence
A = {a,b}
by A0, TARSKI:def 2, A1; verum