reconsider E = succ D as non empty set ;
D in {D} by TARSKI:def 1;
then reconsider S = D as Element of E by XBOOLE_0:def 3;
set R = { [S,<*d,S*>] where d is Element of D : d = d } ;
{ [S,<*d,S*>] where d is Element of D : d = d } c= [:E,(E *):]

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [S,<*d,S*>] where d is Element of D : d = d } or a in [:E,(E *):] )
assume a in { [S,<*d,S*>] where d is Element of D : d = d } ; :: thesis: a in [:E,(E *):]
then consider d being Element of D such that
A1: a = [S,<*d,S*>] and
d = d ;
reconsider d = d as Element of E by XBOOLE_0:def 3;
a = [S,<*d,S*>] by A1;
hence a in [:E,(E *):] ; :: thesis: verum

end;

then reconsider R = { [S,<*d,S*>] where d is Element of D : d = d } as Relation of E,(E *) ;
take GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) ; :: thesis: ( the carrier of GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) = succ D & the InitialSym of GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) = D & the Rules of GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} )
thus ( the carrier of GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) = succ D & the InitialSym of GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) = D & the Rules of GrammarStr(# E,S,(R \/ {[S,(<*> E)]}) #) = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} ) ; :: thesis: verum