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 Th69, Th70;
hence P | X c= R | Y ; :: thesis: verum