set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set A = AtomicTermsOf S;
set w = the Element of AtomicTermsOf S;
A1: the Element of AtomicTermsOf S in AtomicTermsOf S ;
then ( the Element of AtomicTermsOf S in (S -termsOfMaxDepth) . 0 & (S -termsOfMaxDepth) . 0 c= ((AllSymbolsOf S) *) \ {{}} ) by Lm4, Def30;
then reconsider ww = the Element of AtomicTermsOf S as string of S ;
take ww ; :: thesis: ww is m -termal
( ww in (S -termsOfMaxDepth) . 0 & (S -termsOfMaxDepth) . 0 c= (S -termsOfMaxDepth) . (0 + m) ) by Lm5, A1, Def30;
hence ww is m -termal ; :: thesis: verum