let m be Nat; :: thesis: for S being Language
for phi being wff string of S st Depth phi = m + 1 & not phi is exal holds
phi in m -NorFormulasOf S

let S be Language; :: thesis: for phi being wff string of S st Depth phi = m + 1 & not phi is exal holds
phi in m -NorFormulasOf S

let phi be wff string of S; :: thesis: ( Depth phi = m + 1 & not phi is exal implies phi in m -NorFormulasOf S )
set p = Depth phi;
set Phim = S -formulasOfMaxDepth m;
set E = m -ExFormulasOf S;
set PhiM = S -formulasOfMaxDepth (m + 1);
set N = m -NorFormulasOf S;
Z0: (S -formulasOfMaxDepth (m + 1)) \ () = ((() \/ ()) \/ ()) \ () by Th9
.= (() \/ ()) \ () by XBOOLE_1:40 ;
B0: m + 0 < m + 1 by XREAL_1:8;
assume Depth phi = m + 1 ; :: thesis: ( phi is exal or phi in m -NorFormulasOf S )
then ( phi is m + 1 -wff & not phi is m -wff ) by ;
then ( phi in S -formulasOfMaxDepth (m + 1) & not phi in S -formulasOfMaxDepth m ) ;
then Z1: phi in (S -formulasOfMaxDepth (m + 1)) \ () by XBOOLE_0:def 5;
assume not phi is exal ; :: thesis: phi in m -NorFormulasOf S
then not phi in m -ExFormulasOf S ;
hence phi in m -NorFormulasOf S by ; :: thesis: verum