theorem :: RELSET_1:6

for X, Y, Y1 being set
for R being Relation of X,Y st rng R c= Y1 holds
R is Relation of X,Y1