theorem :: RELAT_1:73
for X, Y being set
for R being Relation st X c= Y holds
(R | X) | Y = R | X