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