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 set ; :: 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 set st
( [x,y] in R & y in Y ) by Def14;
hence x in dom R by Def4; :: thesis: verum