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