let P, R be Relation; :: thesis: (P /\ R) ~ = (P ~) /\ (R ~)
let x be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in (P /\ R) ~ iff [x,b] in (P ~) /\ (R ~) )
let y be object ; :: thesis: ( [x,y] in (P /\ R) ~ iff [x,y] in (P ~) /\ (R ~) )
( [x,y] in (P /\ R) ~ iff [y,x] in P /\ R ) by Def5;
then ( [x,y] in (P /\ R) ~ iff ( [y,x] in P & [y,x] in R ) ) by XBOOLE_0:def 4;
then ( [x,y] in (P /\ R) ~ iff ( [x,y] in P ~ & [x,y] in R ~ ) ) by Def5;
hence ( [x,y] in (P /\ R) ~ iff [x,y] in (P ~) /\ (R ~) ) by XBOOLE_0:def 4; :: thesis: verum