let nt be Symbol of PeanoNat; :: thesis: TerminalLanguage nt = {<*0*>}
A1: ( nt = S or nt = O ) by Lm2, TARSKI:def 2;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {<*0*>} c= TerminalLanguage nt
let x be object ; :: thesis: ( x in TerminalLanguage nt implies x in {<*0*>} )
assume x in TerminalLanguage nt ; :: thesis: x in {<*0*>}
then ex tsg being Element of FinTrees the carrier of PeanoNat st
( x = TerminalString tsg & tsg in TS PeanoNat & tsg . {} = nt ) ;
then x = <*O*> by Th13;
hence x in {<*0*>} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {<*0*>} or x in TerminalLanguage nt )
assume x in {<*0*>} ; :: thesis: x in TerminalLanguage nt
then A2: x = <*O*> by TARSKI:def 1;
reconsider prtO = root-tree O as Element of TS PeanoNat ;
reconsider rtO = root-tree O as Element of TS PeanoNat ;
reconsider srtO = <*prtO*> as FinSequence of TS PeanoNat ;
A3: rtO . {} = O by TREES_4:3;
then S ==> roots <*rtO*> by Lm5, Th4;
then A4: S -tree <*prtO*> in TS PeanoNat by Def1;
then A5: TerminalString (S -tree srtO) = x by A2, Th13;
A6: (S -tree <*rtO*>) . {} = S by TREES_4:def 4;
TerminalString rtO = x by A2, Th13;
hence x in TerminalLanguage nt by A1, A3, A4, A5, A6; :: thesis: verum