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
A1: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi ) by Lm33;
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 A1, FOMODEL0:def 22; :: thesis: verum