theorem :: RELSET_1:21

for X, Y, Y1 being set
for R being Relation of X,Y st Y c= Y1 holds
Y1 |` R = R