:: deftheorem Def23 defines AtomicSubst FOMODEL3:def 23 :
for S being Language
for l being literal Element of S
for t being termal string of S
for b₄ being Function of (AtomicFormulasOf S),(AtomicFormulasOf S) holds
( b₄ = l AtomicSubst t iff for phi0 being 0wff string of S
for tt being Element of AllTermsOf S st tt = t holds
b₄ . phi0 = (l,tt) AtomicSubst phi0 );