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 object ; :: 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*> ;
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 object ; :: 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, XTUPLE_0:1;
[a,<*b,a*>] <> [b,n] by A1, XTUPLE_0:1;
then not [b,n] in {[a,<*b,a*>],[a,{}]} by A8, TARSKI:def 2;
hence contradiction by A3, A7; :: thesis: verum