theorem :: RELAT_1:10

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