Beweise D69
RG, TG1e (1) G(S,K(T’(H,r*),T(S,f))); mit T.V1 G(S,KT(S,f)), mit
(1) also wegen TG1c G(S,K(T(S,f)) K(T’(H,r*),T(S,f))), mit C5 und
RG, TG1e also G(S,K(T(S,f) T’(H,r*))), mit G(S,K(T’(H,r*)
T(S,f))) wegen TG1c also G(S,K(T(S,f) T’(H,r*)) K(T’(H,r*)
T(S,f))), mit C4, RG, TG1e also G(S,K(T’(H,r*) T(S,f))).
Für (i.4.2): Nach (i.3) aus den gegebenen Voraussetzungen
G(S,K(G’(H,I(S,f,T’(H,r*))),T(S,f))), mit TV1, d.h. G(S,KT(S,f)), also
wegen TG1c G(S,K(T(S,f)) K(G’(H,I(S,f,T’(H,r*))),T(S,f))), mit C5,
RG, TG1e also (1) G(S,K(T(S,f) G’(H,I(S,f,T’(H,r*))))). Aus T.V2 –
d.h. G(S,K(G’(H,T(S,f)) T(S,f))), mit RC, C3, RG und TG1e
G(S,K(G’(H,T(S,f)) T(S,f))). ...