:: deftheorem Def32 defines termal FOMODEL1:def 32 :
for S being Language
for w being string of S holds
( w is termal iff w in AllTermsOf S );