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

ex phi2 being m -wff string of S st tail phi = phi2

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

ex phi2 being m -wff string of S st tail phi = phi2

let phi be wff string of S; :: thesis: ( Depth phi = m + 1 & not phi is exal implies ex phi2 being m -wff string of S st tail phi = phi2 )

set d = Depth phi;

set Phim = S -formulasOfMaxDepth m;

set N = TheNorSymbOf S;

assume ( Depth phi = m + 1 & not phi is exal ) ; :: thesis: ex phi2 being m -wff string of S st tail phi = phi2

then phi in m -NorFormulasOf S by Lm29;

then consider phi1, phi2 being Element of S -formulasOfMaxDepth m such that

A1: phi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ;

reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S by Def23;

set d1 = Depth phi11;

set d2 = Depth phi22;

take phi22 ; :: thesis: tail phi = phi22

phi = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi22 by A1;

hence phi22 = tail phi by Th23; :: thesis: verum

thus verum ; :: thesis: verum

for phi being wff string of S st Depth phi = m + 1 & not phi is exal holds

ex phi2 being m -wff string of S st tail phi = phi2

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

ex phi2 being m -wff string of S st tail phi = phi2

let phi be wff string of S; :: thesis: ( Depth phi = m + 1 & not phi is exal implies ex phi2 being m -wff string of S st tail phi = phi2 )

set d = Depth phi;

set Phim = S -formulasOfMaxDepth m;

set N = TheNorSymbOf S;

assume ( Depth phi = m + 1 & not phi is exal ) ; :: thesis: ex phi2 being m -wff string of S st tail phi = phi2

then phi in m -NorFormulasOf S by Lm29;

then consider phi1, phi2 being Element of S -formulasOfMaxDepth m such that

A1: phi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ;

reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S by Def23;

set d1 = Depth phi11;

set d2 = Depth phi22;

take phi22 ; :: thesis: tail phi = phi22

phi = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi22 by A1;

hence phi22 = tail phi by Th23; :: thesis: verum

thus verum ; :: thesis: verum