theorem :: RELAT_1:74

for X, Y being set
for R being Relation st Y c= X holds
(R | X) | Y = R | Y