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 ex y being set st [x,y] in P by Def4;
hence x in dom R by A1, 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 ex x being set st [x,y] in P by Def5;
hence y in rng R by A1, Def5; :: thesis: verum