theorem Th3: :: RELAT_1:9

for x, y being object holds
( dom {[x,y]} = {x} & rng {[x,y]} = {y} )