set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set A = AtomicTermsOf S;
set AA = AllTermsOf S;
let t be Element of AllTermsOf S; :: thesis: not t is empty
consider mm being Element of NAT such that
A1: t in (S -termsOfMaxDepth) . mm by Lm6;
reconsider tt = t as Element of (S -termsOfMaxDepth) . mm by A1;
not tt is empty ;
hence not t is empty ; :: thesis: verum