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
B0: Depth phi = m + 1 by NAT_1:6;
set Phim = S -formulasOfMaxDepth m;
phi in m -ExFormulasOf S by B0, Lm14;
then consider ll being Element of LettersOf S, phim being Element of S -formulasOfMaxDepth m such that
B1: phi = <*ll*> ^ phim ;
reconsider phimm = phim as m -wff string of S by DefWff1;
phi = (<*ll*> ^ phimm) ^ {} by B1;
hence for b₁ being set st b₁ = tail phi holds
b₁ is empty by Th23; :: thesis: verum