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