let X be set ; :: thesis: ( 2 c= card X iff ex x, y being set st
( x in X & y in X & x <> y ) )
thus ( 2 c= card X implies ex x, y being set st
( x in X & y in X & x <> y ) ) :: thesis: ( ex x, y being set st
( x in X & y in X & x <> y ) implies 2 c= card X )

proof

assume 2 c= card X ; :: thesis: ex x, y being set st
( x in X & y in X & x <> y )
then card 2 c= card X by CARD_1:def 5;
then consider f being Function such that
A1: ( f is one-to-one & dom f = 2 & rng f c= X ) by CARD_1:26;
take x = f . 0 ; :: thesis: ex y being set st
( x in X & y in X & x <> y )
take y = f . 1; :: thesis: ( x in X & y in X & x <> y )
A2: ( 0 in dom f & 1 in dom f ) by A1, CARD_1:88, TARSKI:def 2;
then f . 0 in rng f by FUNCT_1:def 5;
hence x in X by A1; :: thesis: ( y in X & x <> y )
f . 1 in rng f by A2, FUNCT_1:def 5;
hence y in X by A1; :: thesis: x <> y
thus x <> y by A1, A2, FUNCT_1:def 8; :: thesis: verum

end;

given x, y being set such that A3: ( x in X & y in X & x <> y ) ; :: thesis: 2 c= card X
{x,y} c= X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {x,y} or a in X )
assume a in {x,y} ; :: thesis: a in X
hence a in X by A3, TARSKI:def 2; :: thesis: verum

end;

then card {x,y} c= card X by CARD_1:27;
hence 2 c= card X by A3, CARD_2:76; :: thesis: verum