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 )
assume A1: prob B = 0 ; :: thesis: A,B are_independent
then prob (A /\ B) <= 0 by Th19, XBOOLE_1:17;
then prob (A /\ B) = 0 by Th18;
hence A,B are_independent by A1; :: thesis: verum