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