for S being Language
for V being Element of (AllTermsOf S) * ex mm being Element of NAT st V is Element of ((S -termsOfMaxDepth) . mm) * by Lm3;