for x being set
for S being Language st x in AllTermsOf S holds
ex nn being Element of NAT st x in (S -termsOfMaxDepth) . nn by Lm6;