let X, Y be set ; :: thesis: for R being Relation st Y c= X holds
(R | X) | Y = R | Y
let R be Relation; :: thesis: ( Y c= X implies (R | X) | Y = R | Y )
( Y c= X implies X /\ Y = Y ) by XBOOLE_1:28;
hence ( Y c= X implies (R | X) | Y = R | Y ) by Th65; :: thesis: verum