for X being non trivial set
for x being Element of X ex y being object st
( y in X & x <> y )