set D = Depth phi;
set e = l1 SubstWith l2;
reconsider d = m - (Depth phi) as Nat ;
consider psi being wff string of S such that
B0: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi ) by Lm37;
set DD = Depth psi;
psi null d is (Depth psi) + d -wff ;
hence for b₁ being string of S st b₁ = (l1,l2) -SymbolSubstIn phi holds
b₁ is m -wff by B0, FOMODEL0:def 23; :: thesis: verum