theorem :: TOPS_5:6

for X being non empty set
for x, y being object st X --> x = X --> y holds
x = y