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

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

end;

[x,<*y*>] in the Rules of (SingleGrammar a,b) by A1, TARSKI:def 1;
then A5: 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
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 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 c = b by TARSKI:def 1;
hence c in Terminals (SingleGrammar a,b) by A4; :: thesis: verum