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 A /\ B = {} E by XBOOLE_0:def 7;
hence prob (A /\ B) = 0 by CARD_1:27; :: thesis: verum