theorem :: RELAT_1:63

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