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

proof

reconsider b = D as Symbol of (TotalGrammar D) by Def10;
let a be object ; :: 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
A3: a = s and
A4: for n being FinSequence holds not s ==> n ;
[D,{}] in {[D,{}]} by TARSKI:def 1;
then [D,{}] in the Rules of (TotalGrammar D) by A1, XBOOLE_0:def 3;
then b ==> <*> the carrier of (TotalGrammar D) ;
then s <> D by A4;
then not s in {D} by TARSKI:def 1;
hence a in D by A2, A3, XBOOLE_0:def 3; :: thesis: verum

end;

let a be object ; :: 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 A2, XBOOLE_0:def 3;
assume not a in Terminals (TotalGrammar D) ; :: thesis: contradiction
then consider n being FinSequence such that
A5: x ==> n ;
A6: not a in a ;
then a <> D ;
then [a,n] <> [D,{}] by XTUPLE_0:1;
then A7: not [a,n] in {[D,{}]} by TARSKI:def 1;
[a,n] in the Rules of (TotalGrammar D) by A5;
then [a,n] in { [D,<*d,D*>] where d is Element of D : d = d } by A1, A7, XBOOLE_0:def 3;
then ex d being Element of D st
( [a,n] = [D,<*d,D*>] & d = d ) ;
then a = D by XTUPLE_0:1;
hence contradiction by A6; :: thesis: verum