D62 Georg Meggle
Für (ii): Aus IE(S,f,G’(H,KV(S,H,f,r))) nach D12 direkt
I(S,f,G’(H,KV(S,H,f,r)) und daraus nach T.K75.f direkt
(1) KV(S,H,f,MI(S,H,f,r)).
Da nun, falls KV(S,H,f,r) , daraus nach T.K67.1a KV(S,H,f,KV(S,H,r))
und daraus nach T.K74 KVS(,H,f,MI(S,H,f,r)), aus
K(G’(H,KV(S,H,f,r)),T(S,f))) mit TG1e, RC nd C3 also auch
(2) K(G’(H,KV(S,H,f,MI(S,H,f,r))),T(S,f))
Da nun, falls KV(S,H,f,r), daraus nach T.K0 MI(S,H,f,r), aus
K(G’(H,KV(S,H,f,r)),T(S,f)) wiederum mit TG1e, RC und C3 auch
K(G’(H,MI),T(S,f)), mit KT(S,f) – aus T.V1.E – also wegen C5
auch (.1) K(T(S,f) G’(H,MI(S,H,f,r))). Da nun aber
K(G’(H,T(S,f)),T(S,f)), mit G1 und RC, C3 auch
K(G’(H,T(S,f)),T(S,f)), ...