:: deftheorem Def38 defines SubTerms FOMODEL1:def 38 :
for S being Language
for phi being 0wff string of S
for b₃ being |.(ar ((b₁ -firstChar) . b₂)).| -element Element of (AllTermsOf S) * holds
( b₃ = SubTerms phi iff phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . b₃) );