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 P & [x,y] in R ) by A1, XBOOLE_0:def 4;
then ( y in rng P & y in rng R ) by Def5;
hence y in (rng P) /\ (rng R) by XBOOLE_0:def 4; :: thesis: verum