theorem :: RELAT_1:89

for Y being set
for R being Relation st Y c= rng R holds
rng (Y |` R) = Y