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