set d = Depth phi;

set L = LettersOf S;

set h = head phi;

set t = tail phi;

set F = S -firstChar ;

set FF = AllFormulasOf S;

set SS = AllSymbolsOf S;

set s = (S -firstChar) . phi;

consider m being Nat such that

A1: Depth phi = m + 1 by NAT_1:6;

set Phim = S -formulasOfMaxDepth m;

phi in m -ExFormulasOf S by A1, Lm27;

then consider ll being Element of LettersOf S, phim being Element of S -formulasOfMaxDepth m such that

A2: phi = <*ll*> ^ phim ;

reconsider phimm = phim as m -wff string of S by Def23;

phi = (<*ll*> ^ phimm) ^ {} by A2;

hence for b_{1} being set st b_{1} = tail phi holds

b_{1} is empty
by Th23; :: thesis: verum

set L = LettersOf S;

set h = head phi;

set t = tail phi;

set F = S -firstChar ;

set FF = AllFormulasOf S;

set SS = AllSymbolsOf S;

set s = (S -firstChar) . phi;

consider m being Nat such that

A1: Depth phi = m + 1 by NAT_1:6;

set Phim = S -formulasOfMaxDepth m;

phi in m -ExFormulasOf S by A1, Lm27;

then consider ll being Element of LettersOf S, phim being Element of S -formulasOfMaxDepth m such that

A2: phi = <*ll*> ^ phim ;

reconsider phimm = phim as m -wff string of S by Def23;

phi = (<*ll*> ^ phimm) ^ {} by A2;

hence for b

b