let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma st A,B are_independent_respect_to P holds
B,A are_independent_respect_to P
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A, B being Event of Sigma st A,B are_independent_respect_to P holds
B,A are_independent_respect_to P
let P be Probability of Sigma; :: thesis: for A, B being Event of Sigma st A,B are_independent_respect_to P holds
B,A are_independent_respect_to P
let A, B be Event of Sigma; :: thesis: ( A,B are_independent_respect_to P implies B,A are_independent_respect_to P )
assume A,B are_independent_respect_to P ; :: thesis: B,A are_independent_respect_to P
then P . (B /\ A) = (P . B) * (P . A) by Def5;
hence B,A are_independent_respect_to P by Def5; :: thesis: verum