theorem Th9: :: FOMODEL2:9

for m being Nat
for S being Language holds S -formulasOfMaxDepth (m + 1) = ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)