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 A1: 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 by A1, Th7, PROB_2:19;

hence B c= Indep (A,P) by Th7; :: thesis: verum

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 A1: 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 by A1, Th7, PROB_2:19;

hence B c= Indep (A,P) by Th7; :: thesis: verum