(l,t,nn,f) Subst2 phi in AllFormulasOf S by FOMODEL2:16;
hence (l,t,nn,f) Subst2 phi is Element of AllFormulasOf S ; :: thesis: verum