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