let X be set ; :: thesis: ( 2 c= card X iff ex x, y being object st
( x in X & y in X & x <> y ) )
thus ( 2 c= card X implies ex x, y being object st
( x in X & y in X & x <> y ) ) :: thesis: ( ex x, y being object 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 object st
( x in X & y in X & x <> y )
then card 2 c= card X ;
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:10;
take x = f . 0; :: thesis: ex y being object 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:50, TARSKI:def 2;
then f . 0 in rng f by FUNCT_1:def 3;
hence x in X by A3; :: thesis: ( y in X & x <> y )
A5: 1 in dom f by A2, CARD_1:50, TARSKI:def 2;
then f . 1 in rng f by FUNCT_1:def 3;
hence y in X by A3; :: thesis: x <> y
thus x <> y by A1, A4, A5, FUNCT_1:def 4; :: thesis: verum

end;

given x, y being object such that A6: ( x in X & y in X ) and
A7: x <> y ; :: thesis: 2 c= card X
{x,y} c= X by A6, TARSKI:def 2;
then card {x,y} c= card X by CARD_1:11;
hence 2 c= card X by A7, CARD_2:57; :: thesis: verum