let X be set ; :: thesis: ( not X is empty-membered implies not X is empty )
assume not X is empty-membered ; :: thesis: not X is empty
then ex x being non empty set st x in X by Def11;
hence not X is empty ; :: thesis: verum