set D = Depth phi;
phi is (Depth phi) + (0 * m) -wff by FOMODEL2:def 31;
hence for b₁ being string of S st b₁ = phi null m holds
b₁ is (Depth phi) + m -wff ; :: thesis: verum