D54 Georg Meggle
Für (ii.1)
(ii.1.1): WG
1
(KV(S,H,f,I) T(S,f)) trivial nach T.K1, D1
(ii.1.2): WG
1
(KV(S,H,f,I) P(S,G’(H,MI(S,H,f,MI))))
(ii.1.3): WG
1
(KV(S,H,f,I)
G(S,K(G’(H,MI(S,H,f,MI)),TS(,f)))
(ii.1.4): WG
1
(KV(S,H,f,I)
G(S,G’(H,MI(S,H,f,MI)) T(S,f)))
Und daraus dann mit D1 (ii.1).
Für (ii.1.2): Aus KV(S.H,f,I) nach T.K1 I(S,f,G’(H,I)), mit T.I4 also
P(S,T(S,f)). Aus WG
1
und KV(S,H,f,I) mit dem gleich zu beweisenden
Satz (ii.1.3) G(S,K(G’(H,MI(S,H,f,MI)),T(S,f))), mit C6, TG1e also G
(S,T(S,f) G’(H,MI(S,H,f,MI))), und daraus mit P(S,T(S,f)) wegen P3
P(S,G’(H,MI(S,H,f,MI))).
Für (ii.1.3): Aus KV(S,H,f,I) nach T.K22 I(S,f,G’(H,KV(S,H,f,I)));
und daraus nach D1 (1) ...