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