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