theorem :: RELAT_1:95

for R being Relation holds (rng R) |` R = R ;