let X be set ; :: thesis: ( not X is empty & X is subset-closed implies X is with_empty_element )
assume A1: ( not X is empty & X is subset-closed ) ; :: thesis: X is with_empty_element
then consider x being set such that
A2: x in X by XBOOLE_0:def 1;
{} c= x by XBOOLE_1:2;
then {} in X by A1, A2, CLASSES1:def 1;
hence X is with_empty_element ; :: thesis: verum