let P, R, Q be Relation; :: thesis: ( P c= R implies Q * P c= Q * R )
assume A1: P c= R ; :: thesis: Q * P c= Q * R
for x, y being set st [x,y] in Q * P holds
[x,y] in Q * R

proof

let x, y be set ; :: 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 consider z being set such that
A2: ( [x,z] in Q & [z,y] in P ) by Def8;
thus [x,y] in Q * R by A1, A2, Def8; :: thesis: verum

end;

hence Q * P c= Q * R by Def3; :: thesis: verum