let E be non empty finite set ; :: thesis: 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; :: thesis: ( 0 < prob B & A misses B implies prob ((A `),B) = 1 )
assume that
A1: 0 < prob B and
A2: A misses B ; :: thesis: 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 ; :: thesis: verum