theorem :: RELAT_1:72

for X being set
for R being Relation holds (R | X) | X = R | X ;