theorem :: RELAT_1:85

for Y being set
for R being Relation holds rng (Y |` R) c= Y by Th78;