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 A2: ( y in rng P & not y in rng R ) by XBOOLE_0:def 5;
consider x being set such that
A3: [x,y] in P by A1, Def5;
not [x,y] in R by A2, Def5;
then [x,y] in P \ R by A3, XBOOLE_0:def 5;
hence y in rng (P \ R) by Def5; :: thesis: verum