theorem Th4: :: SCMYCIEL:4

for x1, y1, x2, y2 being object
for X being set st x1 in X & x2 in X & {x1,[y1,X]} = {x2,[y2,X]} holds
( x1 = x2 & y1 = y2 )