let P, R be Relation; :: thesis: ( P c= R implies ( dom P c= dom R & rng P c= rng R ) )
assume A1: P c= R ; :: thesis: ( dom P c= dom R & rng P c= rng R )
thus dom P c= dom R :: thesis: rng P c= rng R

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom P or x in dom R )
assume x in dom P ; :: thesis: x in dom R
then consider y being set such that
A2: [x,y] in P by Def4;
thus x in dom R by A1, A2, Def4; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng P or y in rng R )
assume y in rng P ; :: thesis: y in rng R
then consider x being set such that
A3: [x,y] in P by Def5;
thus y in rng R by A1, A3, Def5; :: thesis: verum