let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for E, F being Subset-Family of st E is non empty Subset of & E is intersection_stable & F is non empty Subset of & F is intersection_stable & ( for p, q being Event of Sigma st p in E & q in F holds
p,q are_independent_respect_to P ) holds
for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for E, F being Subset-Family of st E is non empty Subset of & E is intersection_stable & F is non empty Subset of & F is intersection_stable & ( for p, q being Event of Sigma st p in E & q in F holds
p,q are_independent_respect_to P ) holds
for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P
let P be Probability of Sigma; :: thesis: for E, F being Subset-Family of st E is non empty Subset of & E is intersection_stable & F is non empty Subset of & F is intersection_stable & ( for p, q being Event of Sigma st p in E & q in F holds
p,q are_independent_respect_to P ) holds
for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P
let E, F be Subset-Family of ; :: thesis: ( E is non empty Subset of & E is intersection_stable & F is non empty Subset of & F is intersection_stable & ( for p, q being Event of Sigma st p in E & q in F holds
p,q are_independent_respect_to P ) implies for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P )
assume A1: E is non empty Subset of ; :: thesis: ( not E is intersection_stable or not F is non empty Subset of or not F is intersection_stable or ex p, q being Event of Sigma st
( p in E & q in F & not p,q are_independent_respect_to P ) or for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P )
assume A2: E is intersection_stable ; :: thesis: ( not F is non empty Subset of or not F is intersection_stable or ex p, q being Event of Sigma st
( p in E & q in F & not p,q are_independent_respect_to P ) or for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P )
assume A3: F is non empty Subset of ; :: thesis: ( not F is intersection_stable or ex p, q being Event of Sigma st
( p in E & q in F & not p,q are_independent_respect_to P ) or for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P )
assume A4: F is intersection_stable ; :: thesis: ( ex p, q being Event of Sigma st
( p in E & q in F & not p,q are_independent_respect_to P ) or for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P )
assume A5: for p, q being Event of Sigma st p in E & q in F holds
p,q are_independent_respect_to P ; :: thesis: for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P
reconsider F = F as non empty Subset of by A3;
reconsider E = E as non empty Subset of by A1;
A6: E c= Indep F,P by A5, Th7;
reconsider E = E, F = F as Subset-Family of ;
reconsider sF = sigma F, sE = sigma E as non empty Subset of by PROB_1:def 14;
sigma E c= Indep sF,P by A2, A4, A6, Th9;
hence for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P by Th7; :: thesis: verum