let Omega be non empty set ; for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega
let Sigma be SigmaField of Omega; for P being Probability of Sigma
for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega
let P be Probability of Sigma; for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega
let B be non empty Subset of Sigma; Indep (B,P) is Dynkin_System of Omega
A1:
for b being Element of B holds P . ({} /\ b) = (P . {}) * (P . b)
reconsider Indp = Indep (B,P) as Subset-Family of Omega by XBOOLE_1:1;
{} is Element of Sigma
by PROB_1:22;
then A2:
{} in Indep (B,P)
by A1, Def1;
A3:
for g being SetSequence of Omega st rng g c= Indep (B,P) & g is V71() holds
Union g in Indep (B,P)
for Z being Subset of Omega st Z in Indep (B,P) holds
Z ` in Indep (B,P)
then
Indp is Dynkin_System of Omega
by A2, A3, DYNKIN:def 5;
hence
Indep (B,P) is Dynkin_System of Omega
; verum