:: deftheorem defines finite LANG1:def 12 :
for IT being GrammarStr holds
( IT is finite iff the Rules of IT is finite );