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 and
A2: dom f = 2 and
A3: 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 )
A4: 0 in dom f by A2, CARD_1:88, TARSKI:def 2;
then f . 0 in rng f by FUNCT_1:def 5;
hence x in X by A3; :: thesis: ( y in X & x <> y )
A5: 1 in dom f by A2, CARD_1:88, TARSKI:def 2;
then f . 1 in rng f by FUNCT_1:def 5;
hence y in X by A3; :: thesis: x <> y
thus x <> y by A1, A4, A5, FUNCT_1:def 8; :: thesis: verum

end;

given x, y being set such that A6: ( x in X & y in X ) and
A7: 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 A6, TARSKI:def 2; :: thesis: verum

end;

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