let X be set ; :: thesis: ( 2 c= card X implies for x being set ex y being set st
( y in X & x <> y ) )
assume 2 c= card X ; :: thesis: for x being set ex y being set st
( y in X & x <> y )
then consider a, b being set such that
A1: a in X and
A2: ( b in X & a <> b ) by Th2;
let x be set ; :: thesis: ex y being set st
( y in X & x <> y )

per cases ( x = a or x <> a ) ;

suppose A3: x = a ; :: thesis: ex y being set st
( y in X & x <> y )

take b ; :: thesis: ( b in X & x <> b )
thus ( b in X & x <> b ) by A2, A3; :: thesis: verum

end;

suppose A4: x <> a ; :: thesis: ex y being set st
( y in X & x <> y )

take a ; :: thesis: ( a in X & x <> a )
thus ( a in X & x <> a ) by A1, A4; :: thesis: verum

end;

end;