D24 Georg Meggle
nach TG1a x(xP G(x,G(x,A))), nach TG2a also auch x(xP
G(x,A)), i.e. nach D18.a GG
1
(P,A), i.e. trivial GG
2-1
(P,A).
Für (ii): Aus GG
n+1
(P,A) nach D18.b GG
1
(P,GG
n
(P,A)), nach D18.b
bei n 1 also wegen TG5-1 auch GG
1
(P,GG
1
(P,GG
n-1
(P,A))); und daraus
bei (i) GG
1
(P,GG
n-1
(P,A)), i.e. GG
n+1-1
(P,A)).
Für L.G4.1: x(xP G(x,xP))
(GG
n
(P,A) GG
m
(P,A)) für bel. m,n 1, mit m
n
Direkt aus L.G4 mit (n-m)-facher Anwendung desselben.
Für L.G4.2: x(xP G(x,xP))
(GW
n
(P,A) GG
n
(P,A) A) für bel. n 1
Aus GW
n
(P,A) direkt nach L.G2 GG
n
(P,A) A, insbesondere also auch
(a): x(xP G(x,xP)) (GW
n
(P,A) GG
n
(P,A) A), für bel. n 1.
Aus x(xP G(x,xP)) mit GG
n
(P,A)