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, Th68;
then 1 - (prob (A ` ),B) = 0 by A1, Th70;
hence prob (A ` ),B = 1 ; :: thesis: verum