theorem :: RELAT_1:133

for Y being set
for R being Relation holds R " Y = R " ((rng R) /\ Y)