let X be set ; :: thesis: ( X <> {} implies ex x being set st x in X )
assume Z: X <> {} ; :: thesis: ex x being set st x in X
assume for x being set holds not x in X ; :: thesis: contradiction
then X is empty by Def5;
hence contradiction by Z, Lm1; :: thesis: verum