D78 Georg Meggle
Und daraus dann nach D1 L.21.1.
Für (ii): Aus I(S,f,G’(H,I)) nach T.I4 P(S,T(S,f)). Und mit dem gleich zu
beweisenden Satz (iii) aus () und I(S,f,G’(H,I)) G(S,K(G’(H,MI),T(S,f))),
mit C6 und TG1e also auch G(S,T(S,f) G’(H,MI)), mit P(S,T(S,f)) also
wegen P3 auch P(S,G’(H,MI)).
Für (iii): () (I(S,f,G’(H,I)) G(S,K(G’(H,MI),T(S,f))))
Wir zeigen:
(iii.1) () (I(S,f,G’(H,I)) G(S,K(G’(H,I),T(S,f))))
und
(iii.2) () (I(S,f,G’(H,I)) G(S,K(G’(H,(d)),T(S,f))))
wobei (d): G(S,K(T’(H,r) G’(H,I)))
und daraus dann mit TG1c, C4, RC, C3 und TG1e
(iii.3) () (I(S,f,G’(H,I)) G(S,K(G’(H,I (d)),T(S,f))))
und daraus dann mit L.3, TG1e, RC, C3 schließlich (iii).
Da (iii.1) wegen I(S,f,G’(H,I)) ...