let X be set ; :: thesis: ( X is empty implies X is subset-closed )
assume X is empty ; :: thesis: X is subset-closed
then for x, y being set st x in X & y c= x holds
y in X ;
hence X is subset-closed by CLASSES1:def 1; :: thesis: verum