set X = {<*0*>,<*1*>};
for a being object st a in {<*0*>,<*1*>} holds
a is FinSequence by TARSKI:def 2;
then reconsider X = {<*0*>,<*1*>} as FinSequence-membered set by FINSEQ_1:def 19;
take X ; :: thesis: not X is trivial
A1: ( <*0*> in X & <*1*> in X ) by TARSKI:def 2;
( <*0*> . 1 = 0 & <*1*> . 1 = 1 ) ;
hence not X is trivial by A1, ZFMISC_1:def 10; :: thesis: verum