let Omega be non empty set ; :: thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D
let D be non empty Subset-Family of Omega; :: thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D )
assume A1: ( D is Dynkin_System of Omega & D is intersection_stable ) ; :: thesis: for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D
let f be SetSequence of Omega; :: thesis: ( rng f c= D implies union (rng f) in D )
assume rng f c= D ; :: thesis: union (rng f) in D
then A2: rng (disjointify f) c= D by A1, Th19;
disjointify f is disjoint_valued by Th9;
then Union (disjointify f) in D by A1, A2, Def7;
then union (rng (disjointify f)) in D ;
hence union (rng f) in D by Th10; :: thesis: verum