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} & the InitialSym of (IterGrammar a,b) = a & the Rules of (IterGrammar a,b) = {[a,<*b,a*>],[a,{} ]} ) by Def9;
then reconsider x = a, y = b as Symbol of (IterGrammar a,b) by TARSKI:def 2;
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
A3: ( c = s & ( for n being FinSequence holds not s ==> n ) ) ;
[a,<*b,a*>] in the Rules of (IterGrammar a,b) by A2, TARSKI:def 2;
then x ==> <*y,x*> by Def1;
then s <> x by A3;
then c = b by A2, A3, 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 A4: b = c by TARSKI:def 1;
assume not c in Terminals (IterGrammar a,b) ; :: thesis: contradiction
then consider n being FinSequence such that
A5: y ==> n by A4;
( [a,<*b,a*>] <> [b,n] & [a,{} ] <> [b,n] ) by A1, ZFMISC_1:33;
then not [b,n] in {[a,<*b,a*>],[a,{} ]} by TARSKI:def 2;
hence contradiction by A2, A5, Def1; :: thesis: verum