:: deftheorem defines AtomicSubst FOMODEL3:def 19 :
for S being Language
for l being literal Element of S
for tt being Element of AllTermsOf S
for phi0 being 0wff string of S holds (l,tt) AtomicSubst phi0 = <*((S -firstChar) . phi0)*> ^ ((S -multiCat) . ((((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0)));