theorem :: RELAT_1:115

for X being set
for R being Relation holds rng (R | X) = R .: X