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