for X being non empty set
for x being set
for y being Element of X holds
( x in (singleton X) . y iff x = y )