let X be set ; :: thesis: ( 2 c= card X iff not X is trivial )
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 & y in X & x <> y ) by Th2;

now

given z being set such that A2: X = {z} ; :: thesis: x = y
thus x = z by A1, A2, TARSKI:def 1
.= y by A1, A2, TARSKI:def 1 ; :: thesis: verum

end;

hence not X is trivial by A1, REALSET1:def 4; :: thesis: verum

end;

assume A3: not X is trivial ; :: thesis: 2 c= card X
then A4: ( not X is empty & ( for z being set holds X <> {z} ) ) ;
consider z being Element of X;
{z} c= X by A4, ZFMISC_1:37;
then ( X c= {z} implies X = {z} ) by XBOOLE_0:def 10;
then consider w being set such that
A5: ( w in X & not w in {z} ) by A3, TARSKI:def 3;
( w in X & w <> z ) by A5, TARSKI:def 1;
hence 2 c= card X by Th2; :: thesis: verum