:: deftheorem Def37 defines SubTerms FOMODEL1:def 37 :
for S being Language
for t being termal string of S
for b₃ being Element of (AllTermsOf S) * holds
( b₃ = SubTerms t iff ( b₃ is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b₃) ) );