theorem :: RELSET_1:5

for X, X1, Y being set
for R being Relation of X,Y st dom R c= X1 holds
R is Relation of X1,Y