let X be set ; :: thesis: ( 2 c= card X implies for x being object ex y being object st
( y in X & x <> y ) )
assume 2 c= card X ; :: thesis: for x being object ex y being object st
( y in X & x <> y )
then consider a, b being object such that
A1: a in X and
A2: ( b in X & a <> b ) by Th2;
let x be object ; :: thesis: ex y being object st
( y in X & x <> y )
per cases ( x = a or x <> a ) ;
suppose A3: x = a ; :: thesis: ex y being object 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 object 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;