:: deftheorem defines AllFormulasOf FOMODEL2:def 27 :
for S being Language holds AllFormulasOf S = { w where w is string of S : ex m being Nat st w is m -wff } ;