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 ;
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 ; :: 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 ; :: thesis: verum