let P, R, Q, 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

now

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

end;

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