D72 Georg Meggle
Für (ii.2.3): Falls (α) und (), dann bei T’(H,r) T’(H,r*) ├ und
KV(S,H,f,r) nach Induktionsvoraussetzung auch I
n
(S,H,f,MI(S,H,f,r*)).
Unter diesen Prämissen aus KV(S,H,f,r) nach T.K30 direkt auch
G
0
(S,K(G’(H,I
n
(S,H,f,MI(S,H,f,r*))),T(S,f))).
Für (ii.2.4): Aus T.V2.1 nach TG1a G(S,G’(H,T(S,f)) T(S,f)) –i.e.:
(1). Und da I
n
(S,H,f,MI(S,H,f,r*)) T(S,f) für bel. n 1, nach RG
auch G’(H,I
n
(S,H,f,MI(S,H,f,r*)) T(S,f)), nach G1 also
G’(H,I
n
(S,H,f,MI(S,H,f,r*))) G’(H,T(S,f)), nach RG also
G(S,G’(H,I
n
(S,H,f,MI(S,H,f,r*))) G’(H,T(S,f))), mit (1) nach TG1c,
RG, TG1e also G(S,G’(H,I
n
(S,H,f, MI(S,H,f,r*))) T(S,f))).
Für T.K80.1: A B ├ KV(S,H,f,A) (G(S,K(G’(H,B)) ...