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 Th41
.= 0 * ((prob B) " ) ;
hence prob A,B = 0 ; :: thesis: verum