let D be non empty set ; :: thesis: Terminals (TotalGrammar D) = D
set T = TotalGrammar D;
A1: ( the carrier of (TotalGrammar D) = succ D & the InitialSym of (TotalGrammar D) = D & the Rules of (TotalGrammar D) = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{} ]} ) by Def10;
thus Terminals (TotalGrammar D) c= D :: according to XBOOLE_0:def 10 :: thesis: D c= Terminals (TotalGrammar D)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Terminals (TotalGrammar D) or a in D )
assume a in Terminals (TotalGrammar D) ; :: thesis: a in D
then consider s being Symbol of (TotalGrammar D) such that
A2: ( a = s & ( for n being FinSequence holds not s ==> n ) ) ;
( [D,{} ] in {[D,{} ]} & D in {D} ) by TARSKI:def 1;
then A3: ( [D,{} ] in the Rules of (TotalGrammar D) & D in succ D ) by A1, XBOOLE_0:def 3;
reconsider b = D as Symbol of (TotalGrammar D) by Def10;
b ==> <*> the carrier of (TotalGrammar D) by A3, Def1;
then s <> D by A2;
then not s in {D} by TARSKI:def 1;
hence a in D by A1, A2, XBOOLE_0:def 3; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in D or a in Terminals (TotalGrammar D) )
assume a in D ; :: thesis: a in Terminals (TotalGrammar D)
then reconsider a = a as Element of D ;
reconsider x = a as Symbol of (TotalGrammar D) by A1, XBOOLE_0:def 3;
assume not a in Terminals (TotalGrammar D) ; :: thesis: contradiction
then consider n being FinSequence such that
A4: x ==> n ;
A5: not a in a ;
then a <> D ;
then [a,n] <> [D,{} ] by ZFMISC_1:33;
then ( [a,n] in the Rules of (TotalGrammar D) & not [a,n] in {[D,{} ]} ) by A4, Def1, TARSKI:def 1;
then [a,n] in { [D,<*d,D*>] where d is Element of D : d = d } by A1, XBOOLE_0:def 3;
then ex d being Element of D st
( [a,n] = [D,<*d,D*>] & d = d ) ;
then a = D by ZFMISC_1:33;
hence contradiction by A5; :: thesis: verum