let X be set ; :: thesis: for R being Relation holds R .: X c= rng R
let R be Relation; :: thesis: R .: X c= rng R
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in R .: X or y in rng R )
assume y in R .: X ; :: thesis: y in rng R
then ex x being set st
( [x,y] in R & x in X ) by Def13;
hence y in rng R by Def5; :: thesis: verum