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

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