D28 Georg Meggle
Für L.G9.1: x(GW
n
(P,B(x)) v GW
n
(P, B(x)))
(x(B(x) GG
n
(P,B(x))) x( B(x)
GG
n
(P, B(x)))) für
bel. n 1
Beweis direkt analog zu dem für TG.V in D.1, mit L.G1 anstelle von D0.
Für L.G10: x(GW
n
(P,B(x)) v GW
n
(P, B(x)))
(GG
m
(P,x(B(x) F(x))) x(B(x) GG
m
(P,F(x))))
für bel. m,n 1, mit m n
Direkt aus L.G10-1 und L.G10-2 mit L.G9-1.
Für L.G10.1: x(B(x) GW
n
(P,B(x)))
(GG
m
(P,x(B(x) F(x))) x(B(x) GG
m
(P,F(x))))
für bel. m,n 1, mit m n
Da aus x(B(x) GW
n
(P,B(x))) nach L.G3-3 x(B(x) GG
m
(P,B(x)))
für alle m n, L.G10-1 somit dann direkt mit T.G13a-1.
Für L.G10.2: x( B(x) GW
n
(P, B(x)))
(x(B(x) GW
n
(P,F(x))) GG
m
(P,x(B(x) F(x))))
für bel. ...