theorem :: MCART_1:90

for R being non empty Relation
for x, y being Element of R st x `1 = y `1 & x `2 = y `2 holds
x = y by Th73;