for mm being Element of NAT
for S being Language holds (S -termsOfMaxDepth) . mm c= AllTermsOf S