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 ) ) ) )

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

( 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 )

given x, y being set such that A4:
x in X
and ( 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;( 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

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