let D be set ; :: thesis: for A being Subset of D st not A is trivial holds
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 implies ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 ) )
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 object such that
A1: ( d1 in A & d2 in A ) and
A2: d1 <> d2 ;
reconsider d1 = d1, d2 = d2 as set by TARSKI:1;
( d1 in D & d2 in D ) by A1, Lm1;
then reconsider d1 = d1, d2 = d2 as Element of D by Def1;
take d1 ; :: thesis: ex d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 )
take d2 ; :: thesis: ( d1 in A & d2 in A & d1 <> d2 )
thus ( d1 in A & d2 in A & d1 <> d2 ) by A1, A2; :: thesis: verum