assume not R .: X is empty ; :: thesis: contradiction
then ex x being object st
( [x, the Element of {} .: X] in {} & x in X ) by Def11;
hence contradiction ; :: thesis: verum