theorem Th15: :: MCART_1:21

for x being object
for R being Relation st x in R holds
x = [(x `1),(x `2)]