let Omega be non empty set ; 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; 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; 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; ( 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
; ([#] 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
; verum