:: deftheorem defines -subTerms FOMODEL1:def 39 :
for S being Language
for b₂ being Function of (AllTermsOf S),((AllTermsOf S) *) holds
( b₂ = S -subTerms iff for t being Element of AllTermsOf S holds b₂ . t = SubTerms t );