set x = the Element of R " {};
( the Element of R " {} in R " {} implies ex y being object st
( [ the Element of R " {},y] in R & y in {} ) ) by Def12;
hence R " Y is empty ; :: thesis: verum