theorem :: SETWISEO:56

for X being non empty set
for x, y, z being Element of X st x in (singleton X) . z & y in (singleton X) . z holds
x = y