theorem :: PREFER_1:5

for A being non trivial set ex a, b being Element of A st a <> b