theorem Th3: :: SYSREL:3

for X, Y being set
for R being Relation st R c= [:X,Y:] holds
( dom R c= X & rng R c= Y )