theorem Th3: :: RELAT_1:9

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