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;
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 object ; :: 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;

now :: thesis: not p = <*x*>

assume p = <*x*> ; :: thesis: contradiction
then rng p = {x} by FINSEQ_1:38;
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;
then [x,m] = [a,<*b*>] by TARSKI:def 1;
then A17: m = <*b*> by XTUPLE_0:1;

A18: now :: thesis: not 2 < len q

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;
then [y,l] = [a,<*b*>] by TARSKI:def 1;
hence contradiction by A4, XTUPLE_0:1; :: 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 object ; :: 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:38;
hence c in Lang (SingleGrammar (a,b)) by A5, A21, A3; :: thesis: verum