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