for x being object
for X, Y being set st x in X & X,Y are_equipotent holds
( Y <> {} & ex x being object st x in Y )