set w = <*l*>;
set L = LettersOf S;
set AT = AtomicTermsOf S;
set T = S -termsOfMaxDepth ;
reconsider ll = l as Element of LettersOf S by Def14;
<*l*> = <*ll*> ;
then <*l*> in AtomicTermsOf S by FINSEQ_2:98;
then <*l*> in (S -termsOfMaxDepth) . 0 by Def30;
hence for b₁ being string of S st b₁ = <*l*> holds
b₁ is 0 -termal ; :: thesis: verum