theorem Th73: :: MCART_1:89

for y being object
for R being Relation
for x being object st x in R & y in R & x `1 = y `1 & x `2 = y `2 holds
x = y