set T = S -termsOfMaxDepth ;
set Z = AtomicTermsOf S;
set SS = AllSymbolsOf S;
set x = the Element of AtomicTermsOf S;
( the Element of AtomicTermsOf S in AtomicTermsOf S & AtomicTermsOf S = (S -termsOfMaxDepth) . 0 ) by Def30;
then ( the Element of AtomicTermsOf S in (S -termsOfMaxDepth) . 0 & (S -termsOfMaxDepth) . 0 c= (S -termsOfMaxDepth) . (0 + m) ) by Lm5;
hence not (S -termsOfMaxDepth) . m is empty ; :: thesis: verum