:: deftheorem Def33 defines -termal FOMODEL1:def 33 :
for m being Nat
for S being Language
for w being string of S holds
( w is m -termal iff w in (S -termsOfMaxDepth) . m );