let Omega be non empty set ; :: thesis: 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)

let Sigma be SigmaField of Omega; :: thesis: 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)

let P be Probability of Sigma; :: thesis: 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)

let A be Subset-Family of Omega; :: thesis: ( A is non empty Subset of Sigma & A is intersection_stable implies 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) )

assume A is non empty Subset of Sigma ; :: thesis: ( not A is intersection_stable or 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) )

then reconsider sA = sigma A as non empty Subset of Sigma by PROB_1:def 9;

assume A1: A is intersection_stable ; :: thesis: 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)

let B be non empty Subset of Sigma; :: thesis: ( B is intersection_stable & A c= Indep (B,P) implies 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) )

assume A2: B is intersection_stable ; :: thesis: ( not A c= Indep (B,P) or 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) )

assume A c= Indep (B,P) ; :: thesis: 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)

then A3: sigma A c= Indep (B,P) by A1, Th6;

let D be Subset-Family of Omega; :: thesis: for sB being non empty Subset of Sigma st D = B & sigma D = sB holds

sigma A c= Indep (sB,P)

let sB be non empty Subset of Sigma; :: thesis: ( D = B & sigma D = sB implies sigma A c= Indep (sB,P) )

assume A4: ( D = B & sigma D = sB ) ; :: thesis: sigma A c= Indep (sB,P)

reconsider B = B as Subset-Family of Omega by XBOOLE_1:1;

B c= Indep (sA,P) by A3, Th8;

then sigma B c= Indep (sA,P) by A2, Th6;

hence sigma A c= Indep (sB,P) by A4, Th8; :: thesis: verum

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)

let Sigma be SigmaField of Omega; :: thesis: 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)

let P be Probability of Sigma; :: thesis: 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)

let A be Subset-Family of Omega; :: thesis: ( A is non empty Subset of Sigma & A is intersection_stable implies 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) )

assume A is non empty Subset of Sigma ; :: thesis: ( not A is intersection_stable or 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) )

then reconsider sA = sigma A as non empty Subset of Sigma by PROB_1:def 9;

assume A1: A is intersection_stable ; :: thesis: 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)

let B be non empty Subset of Sigma; :: thesis: ( B is intersection_stable & A c= Indep (B,P) implies 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) )

assume A2: B is intersection_stable ; :: thesis: ( not A c= Indep (B,P) or 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) )

assume A c= Indep (B,P) ; :: thesis: 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)

then A3: sigma A c= Indep (B,P) by A1, Th6;

let D be Subset-Family of Omega; :: thesis: for sB being non empty Subset of Sigma st D = B & sigma D = sB holds

sigma A c= Indep (sB,P)

let sB be non empty Subset of Sigma; :: thesis: ( D = B & sigma D = sB implies sigma A c= Indep (sB,P) )

assume A4: ( D = B & sigma D = sB ) ; :: thesis: sigma A c= Indep (sB,P)

reconsider B = B as Subset-Family of Omega by XBOOLE_1:1;

B c= Indep (sA,P) by A3, Th8;

then sigma B c= Indep (sA,P) by A2, Th6;

hence sigma A c= Indep (sB,P) by A4, Th8; :: thesis: verum