let Y be set ; :: thesis: for R being Relation holds R " Y c= dom R
let R be Relation; :: thesis: R " Y c= dom R
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R " Y or x in dom R )
assume x in R " Y ; :: thesis: x in dom R
then ex y being object st
( [x,y] in R & y in Y ) by Def12;
hence x in dom R by XTUPLE_0:def 12; :: thesis: verum