A1: D in {D} by TARSKI:def 1;
reconsider E = succ D as non empty set ;
reconsider S = D as Element of E by A1, 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 set ; :: 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
A2: ( a = [S,<*d,S*>] & d = d ) ;
reconsider d = d as Element of E by XBOOLE_0:def 3;
a = [S,<*d,S*>] by A2;
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