:: deftheorem Def9 defines IterGrammar LANG1:def 9 :
for a, b being set
for b₃ being strict GrammarStr holds
( b₃ = IterGrammar (a,b) iff ( the carrier of b₃ = {a,b} & the InitialSym of b₃ = a & the Rules of b₃ = {[a,<*b,a*>],[a,{}]} ) );