set A = AllTermsOf S;
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;

A1: now :: thesis: for x being object st x in AllTermsOf S holds
x in (AllSymbolsOf S) *

let x be object ; :: thesis: ( x in AllTermsOf S implies x in (AllSymbolsOf S) * )
assume x in AllTermsOf S ; :: thesis: x in (AllSymbolsOf S) *
then consider mm being Element of NAT such that
A2: x in (S -termsOfMaxDepth) . mm by Lm6;
thus x in (AllSymbolsOf S) * by A2; :: thesis: verum

end;

AllTermsOf S = ((S -termsOfMaxDepth) . 0) \/ (AllTermsOf S) by Th2, XBOOLE_1:12
.= (AtomicTermsOf S) \/ (AllTermsOf S) by Def30 ;
hence AllTermsOf S is non empty Subset of ((AllSymbolsOf S) *) by A1, TARSKI:def 3; :: thesis: verum