:: deftheorem Def10 defines TotalGrammar LANG1:def 10 :
for D being non empty set
for b₂ being strict GrammarStr holds
( b₂ = TotalGrammar D iff ( the carrier of b₂ = succ D & the InitialSym of b₂ = D & the Rules of b₂ = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} ) );