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