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)) \ (S -formulasOfMaxDepth m) = (((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)) \ (S -formulasOfMaxDepth m) by Th9
.= ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \ (S -formulasOfMaxDepth m) 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 B0, Def30;
then ( phi in S -formulasOfMaxDepth (m + 1) & not phi in S -formulasOfMaxDepth m ) ;
then Z1: phi in (S -formulasOfMaxDepth (m + 1)) \ (S -formulasOfMaxDepth m) 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 Z0, Z1, XBOOLE_0:def 3; :: thesis: verum