assume not R " Y is empty ; :: thesis: contradiction
then ex y being set st
( [ the Element of {} " Y,y] in {} & y in Y ) by Def14;
hence contradiction ; :: thesis: verum