theorem :: FOMODEL2:18

for m being Nat
for S being Language
for phi being wff string of S st Depth phi = m + 1 holds
( ( phi is exal implies phi in m -ExFormulasOf S ) & ( phi in m -ExFormulasOf S implies phi is exal ) & ( not phi is exal implies phi in m -NorFormulasOf S ) & ( phi in m -NorFormulasOf S implies not phi is exal ) ) by Lm27, Lm29;