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
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 A0: ( A is intersection_stable & A c= Indep B,P ) ; :: thesis: sigma A c= Indep B,P
reconsider Indp = Indep B,P as Dynkin_System of Omega by Th3;
sigma A c= Indp by A0, DYNKIN:27;
hence sigma A c= Indep B,P ; :: thesis: verum