for Y being non empty 1-sorted
for y being Element of Y st {y} is proper holds
not Y is trivial ;