theorem Th88: :: RELAT_1:94

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