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_{1} being string of S st b_{1} = (l1,l2) -SymbolSubstIn phi holds

b_{1} is m -wff
by A1, FOMODEL0:def 22; :: thesis: verum

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

b