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