D34 Georg Meggle
Aus (i) und (ii) dann wegen T.K42.1 – mit KV(S,H,f,r) für p – T.K75a.
Für (i) zeigen wir:
(i.1) I(S,f,G’(H,KV(S,H,f,r))) T(S,f) trivial nach D1
(i.2) I(S,f,G’(H,KV(S,H,f,r))) P(S.G’(H,KV(S,H,f,))) dto.
(i.3) I(S,f,G’(H,KV(S,H,f,r)))
G(S,K(G’(H,I(S,f,G’(H,KV(S,H,f,KV(S,H,f,r)))),T(S,f)))
(i.4) I(S,f,G’(H,KV(S,H,f,r)))
G(S,K(G’(H,KV(S,H,f,r))
G’(H,I(S,f,G’(H,KV(S,H,f,r))))))
Für (i.3): Aus KV(S,H,f,r) nach T.K22 I(S,f,G’(H,KV(S,H,f,r))). Wegen
RG daher auch G’(H,KV(S,H,f,r) I(S,f,G’(H,KV(S,H,f,r)))), und daraus
wegen G1 auch () G’(H,KV(S,H,f,r)) G’(H,I(S,f,G’(H,KV(S,H,f,r)))).
Da () G(S,G’(H,I(S,f,G’(H,KV(S,H,f,r)))) T(S,f)) – wegen T.V2.1 aus
G(S,G’(H,T(S,f)) T(S,f)), und ...