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 that
A1: D is Dynkin_System of Omega and
A2: 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 A3: rng (disjointify f) c= D by A1, A2, Th15;
disjointify f is disjoint_valued by Th5;
then Union (disjointify f) in D by A1, A3, Def5;
hence union (rng f) in D by Th6; :: thesis: verum