let Omega be non empty set ; 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; 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; 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; 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; ( 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) )
; sigma A c= Indep (B,P)
then
sigma A c= Indp
by DYNKIN:24;
hence
sigma A c= Indep (B,P)
; verum