let a, b be set ; :: thesis: ( a <> b implies Lang (SingleGrammar a,b) = {<*b*>} )
set E = SingleGrammar a,b;
A1: the InitialSym of (SingleGrammar a,b) = a by Def8;
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;
A2: the Rules of (SingleGrammar a,b) = {[a,<*b*>]} by Def8;
then [a,<*b*>] in the Rules of (SingleGrammar a,b) by TARSKI:def 1;
then the InitialSym of (SingleGrammar a,b) ==> <*y*> by A1, Def1;
then A3: <*y*> is_derivable_from <*the InitialSym of (SingleGrammar a,b)*> by Th3, Th7;
assume A4: a <> b ; :: thesis: Lang (SingleGrammar a,b) = {<*b*>}
then A5: Terminals (SingleGrammar a,b) = {b} by Th12;
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
A6: c = p and
A7: rng p c= Terminals (SingleGrammar a,b) and
A8: p is_derivable_from <*the InitialSym of (SingleGrammar a,b)*> ;
consider q being FinSequence such that
A9: len q >= 1 and
A10: q . 1 = <*the InitialSym of (SingleGrammar a,b)*> and
A11: q . (len q) = p and
A12: 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 A8, 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 A4, A5, A7, TARSKI:def 1; :: thesis: verum

end;

then A13: len q > 1 by A1, A9, A10, A11, XXREAL_0:1;
then consider n, m being String of (SingleGrammar a,b) such that
A14: q . 1 = n and
A15: q . (1 + 1) = m and
A16: n ==> m by A12;
x ==> m by A1, A10, A14, A16, Th4;
then [x,m] in {[a,<*b*>]} by A2, Def1;
then [x,m] = [a,<*b*>] by TARSKI:def 1;
then A17: m = <*b*> by ZFMISC_1:33;

A18: now

assume 2 < len q ; :: thesis: contradiction
then consider k, l being String of (SingleGrammar a,b) such that
A19: q . 2 = k and
q . (2 + 1) = l and
A20: k ==> l by A12;
y ==> l by A15, A17, A19, A20, Th4;
then [y,l] in {[a,<*b*>]} by A2, Def1;
then [y,l] = [a,<*b*>] by TARSKI:def 1;
hence contradiction by A4, ZFMISC_1:33; :: thesis: verum

end;

len q >= 1 + 1 by A13, NAT_1:13;
then c = <*b*> by A6, A11, A15, A17, A18, 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 A21: c = <*b*> by TARSKI:def 1;
rng <*b*> = {b} by FINSEQ_1:55;
hence c in Lang (SingleGrammar a,b) by A5, A21, A3; :: thesis: verum