:: deftheorem Def7 defines EmptyGrammar LANG1:def 7 :
for a being set
for b₂ being strict GrammarStr holds
( b₂ = EmptyGrammar a iff ( the carrier of b₂ = {a} & the Rules of b₂ = {[a,{}]} ) );