let E be non empty finite set ; :: thesis: for A, B being Event of E st prob B = 0 holds
A,B are_independent
let A, B be Event of E; :: thesis: ( prob B = 0 implies A,B are_independent )
A1: 0 = (prob A) * 0 ;
assume A2: prob B = 0 ; :: thesis: A,B are_independent
then prob (A /\ B) <= 0 by Th44, XBOOLE_1:17;
then prob (A /\ B) = 0 by Th43;
hence A,B are_independent by A2, A1, Def6; :: thesis: verum