let A be set ; :: thesis: ( not A is trivial iff ex a1, a2 being set st
( a1 in A & a2 in A & a1 <> a2 ) )

hereby :: thesis: ( ex a1, a2 being set st
( a1 in A & a2 in A & a1 <> a2 ) implies not A is trivial )

assume A1: not A is trivial ; :: thesis: ex a1, a2 being set st
( a1 in A & a2 in A & a1 <> a2 )
then consider a1 being set such that
A2: a1 in A by XBOOLE_0:def 1;
A <> {a1} by A1;
then consider a2 being set such that
A3: a2 in A and
A4: a1 <> a2 by A2, ZFMISC_1:41;
take a1 = a1; :: thesis: ex a2 being set st
( a1 in A & a2 in A & a1 <> a2 )
take a2 = a2; :: thesis: ( a1 in A & a2 in A & a1 <> a2 )
thus ( a1 in A & a2 in A & a1 <> a2 ) by A2, A3, A4; :: thesis: verum

end;

given a1, a2 being set such that A5: ( a1 in A & a2 in A ) and
A6: a1 <> a2 ; :: thesis: not A is trivial
thus not A is empty by A5; :: according to REALSET1:def 4 :: thesis: for x being set holds not A = {x}
given x being set such that A7: A = {x} ; :: thesis: contradiction
{a1,a2} c= {x} by A5, A7, ZFMISC_1:38;
then ( a1 = x & a2 = x ) by ZFMISC_1:26;
hence contradiction by A6; :: thesis: verum