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