set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set A = AtomicTermsOf S;
let w be Element of (S -termsOfMaxDepth) . m; :: thesis: not w is empty
w in ((AllSymbolsOf S) *) \ {{}} by Lm4, TARSKI:def 3;
hence not w is empty ; :: thesis: verum