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:32;
then A1: prob ((A ` ) /\ B) = (prob B) - (prob (A /\ B)) by Th49;
assume A,B are_independent ; :: thesis: A ` ,B are_independent
then prob ((A ` ) /\ B) = (1 * (prob B)) - ((prob A) * (prob B)) by A1, Def6;
then prob ((A ` ) /\ B) = (1 - (prob A)) * (prob B) ;
then prob ((A ` ) /\ B) = (prob (A ` )) * (prob B) by Th48;
hence A ` ,B are_independent by Def6; :: thesis: verum