:: deftheorem defines -ExFormulasOf FOMODEL2:def 29 :
for S being Language
for m being Nat holds m -ExFormulasOf S = { (<*v*> ^ phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : verum } ;