theorem Th11: :: RELAT_1:17

for x, y being object holds field {[x,y]} = {x,y}