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