:: deftheorem defines SubstIn FOMODEL3:def 25 :
for S being Language
for l being literal Element of S
for t being termal string of S
for phi being wff string of S holds (l,t) SubstIn phi = (((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi;