let X be set ; :: thesis: ( not X is empty & X is with_non-empty_elements implies not X is empty-membered )
assume that
A1: not X is empty and
A2: X is with_non-empty_elements ; :: thesis: not X is empty-membered
consider x being Element of X such that
A3: x in [#] X by A1, SUBSET_1:4;
reconsider x = x as non empty set by A2, A3;
take x ; :: according to SETFAM_1:def 10 :: thesis: x in X
thus x in X by A3; :: thesis: verum