:: deftheorem Def23 defines -wff FOMODEL2:def 24 :
for S being Language
for m being natural Number
for w being string of S holds
( w is m -wff iff w in S -formulasOfMaxDepth m );