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 Omega st E is non empty Subset of Sigma & E is intersection_stable & F is non empty Subset of Sigma & 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 Omega st E is non empty Subset of Sigma & E is intersection_stable & F is non empty Subset of Sigma & 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 Omega st E is non empty Subset of Sigma & E is intersection_stable & F is non empty Subset of Sigma & 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 Omega; :: thesis: ( E is non empty Subset of Sigma & E is intersection_stable & F is non empty Subset of Sigma & 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 Sigma ; :: thesis: ( not E is intersection_stable or not F is non empty Subset of Sigma 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 Sigma 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 Sigma ; :: 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 Sigma by A3;
reconsider E = E as non empty Subset of Sigma by A1;
A6: E c= Indep (F,P) by A5, Th7;
reconsider E = E, F = F as Subset-Family of Omega ;
reconsider sF = sigma F as non empty Subset of Sigma by PROB_1:def 9;
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