Beweise D33
und
T.K74.1b: VAKV(Y,S,H,f) r(VAK(S,S,H,f,r)
W(Y,VAKV(S,S,H,f,r)))
VKV(Y,S,H,f)
Für T.K74.1a: Aus VKV(Y,S,H,f) nach D7 direkt KV(S,H,f), woraus
nach D11.1 und T.K1 und D1 T(S,f), mit P0 somit f(S). Aus
VKV(Y,S,H,f) nach D7 ebenso G(Y,KV(S,H,f)), mit D3.2.1 also
VAKV(Y,S,H,f)) (i). Aus VKV(Y,S,H,f) nach D7 ferner r(KV(S,H,f,r)
W(Y,KV(S,H,f,r)), woraus, da KV(S,H,f,r) nach T.K44 äquivalent mit
f(S) – ebenfalls aus KV – und G(S,KV(S,H,f,r)), mit D3.1
r(VAKV(S,S,f,r) W(Y,VAKV(S,S,H,f,r))) (ii). Mit (i) somit bereits a.l.
T.K74.1a.
Für T.K74.1b: Sei VAK(S,S,H,r) für ein bel. r. Dann nach der 2. Bedin-
gung des Wenn-Satzes auch W(Y,VAKV(S,S,H,f,r)), d.h. nach D3.2 ...