set A = AtomicTermsOf S;
set L = LettersOf S;
set T = S -termsOfMaxDepth ;
let w be string of S; :: thesis: ( w is 0 -termal implies w is 1 -element )
assume w is 0 -termal ; :: thesis: w is 1 -element
then w in (S -termsOfMaxDepth) . 0 ;
then w in AtomicTermsOf S by Def30;
then reconsider ww = w as Element of 1 -tuples_on (LettersOf S) ;
ww is 1 -element ;
hence w is 1 -element ; :: thesis: verum