theorem :: RELAT_1:91

for Y being set
for P, R being Relation holds P * (Y |` R) c= P * R by Th23, Th80;