set psi = (l1,l2) -SymbolSubstIn phi;
consider m being Nat such that
B0: phi is m -wff by FOMODEL2:def 25;
thus for b₁ being string of S st b₁ = (l1,l2) -SymbolSubstIn phi holds
b₁ is wff by B0; :: thesis: verum