:: deftheorem defines Subst1 FOMODEL3:def 24 :
for S being Language
for l being literal Element of S
for t being termal string of S holds l Subst1 t = (id (AllFormulasOf S)) +* (l AtomicSubst t);