let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being non empty Subset of Sigma holds
( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P )
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A, B being non empty Subset of Sigma holds
( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P )
let P be Probability of Sigma; :: thesis: for A, B being non empty Subset of Sigma holds
( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P )
let A, B be non empty Subset of Sigma; :: thesis: ( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P )

A1: now :: thesis: ( ( for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P ) implies A c= Indep (B,P) )

assume A2: for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P ; :: thesis: A c= Indep (B,P)
thus A c= Indep (B,P) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Indep (B,P) )
assume A3: x in A ; :: thesis: x in Indep (B,P)
then reconsider x = x as Event of Sigma ;
for b being Element of B holds P . (x /\ b) = (P . x) * (P . b) by A2, A3, PROB_2:def 4;
hence x in Indep (B,P) by Def1; :: thesis: verum

end;

end;

now :: thesis: ( A c= Indep (B,P) implies for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P )

assume A4: A c= Indep (B,P) ; :: thesis: for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P
thus for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P :: thesis: verum

proof

let p, q be Event of Sigma; :: thesis: ( p in A & q in B implies p,q are_independent_respect_to P )
assume that
A5: p in A and
A6: q in B ; :: thesis: p,q are_independent_respect_to P
reconsider q = q as Element of B by A6;
reconsider p = p as Element of Sigma ;
P . (p /\ q) = (P . p) * (P . q) by A4, A5, Def1;
hence p,q are_independent_respect_to P by PROB_2:def 4; :: thesis: verum

end;

end;

hence ( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P ) by A1; :: thesis: verum