let E be non empty finite set ; for A, B being Event of E st 0 < prob B & A misses B holds
prob ((A `),B) = 1
let A, B be Event of E; ( 0 < prob B & A misses B implies prob ((A `),B) = 1 )
assume that
A1:
0 < prob B
and
A2:
A misses B
; prob ((A `),B) = 1
prob (A,B) = 0
by A2, Th38;
then
1 - (prob ((A `),B)) = 0
by A1, Th40;
hence
prob ((A `),B) = 1
; verum