:: deftheorem Def24 defines wff FOMODEL2:def 25 :
for S being Language
for w being string of S holds
( w is wff iff ex m being Nat st w is m -wff );