let a, b be set ; :: thesis: ( a <> b implies Terminals (SingleGrammar a,b) = {b} )
assume A1: a <> b ; :: thesis: Terminals (SingleGrammar a,b) = {b}
set E = SingleGrammar a,b;
A2: ( the carrier of (SingleGrammar a,b) = {a,b} & the InitialSym of (SingleGrammar a,b) = a & the Rules of (SingleGrammar a,b) = {[a,<*b*>]} & Terminals (SingleGrammar a,b) = { s where s is Symbol of (SingleGrammar a,b) : for n being FinSequence holds not s ==> n } ) by Def8;
then reconsider x = a, y = b as Symbol of (SingleGrammar a,b) by TARSKI:def 2;
[x,<*y*>] in the Rules of (SingleGrammar a,b) by A2, TARSKI:def 1;
then A3: x ==> <*y*> by Def1;
thus Terminals (SingleGrammar a,b) c= {b} :: according to XBOOLE_0:def 10 :: thesis: {b} c= Terminals (SingleGrammar a,b)

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in Terminals (SingleGrammar a,b) or c in {b} )
assume c in Terminals (SingleGrammar a,b) ; :: thesis: c in {b}
then consider s being Symbol of (SingleGrammar a,b) such that
A4: ( c = s & ( for n being FinSequence holds not s ==> n ) ) ;
s <> x by A3, A4;
then c = b by A2, A4, TARSKI:def 2;
hence c in {b} by TARSKI:def 1; :: thesis: verum

end;

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in {b} or c in Terminals (SingleGrammar a,b) )
assume c in {b} ; :: thesis: c in Terminals (SingleGrammar a,b)
then A5: c = b by TARSKI:def 1;

now

let n be FinSequence; :: thesis: not y ==> n
assume y ==> n ; :: thesis: contradiction
then [y,n] in {[a,<*b*>]} by A2, Def1;
then [y,n] = [a,<*b*>] by TARSKI:def 1;
hence contradiction by A1, ZFMISC_1:33; :: thesis: verum

end;

hence c in Terminals (SingleGrammar a,b) by A5; :: thesis: verum