theorem :: RELAT_1:188

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