let P, Q, R be Relation; :: thesis: (P /\ Q) * R c= (P * R) /\ (Q * R)
let x, y be object ; :: 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 object such that
A1: [x,z] in P /\ Q and
A2: [z,y] in R by RELAT_1:def 8;
A3: [x,z] in P by A1, XBOOLE_0:def 4;
A4: [x,z] in Q by A1, XBOOLE_0:def 4;
A5: [x,y] in P * R by A2, A3, RELAT_1:def 8;
[x,y] in Q * R by A2, A4, RELAT_1:def 8;
hence [x,y] in (P * R) /\ (Q * R) by A5, XBOOLE_0:def 4; :: thesis: verum