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