let X be set ; ( 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 ( 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
;
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;
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;
( 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;
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 )
; 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; verum