D36 Georg Meggle
und
T.K75.1.b: I*(S,H,f,KV(S,H,f,r)) I(S,f,G’(H,KV(S,H,f,r)))
T.K75.1.b direct aus D9.
Für T.K75.1.a: Es gilt:
T.K36: KV(S,H,f,r) I*(S,H,f,r)
Und daraus mit D11’, D9 – Mit T’(H,G’(x,p)) G’(H,p) – dann
T.K36.1: KV(S,H,f,p) I*(S,H,f,p)
Und daraus, mit KV(S,H,f,r) für p, dann direkt
() KV(S,H,f,KV(S,H,f,r)) I*(S,H,f,KV(S,H,f,r))
Aus T.K75 mit () dann direct T.K75.1.a.
Für T.K75.2: I(S,f,G’(H,KV(S,H,f,r))) MI(S,H,f,KV(S,H,f,r))
Dazu ist zu zeigen:
T.K75.2.1: I(S,f,G’(H,KV(S,H,f,r))) MI(S,H,f,KV(S,H,f,r))
T.K75.2.2: MI(S,H,f,KV(S,H,f,r)) I(S,f,G’(H,KV(S,H,f,r)))
T.K75.2.2 direkt wegen L.1 mit G’(H,p) statt T’(H,r) und KV(S,H,f,r) für
p.
Für T.K75.2.1: Aus I(S,f,G’(H,KV(S,H,f,r))) ...