theorem :: RELAT_1:83

for X being set
for P, R being Relation holds (P * R) | X = (P | X) * R