theorem :: SUBSET_1:50

for X being non trivial set
for p being set ex q being Element of X st q <> p