theorem :: SUBSET_1:45

for D being set
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 )