let a, b be set ; ( a <> b implies Terminals (IterGrammar (a,b)) = {b} )
set T = IterGrammar (a,b);
assume A1:
a <> b
; 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}
XBOOLE_0:def 10 {b} c= Terminals (IterGrammar (a,b))proof
let c be
object ;
TARSKI:def 3 ( not c in Terminals (IterGrammar (a,b)) or c in {b} )
assume
c in Terminals (IterGrammar (a,b))
;
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;
verum
end;
let c be object ; TARSKI:def 3 ( not c in {b} or c in Terminals (IterGrammar (a,b)) )
assume
c in {b}
; c in Terminals (IterGrammar (a,b))
then A6:
b = c
by TARSKI:def 1;
assume
not c in Terminals (IterGrammar (a,b))
; 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; verum