theorem :: RELAT_1:87

for Y being set
for R being Relation holds rng (Y |` R) c= rng R by Th80, XTUPLE_0:9;