let P, Q, R be Relation; :: thesis: ( P c= R implies Q * P c= Q * R )
assume A1: P c= R ; :: thesis: Q * P c= Q * R
let x be object ; :: according to RELAT_1:def 3 :: thesis: for b being object st [x,b] in Q * P holds
[x,b] in Q * R
let y be object ; :: thesis: ( [x,y] in Q * P implies [x,y] in Q * R )
assume [x,y] in Q * P ; :: thesis: [x,y] in Q * R
then ex z being object st
( [x,z] in Q & [z,y] in P ) by Def6;
hence [x,y] in Q * R by A1, Def6; :: thesis: verum