theorem :: RELAT_1:64

for X being set
for P, R being Relation holds P * (R | X) c= P * R by Th23, Th53;