let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st A,B are_independent_respect_to P holds
([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P
let Sigma be SigmaField of Omega; :: thesis: for A, B being Event of Sigma
for P being Probability of Sigma st A,B are_independent_respect_to P holds
([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P
let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma st A,B are_independent_respect_to P holds
([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P
let P be Probability of Sigma; :: thesis: ( A,B are_independent_respect_to P implies ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P )
assume A,B are_independent_respect_to P ; :: thesis: ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P
then A,([#] Sigma) \ B are_independent_respect_to P by Th25;
then ([#] Sigma) \ B,A are_independent_respect_to P ;
then ([#] Sigma) \ B,([#] Sigma) \ A are_independent_respect_to P by Th25;
hence ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P ; :: thesis: verum