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