let P, R, Q be Relation; :: thesis: P * (R /\ Q) c= (P * R) /\ (P * Q)
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b being set st [x,b] in P * (R /\ Q) holds
[x,b] in (P * R) /\ (P * Q)
let y be set ; :: thesis: ( [x,y] in P * (R /\ Q) implies [x,y] in (P * R) /\ (P * Q) )
assume [x,y] in P * (R /\ Q) ; :: thesis: [x,y] in (P * R) /\ (P * Q)
then consider z being set such that
A1: [x,z] in P and
A2: [z,y] in R /\ Q by Def8;
[z,y] in Q by A2, XBOOLE_0:def 4;
then A3: [x,y] in P * Q by A1, Def8;
[z,y] in R by A2, XBOOLE_0:def 4;
then [x,y] in P * R by A1, Def8;
hence [x,y] in (P * R) /\ (P * Q) by A3, XBOOLE_0:def 4; :: thesis: verum