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 A0: 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 )
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 A3: 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
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 sA = sigma A as non empty Subset of Sigma by A0, PROB_1:def 14;
A5: sigma A c= Indep B,P by A1, A3, Th4;
reconsider B = B as Subset-Family of Omega by XBOOLE_1:1;
B c= Indep sA,P by A5, Th6;
then sigma B c= Indep sA,P by A2, Th4;
hence sigma A c= Indep sB,P by A4, Th6; :: thesis: verum