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 ;
then <*l*> in (S -termsOfMaxDepth) . 0 by Def30;
hence for b₁ being string of S st b₁ = <*l*> holds
b₁ is 0 -termal by Def33; :: thesis: verum