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