let P, Q, R be Relation; :: thesis: P * (R /\ Q) c= (P * R) /\ (P * Q)
let x be object ; :: according to RELAT_1:def 3 :: thesis: for b being object st [x,b] in P * (R /\ Q) holds
[x,b] in (P * R) /\ (P * Q)
let y be object ; :: 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 object such that
A1: [x,z] in P and
A2: [z,y] in R /\ Q by Def6;
[z,y] in Q by A2, XBOOLE_0:def 4;
then A3: [x,y] in P * Q by A1, Def6;
[z,y] in R by A2, XBOOLE_0:def 4;
then [x,y] in P * R by A1, Def6;
hence [x,y] in (P * R) /\ (P * Q) by A3, XBOOLE_0:def 4; :: thesis: verum