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