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 A0: 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 A1: 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 A2: 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 A3: 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 A4: 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 E = E as non empty Subset of Sigma by A0;
reconsider F = F as non empty Subset of Sigma by A2;
A5: E c= Indep F,P by A4, Th5;
reconsider E = E, F = F as Subset-Family of Omega ;
reconsider sF = sigma F, sE = sigma E as non empty Subset of Sigma by PROB_1:def 14;
sigma E c= Indep sF,P by A1, A3, A5, Th7;
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 Th5; :: thesis: verum