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
A1: ( w1 in W & w2 in W ) and
A2: w1 <> w2 by ZFMISC_1:def 10;
( w1 <> {} or w2 <> {} ) by A2;
hence not W is empty-membered by A1, Def11; :: thesis: verum