reconsider mm = m as Element of NAT by ORDINAL1:def 12;
let w be string of S; :: thesis: ( w is m -termal implies w is termal )
assume w is m -termal ; :: thesis: w is termal
then ( w in (S -termsOfMaxDepth) . m & (S -termsOfMaxDepth) . mm c= AllTermsOf S ) by Th2;
hence w is termal ; :: thesis: verum