set m = Depth phi;
set psi = <*l*> ^ phi;
set M = Depth (<*l*> ^ phi);
Depth phi < Depth (<*l*> ^ phi) by Lm28;
hence for b₁ being string of S st b₁ = <*l*> ^ phi holds
not b₁ is Depth phi -wff by Def30; :: thesis: verum