let E be non empty finite set ; :: thesis: for A, B being Event of E st A,B are_independent holds
A ` ,B are_independent
let A, B be Event of E; :: thesis: ( A,B are_independent implies A ` ,B are_independent )
prob ((A `) /\ B) = prob (B \ A) by SUBSET_1:13;
then A1: prob ((A `) /\ B) = (prob B) - (prob (A /\ B)) by Th23;
assume A,B are_independent ; :: thesis: A ` ,B are_independent
then prob ((A `) /\ B) = (1 * (prob B)) - ((prob A) * (prob B)) by A1;
then prob ((A `) /\ B) = (1 - (prob A)) * (prob B) ;
then prob ((A `) /\ B) = (prob (A `)) * (prob B) by Th22;
hence A ` ,B are_independent ; :: thesis: verum