let a, b be set ; :: thesis: ( a <> b implies Terminals (IterGrammar a,b) = {b} )
set T = IterGrammar a,b;
assume A1: a <> b ; :: thesis: Terminals (IterGrammar a,b) = {b}
A2: the carrier of (IterGrammar a,b) = {a,b} by Def9;
then reconsider x = a, y = b as Symbol of (IterGrammar a,b) by TARSKI:def 2;
A3: the Rules of (IterGrammar a,b) = {[a,<*b,a*>],[a,{} ]} by Def9;
thus Terminals (IterGrammar a,b) c= {b} :: according to XBOOLE_0:def 10 :: thesis: {b} c= Terminals (IterGrammar a,b)

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in Terminals (IterGrammar a,b) or c in {b} )
assume c in Terminals (IterGrammar a,b) ; :: thesis: c in {b}
then consider s being Symbol of (IterGrammar a,b) such that
A4: c = s and
A5: for n being FinSequence holds not s ==> n ;
[a,<*b,a*>] in the Rules of (IterGrammar a,b) by A3, TARSKI:def 2;
then x ==> <*y,x*> by Def1;
then s <> x by A5;
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 (IterGrammar a,b) )
assume c in {b} ; :: thesis: c in Terminals (IterGrammar a,b)
then A6: b = c by TARSKI:def 1;
assume not c in Terminals (IterGrammar a,b) ; :: thesis: contradiction
then consider n being FinSequence such that
A7: y ==> n by A6;
A8: [a,{} ] <> [b,n] by A1, ZFMISC_1:33;
[a,<*b,a*>] <> [b,n] by A1, ZFMISC_1:33;
then not [b,n] in {[a,<*b,a*>],[a,{} ]} by A8, TARSKI:def 2;
hence contradiction by A3, A7, Def1; :: thesis: verum