let E be non empty finite set ; :: thesis: for A, B being Event of E st A misses B holds
prob (A,B) = 0
let A, B be Event of E; :: thesis: ( A misses B implies prob (A,B) = 0 )
assume A misses B ; :: thesis: prob (A,B) = 0
then prob (A,B) = 0 / (prob B) by Th16
.= 0 * ((prob B) ") ;
hence prob (A,B) = 0 ; :: thesis: verum