theorem Th9: :: KOLMOG01:9

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Subset-Family of Omega st A is non empty Subset of Sigma & A is intersection_stable holds
for B being non empty Subset of Sigma st B is intersection_stable & A c= Indep (B,P) holds
for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P)