let X be set ; :: thesis: ( card X = 2 iff ex x, y being set st
( x in X & y in X & x <> y & ( for z being set holds
( not z in X or z = x or z = y ) ) ) )

hereby :: thesis: ( ex x, y being set st
( x in X & y in X & x <> y & ( for z being set holds
( not z in X or z = x or z = y ) ) ) implies card X = 2 )

assume A1: card X = 2 ; :: thesis: ex x, y being set st
( x in X & y in X & x <> y & ( for z being set holds
( not z in X or z = x or z = y ) ) )
then reconsider X9 = X as finite set ;
consider x, y being object such that
A2: x <> y and
A3: X9 = {x,y} by A1, CARD_2:60;
reconsider x = x, y = y as set by TARSKI:1;
take x = x; :: thesis: ex y being set st
( x in X & y in X & x <> y & ( for z being set holds
( not z in X or z = x or z = y ) ) )
take y = y; :: thesis: ( x in X & y in X & x <> y & ( for z being set holds
( not z in X or z = x or z = y ) ) )
thus ( x in X & y in X & x <> y & ( for z being set holds
( not z in X or z = x or z = y ) ) ) by A2, A3, TARSKI:def 2; :: thesis: verum

end;

given x, y being set such that A4: x in X and
A5: y in X and
A6: x <> y and
A7: for z being set holds
( not z in X or z = x or z = y ) ; :: thesis: card X = 2
for z being object holds
( z in X iff ( z = x or z = y ) ) by A4, A5, A7;
then X = {x,y} by TARSKI:def 2;
hence card X = 2 by A6, CARD_2:57; :: thesis: verum