let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for P being Probability of Sigma

for B being non empty Subset of Sigma

for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds

sigma A c= Indep (B,P)

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma

for B being non empty Subset of Sigma

for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds

sigma A c= Indep (B,P)

let P be Probability of Sigma; :: thesis: for B being non empty Subset of Sigma

for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds

sigma A c= Indep (B,P)

let B be non empty Subset of Sigma; :: thesis: for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds

sigma A c= Indep (B,P)

reconsider Indp = Indep (B,P) as Dynkin_System of Omega by Th5;

let A be Subset-Family of Omega; :: thesis: ( A is intersection_stable & A c= Indep (B,P) implies sigma A c= Indep (B,P) )

assume ( A is intersection_stable & A c= Indep (B,P) ) ; :: thesis: sigma A c= Indep (B,P)

then sigma A c= Indp by DYNKIN:24;

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

for P being Probability of Sigma

for B being non empty Subset of Sigma

for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds

sigma A c= Indep (B,P)

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma

for B being non empty Subset of Sigma

for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds

sigma A c= Indep (B,P)

let P be Probability of Sigma; :: thesis: for B being non empty Subset of Sigma

for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds

sigma A c= Indep (B,P)

let B be non empty Subset of Sigma; :: thesis: for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds

sigma A c= Indep (B,P)

reconsider Indp = Indep (B,P) as Dynkin_System of Omega by Th5;

let A be Subset-Family of Omega; :: thesis: ( A is intersection_stable & A c= Indep (B,P) implies sigma A c= Indep (B,P) )

assume ( A is intersection_stable & A c= Indep (B,P) ) ; :: thesis: sigma A c= Indep (B,P)

then sigma A c= Indp by DYNKIN:24;

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