let E be non empty finite set ; :: thesis: for A, B being Event of E st A misses B & A,B are_independent & not prob A = 0 holds
prob B = 0
let A, B be Event of E; :: thesis: ( A misses B & A,B are_independent & not prob A = 0 implies prob B = 0 )
assume that
A1: A misses B and
A2: A,B are_independent ; :: thesis: ( prob A = 0 or prob B = 0 )
prob (A /\ B) = 0 by A1, Th41;
then (prob A) * (prob B) = 0 by A2, Def6;
hence ( prob A = 0 or prob B = 0 ) by XCMPLX_1:6; :: thesis: verum