let X be set ; :: thesis: ( not X is empty & X is with_non-empty_elements implies X is with_non-empty_element )
assume that
A1: not X is empty and
A2: X is with_non-empty_elements ; :: thesis: X is with_non-empty_element
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