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