let W be set ; :: thesis: ( not W is trivial implies not W is empty-membered )
assume not W is trivial ; :: thesis: not W is empty-membered
then consider w1, w2 being set such that
W1: ( w1 in W & w2 in W ) and
W2: w1 <> w2 by ZFMISC_1:def 10;
( w1 <> {} or w2 <> {} ) by W2;
hence not W is empty-membered by W1, Def11; :: thesis: verum