set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set A = AtomicTermsOf S;
set w = the Element of AtomicTermsOf S;
Z0: 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 Lm9, DefTerm;
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 Lm2, Z0, DefTerm;
hence ww is m -termal by DefTermal; :: thesis: verum