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

Z0: now

let x be set ; :: 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
C1: x in (S -termsOfMaxDepth) . mm by Lm26;
thus x in (AllSymbolsOf S) * by C1; :: thesis: verum

end;

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