set T = {<*0*>,<*1*>};
for a being object st a in {<*0*>,<*1*>} holds
a is FinSequence by TARSKI:def 2;
then reconsider T = {<*0*>,<*1*>} as non empty FinSequence-membered set by FINSEQ_1:def 19;
for p being FinSequence st p in T holds
dom p = Seg 1

proof

let p be FinSequence; :: thesis: ( p in T implies dom p = Seg 1 )
assume p in T ; :: thesis: dom p = Seg 1
then ( p = <*0*> or p = <*1*> ) by TARSKI:def 2;
hence dom p = Seg 1 by FINSEQ_1:def 8; :: thesis: verum

end;

then reconsider T = T as Polish-language by Th45;
take T ; :: thesis: not T is trivial
not T is trivial

proof

assume A3: T is trivial ; :: thesis: contradiction
( <*0*> in T & <*1*> in T ) by TARSKI:def 2;
then <*0*> = <*1*> by ZFMISC_1:def 10, A3;
then 0 = <*1*> . 1 ;
hence contradiction ; :: thesis: verum

end;

hence not T is trivial ; :: thesis: verum