theorem :: TEX_2:4

for S being non trivial set
for y being Element of S holds {y} is proper ;