let W be set ; :: thesis: ( not W is trivial implies W is with_non-empty_element )
assume not W is trivial ; :: thesis: W is with_non-empty_element
then consider w1, w2 being object such that
A1: ( w1 in W & w2 in W ) and
A2: w1 <> w2 by ZFMISC_1:def 10;
( w1 <> {} or w2 <> {} ) by A2;
hence W is with_non-empty_element by A1; :: thesis: verum