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 set ; :: 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 Th14;
hence x in {<*0 *>} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: 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 Lm4, Th4;
then A4: S -tree <*prtO*> in TS PeanoNat by Def4;
then ( TerminalString (S -tree srtO) = x & (S -tree <*rtO*>) . {} = S & TerminalString rtO = x ) by A2, Th14, TREES_4:def 4;
hence x in TerminalLanguage nt by A1, A3, A4; :: thesis: verum