let a, b be set ; :: thesis: ( a <> b implies Terminals (SingleGrammar (a,b)) = {b} )
set E = SingleGrammar (a,b);
A1: the Rules of (SingleGrammar (a,b)) = {[a,<*b*>]} by Def8;
A2: the carrier of (SingleGrammar (a,b)) = {a,b} by Def8;
then reconsider x = a, y = b as Symbol of (SingleGrammar (a,b)) by TARSKI:def 2;
assume A3: a <> b ; :: thesis: Terminals (SingleGrammar (a,b)) = {b}

A4: now :: thesis: for n being FinSequence holds not y ==> n

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

end;

[x,<*y*>] in the Rules of (SingleGrammar (a,b)) by A1, TARSKI:def 1;
then A5: x ==> <*y*> ;
thus Terminals (SingleGrammar (a,b)) c= {b} :: according to XBOOLE_0:def 10 :: thesis: {b} c= Terminals (SingleGrammar (a,b))

proof

let c be object ; :: 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
A6: c = s and
A7: for n being FinSequence holds not s ==> n ;
s <> x by A5, A7;
then c = b by A2, A6, TARSKI:def 2;
hence c in {b} by TARSKI:def 1; :: thesis: verum

end;

let c be object ; :: 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 c = b by TARSKI:def 1;
hence c in Terminals (SingleGrammar (a,b)) by A4; :: thesis: verum