let X be set ; :: thesis: ( 2 c= card X iff not X is trivial )
set z = the Element of X;
thus ( 2 c= card X implies not X is trivial ) :: thesis: ( not X is trivial implies 2 c= card X )
proof
assume 2 c= card X ; :: thesis: not X is trivial
then consider x, y being object such that
A1: x in X and
A2: y in X and
A3: x <> y by Th2;
now :: thesis: ( ex z being object st X = {z} implies x = y )
given z being object such that A4: X = {z} ; :: thesis: x = y
thus x = z by A1, A4, TARSKI:def 1
.= y by A2, A4, TARSKI:def 1 ; :: thesis: verum
end;
hence not X is trivial by A1, A3, ZFMISC_1:131; :: thesis: verum
end;
assume A5: not X is trivial ; :: thesis: 2 c= card X
then ( X c= { the Element of X} implies X = { the Element of X} ) ;
then consider w being object such that
A6: w in X and
A7: not w in { the Element of X} by A5;
w <> the Element of X by A7, TARSKI:def 1;
hence 2 c= card X by A6, Th2; :: thesis: verum