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

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