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