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