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