let X, Y be set ; :: thesis: for P, R being Relation st P c= R & X c= Y holds
P | X c= R | Y
let P, R be Relation; :: thesis: ( P c= R & X c= Y implies P | X c= R | Y )
assume ( P c= R & X c= Y ) ; :: thesis: P | X c= R | Y
then ( P | X c= R | X & R | X c= R | Y ) by Th104, Th105;
hence P | X c= R | Y by XBOOLE_1:1; :: thesis: verum