let P, Q, R be Relation; :: thesis: (P /\ Q) * R c= (P * R) /\ (Q * R)
let x, y be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in (P /\ Q) * R or [x,y] in (P * R) /\ (Q * R) )
assume [x,y] in (P /\ Q) * R ; :: thesis: [x,y] in (P * R) /\ (Q * R)
then consider z being set such that
A1: ( [x,z] in P /\ Q & [z,y] in R ) by RELAT_1:def 8;
A2: ( [x,z] in P & [x,z] in Q ) by A1, XBOOLE_0:def 4;
then A3: [x,y] in P * R by A1, RELAT_1:def 8;
[x,y] in Q * R by A1, A2, RELAT_1:def 8;
hence [x,y] in (P * R) /\ (Q * R) by A3, XBOOLE_0:def 4; :: thesis: verum