theorem :: RELAT_1:97

for Y being set
for R being Relation holds Y |` (Y |` R) = Y |` R ;