reconsider S = a as Element of {a} by TARSKI:def 1;
take GrammarStr(# {a},S,{[S,(<*> {a})]} #) ; :: thesis: ( the carrier of GrammarStr(# {a},S,{[S,(<*> {a})]} #) = {a} & the Rules of GrammarStr(# {a},S,{[S,(<*> {a})]} #) = {[a,{}]} )
thus ( the carrier of GrammarStr(# {a},S,{[S,(<*> {a})]} #) = {a} & the Rules of GrammarStr(# {a},S,{[S,(<*> {a})]} #) = {[a,{}]} ) ; :: thesis: verum