theorem Th9: :: HILBERT3:10

for a, b, x, y, x9, y9 being set st a <> b & (a,b) --> (x,y) = (a,b) --> (x9,y9) holds
( x = x9 & y = y9 )