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