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