:: deftheorem defines AllTermsOf FOMODEL1:def 31 :
for S being Language holds AllTermsOf S = union (rng (S -termsOfMaxDepth));