:: deftheorem defines are_independent RPR_1:def 3 :
for E being finite set
for A, B being Event of E holds
( A,B are_independent iff prob (A /\ B) = (prob A) * (prob B) );