let X be set ; :: thesis: ( 2 c= card X iff not X is trivial )
consider z being 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 set such that
A1: x in X and
A2: y in X and
A3: x <> y by Th2;

now

given z being set 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, REALSET1:def 4; :: thesis: verum

end;

assume A5: not X is trivial ; :: thesis: 2 c= card X
then {z} c= X by ZFMISC_1:37;
then ( X c= {z} implies X = {z} ) by XBOOLE_0:def 10;
then consider w being set such that
A6: w in X and
A7: not w in {z} by A5, TARSKI:def 3;
w <> z by A7, TARSKI:def 1;
hence 2 c= card X by A6, Th2; :: thesis: verum