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

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in Lang (SingleGrammar a,b) or c in {<*b*>} )
assume c in Lang (SingleGrammar a,b) ; :: thesis: c in {<*b*>}
then consider p being String of (SingleGrammar a,b) such that
A4: ( c = p & rng p c= Terminals (SingleGrammar a,b) & p is_derivable_from <*the InitialSym of (SingleGrammar a,b)*> ) ;
consider q being FinSequence such that
A5: ( len q >= 1 & q . 1 = <*the InitialSym of (SingleGrammar a,b)*> & q . (len q) = p & ( for i being Element of NAT st i >= 1 & i < len q holds
ex a, b being String of (SingleGrammar a,b) st
( q . i = a & q . (i + 1) = b & a ==> b ) ) ) by A4, Def5;

now

assume p = <*x*> ; :: thesis: contradiction
then rng p = {x} by FINSEQ_1:55;
then x in rng p by TARSKI:def 1;
hence contradiction by A1, A2, A4, TARSKI:def 1; :: thesis: verum

end;

then A6: len q > 1 by A3, A5, XXREAL_0:1;
then consider n, m being String of (SingleGrammar a,b) such that
A7: ( q . 1 = n & q . (1 + 1) = m & n ==> m ) by A5;
x ==> m by A3, A5, A7, Th4;
then [x,m] in {[a,<*b*>]} by A3, Def1;
then [x,m] = [a,<*b*>] by TARSKI:def 1;
then A8: ( m = <*b*> & 1 <= 2 ) by ZFMISC_1:33;

now

assume 2 < len q ; :: thesis: contradiction
then consider k, l being String of (SingleGrammar a,b) such that
A9: ( q . 2 = k & q . (2 + 1) = l & k ==> l ) by A5;
y ==> l by A7, A8, A9, Th4;
then [y,l] in {[a,<*b*>]} by A3, Def1;
then [y,l] = [a,<*b*>] by TARSKI:def 1;
hence contradiction by A1, ZFMISC_1:33; :: thesis: verum

end;

then ( 2 >= len q & len q >= 1 + 1 ) by A6, NAT_1:13;
then c = <*b*> by A4, A5, A7, A8, XXREAL_0:1;
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 Lang (SingleGrammar a,b) )
assume c in {<*b*>} ; :: thesis: c in Lang (SingleGrammar a,b)
then A10: ( [a,<*b*>] in the Rules of (SingleGrammar a,b) & c = <*b*> & rng <*b*> = {b} ) by A3, FINSEQ_1:55, TARSKI:def 1;
then the InitialSym of (SingleGrammar a,b) ==> <*y*> by A3, Def1;
then <*y*> is_derivable_from <*the InitialSym of (SingleGrammar a,b)*> by Th3, Th7;
hence c in Lang (SingleGrammar a,b) by A2, A10; :: thesis: verum