set T = S -termsOfMaxDepth ;
set TS = TermSymbolsOf S;
let w be string of S; :: thesis: ( w is termal implies w is TermSymbolsOf S -valued )
assume w is termal ; :: thesis: w is TermSymbolsOf S -valued
then reconsider tt = w as termal string of S ;
set d = Depth tt;
reconsider t = tt null 0 as (Depth tt) + 0 -termal string of S ;
( t in (S -termsOfMaxDepth) . (Depth tt) & (S -termsOfMaxDepth) . (Depth tt) c= (TermSymbolsOf S) * ) by Lm11, Def33;
hence w is TermSymbolsOf S -valued ; :: thesis: verum