:: deftheorem defines -NorFormulasOf FOMODEL2:def 30 :
for S being Language
for m being Nat holds m -NorFormulasOf S = { ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : verum } ;