let D be set ; :: thesis: for A being Subset of D holds
( not A is trivial iff ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 ) )
let A be Subset of D; :: thesis: ( not A is trivial iff ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 ) )

hereby :: thesis: ( ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 ) implies not A is trivial )

assume not A is trivial ; :: thesis: ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 )
then consider d1, d2 being set such that
A1: ( d1 in A & d2 in A ) and
A2: d1 <> d2 by Th14;
reconsider d1 = d1, d2 = d2 as Element of D by A1;
take d1 = d1; :: thesis: ex d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 )
take d2 = d2; :: thesis: ( d1 in A & d2 in A & d1 <> d2 )
thus ( d1 in A & d2 in A & d1 <> d2 ) by A1, A2; :: thesis: verum

end;

thus ( ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 ) implies not A is trivial ) by Th14; :: thesis: verum