D74 Georg Meggle
Für (i.1): trivial nach D1.
Für (i.2): trivial nach D1 wegen I(S,f,T’(H,r)).
Für (i.3): Wegen T.K1: KV(S,H,f,r) I(S,f,T’(H,r)) ├, wegen TG1a also
() G’(H,KV(S,H,f,r)) G’(H,I(S,f,T’(H,r))) ├. Da nach D1 I(S,f,T’(H,r))
T(S,f) ├, nach TG1a also G’(H,I(S,f,T’(H,r))) G’(H,T(S,f)) ├, mit RC,
C2 und RG also G(S,K(G’(H,I(S,f,T’(H,r))) G’(H,T(S,f)))), mit
G(S,K(G’(H,T(S,f)) T(S,f))) – aus T.V2 mit RC, C3, TG1a – also
wegen C4, C3, TG1a G(S,K(G’(H,I(S,f,T’(H,r))) T(S,f))), mit V6 – d.h.
mit: G(S,KG’(H,I(S,f,T’(H,r)))), wegen C5, RG, TG1a, TG1c
dann G(S,K(T(S,f),G’(H,I(S,f,T’(H,r))))), mit C6, TG1a also ()
G(S,G’(H,I(S,f,T’(H,r))) T(S,f)). Mit () und () und T.I10 aus ...