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