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₁ being set st b₁ = tail phi holds
b₁ is empty by Th23; :: thesis: verum