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