let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being non empty Subset of Sigma st A c= Indep B,P holds
B c= Indep A,P
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A, B being non empty Subset of Sigma st A c= Indep B,P holds
B c= Indep A,P
let P be Probability of Sigma; :: thesis: for A, B being non empty Subset of Sigma st A c= Indep B,P holds
B c= Indep A,P
let A, B be non empty Subset of Sigma; :: thesis: ( A c= Indep B,P implies B c= Indep A,P )
assume A0: A c= Indep B,P ; :: thesis: B c= Indep A,P
for q, p being Event of Sigma st q in B & p in A holds
q,p are_independent_respect_to P

proof

let q, p be Event of Sigma; :: thesis: ( q in B & p in A implies q,p are_independent_respect_to P )
assume B0: q in B ; :: thesis: ( not p in A or q,p are_independent_respect_to P )
assume p in A ; :: thesis: q,p are_independent_respect_to P
then p,q are_independent_respect_to P by A0, B0, Th5;
hence q,p are_independent_respect_to P by PROB_2:31; :: thesis: verum

end;

hence B c= Indep A,P by Th5; :: thesis: verum