let X, Y be set ; :: thesis: for R being Relation of X,Y holds
( dom R c= X & rng R c= Y )
let R be Relation of X,Y; :: thesis: ( dom R c= X & rng R c= Y )
thus dom R c= X :: thesis: rng R c= Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom R or x in X )
assume x in dom R ; :: thesis: x in X
then ex y being set st [x,y] in R by RELAT_1:def 4;
hence x in X by ZFMISC_1:106; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng R or y in Y )
assume y in rng R ; :: thesis: y in Y
then ex x being set st [x,y] in R by RELAT_1:def 5;
hence y in Y by ZFMISC_1:106; :: thesis: verum