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 ;
TARSKI:def 3 ( 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 }
;
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 *):]
;
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)]}) #)
; ( 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,{}]} )
; verum