dynkin.miz

    begin

    reserve Omega,F for non empty set,

f for SetSequence of Omega,

X,A,B for Subset of Omega,

D for non empty Subset-Family of Omega,

n,m for Element of NAT ,

h,x,y,z,u,v,Y,I for set;

    theorem :: DYNKIN:1



     Th1: for f be SetSequence of Omega holds for x holds x in ( rng f) iff ex n st (f . n) = x

    proof

      let f be SetSequence of Omega;

      let x;

       A1:

      now

        assume x in ( rng f);

        then

        consider z be object such that

         A2: z in ( dom f) and

         A3: x = (f . z) by FUNCT_1:def 3;

        reconsider n = z as Element of NAT by A2, FUNCT_2:def 1;

        take n;

        thus (f . n) = x by A3;

      end;

      ( dom f) = NAT by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1:def 3;

    end;



     Lm1: for X be non empty set holds for a,b,c be Element of X holds ((a,b) followed_by c) is sequence of X;

    definition

      let Omega be non empty set;

      let a,b,c be Subset of Omega;

      :: original: followed_by

      redefine

      func (a,b) followed_by c -> SetSequence of Omega ;

      coherence

      proof

        thus ((a,b) followed_by c) is SetSequence of Omega;

      end;

    end

    ::$Canceled

    theorem :: DYNKIN:3



     Th2: for a,b be set holds ( Union ((a,b) followed_by {} )) = (a \/ b)

    proof

      let a,b be set;

      ( rng ((a,b) followed_by {} )) = {a, b, {} } by FUNCT_7: 127;



      hence ( Union ((a,b) followed_by {} )) = ( union {a, b}) by MEASURE1: 1

      .= (a \/ b) by ZFMISC_1: 75;

    end;

    definition

      let Omega be non empty set;

      let f be SetSequence of Omega;

      let X be Subset of Omega;

      :: DYNKIN:def1

      func seqIntersection (X,f) -> SetSequence of Omega means

      : Def1: for n holds (it . n) = (X /\ (f . n));

      existence

      proof

        deffunc F( Element of NAT ) = (X /\ (f . $1));

        consider g be sequence of ( bool Omega) such that

         A1: for x be Element of NAT holds (g . x) = F(x) from FUNCT_2:sch 4;

        take g;

        let n;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let i1,i2 be SetSequence of Omega;

        assume

         A2: for n holds (i1 . n) = (X /\ (f . n));

        assume

         A3: for n holds (i2 . n) = (X /\ (f . n));

        now

          let n be Element of NAT ;

          (i1 . n) = (X /\ (f . n)) by A2;

          hence (i1 . n) = (i2 . n) by A3;

        end;

        hence i1 = i2 by FUNCT_2: 63;

      end;

    end

    begin

    definition

      let Omega;

      let f;

      :: original: disjoint_valued

      redefine

      :: DYNKIN:def2

      attr f is disjoint_valued means n < m implies (f . n) misses (f . m);

      compatibility

      proof

        thus f is disjoint_valued implies for n, m holds (n < m implies (f . n) misses (f . m)) by PROB_2:def 2;

        assume

         A1: n < m implies (f . n) misses (f . m);

        now

          let x,y be object;

          assume

           A2: x <> y;

          per cases ;

            suppose x in ( dom f) & y in ( dom f);

            then

            reconsider n = x, m = y as Element of NAT by FUNCT_2:def 1;

            n < m or n > m by A2, XXREAL_0: 1;

            hence (f . x) misses (f . y) by A1;

          end;

            suppose not (x in ( dom f) & y in ( dom f));

            then (f . x) = {} or (f . y) = {} by FUNCT_1:def 2;

            hence (f . x) misses (f . y) by XBOOLE_1: 65;

          end;

        end;

        hence thesis by PROB_2:def 2;

      end;

    end

    theorem :: DYNKIN:4



     Th3: for Y be non empty set holds for x holds x c= ( meet Y) iff for y be Element of Y holds x c= y

    proof

      let Y be non empty set;

      let x;

      thus x c= ( meet Y) implies for y be Element of Y holds x c= y by SETFAM_1:def 1;

      assume

       A1: for y be Element of Y holds x c= y;

      let z be object;

      assume

       A2: z in x;

      now

        let u;

        assume u in Y;

        then x c= u by A1;

        hence z in u by A2;

      end;

      hence thesis by SETFAM_1:def 1;

    end;

    notation

      let x be set;

      synonym x is intersection_stable for x is cap-closed;

    end

    definition

      let Omega be non empty set;

      let f be SetSequence of Omega;

      let n be Nat;

      :: DYNKIN:def3

      func disjointify (f,n) -> Subset of Omega equals ((f . n) \ ( union ( rng (f | n))));

      coherence ;

    end

    definition

      let Omega be non empty set;

      let g be SetSequence of Omega;

      :: DYNKIN:def4

      func disjointify (g) -> SetSequence of Omega means

      : Def4: for n be Nat holds (it . n) = ( disjointify (g,n));

      existence

      proof

        deffunc F( Nat) = ( disjointify (g,$1));

        consider f be sequence of ( bool Omega) such that

         A1: for x be Element of NAT holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let i1,i2 be SetSequence of Omega;

        assume

         A2: for n be Nat holds (i1 . n) = ( disjointify (g,n));

        assume

         A3: for n be Nat holds (i2 . n) = ( disjointify (g,n));

        now

          let n be Element of NAT ;

          (i1 . n) = ( disjointify (g,n)) by A2;

          hence (i1 . n) = (i2 . n) by A3;

        end;

        hence i1 = i2 by FUNCT_2: 63;

      end;

    end

    theorem :: DYNKIN:5



     Th4: for n be Nat holds (( disjointify f) . n) = ((f . n) \ ( union ( rng (f | n))))

    proof

      let n be Nat;

      (( disjointify f) . n) = ( disjointify (f,n)) by Def4;

      hence thesis;

    end;

    theorem :: DYNKIN:6



     Th5: for f be SetSequence of Omega holds ( disjointify f) is disjoint_valued

    proof

      let f be SetSequence of Omega;

      now

        let n, m;

        assume n < m;

        then

         A1: n in ( Segm m) by NAT_1: 44;

        ( dom f) = NAT by FUNCT_2:def 1;

        then ( dom (f | m)) = (m /\ NAT ) by RELAT_1: 61;

        then n in ( dom (f | m)) by A1, XBOOLE_0:def 4;

        then

         A2: ((f | m) . n) in ( rng (f | m)) by FUNCT_1:def 3;

        ((f | m) . n) = (f . n) by A1, FUNCT_1: 49;

        then (f . n) misses ((f . m) \ ( union ( rng (f | m)))) by A2, XBOOLE_1: 85, ZFMISC_1: 74;

        then

         A3: (f . n) misses (( disjointify f) . m) by Th4;

        ((f . n) \ ( union ( rng (f | n)))) c= (f . n) by XBOOLE_1: 36;

        then (( disjointify f) . n) c= (f . n) by Th4;

        hence (( disjointify f) . n) misses (( disjointify f) . m) by A3, XBOOLE_1: 63;

      end;

      hence thesis;

    end;

    theorem :: DYNKIN:7



     Th6: for f be SetSequence of Omega holds ( union ( rng ( disjointify f))) = ( union ( rng f))

    proof

      let f be SetSequence of Omega;



       A1: ( dom f) = NAT by FUNCT_2:def 1;



       A2: ( dom ( disjointify f)) = NAT by FUNCT_2:def 1;

      now

        let x be object;

        defpred P[ Nat] means x in (f . $1);

        assume x in ( union ( rng f));

        then

        consider y such that

         A3: x in y and

         A4: y in ( rng f) by TARSKI:def 4;

        consider z be object such that

         A5: z in ( dom f) and

         A6: y = (f . z) by A4, FUNCT_1:def 3;

        reconsider n = z as Element of NAT by A5, FUNCT_2:def 1;



         A7: ex k be Nat st P[k]

        proof

          take n;

          thus thesis by A3, A6;

        end;

        consider k be Nat such that

         A8: P[k] & for m be Nat st P[m] holds k <= m from NAT_1:sch 5( A7);

        now

          assume x in ( union ( rng (f | k)));

          then

          consider y such that

           A9: x in y and

           A10: y in ( rng (f | k)) by TARSKI:def 4;

          consider z be object such that

           A11: z in ( dom (f | k)) and

           A12: y = ((f | k) . z) by A10, FUNCT_1:def 3;

          ( dom (f | k)) c= NAT by A1, RELAT_1: 60;

          then

          reconsider n = z as Element of NAT by A11;

          ( dom (f | k)) c= ( Segm k) by RELAT_1: 58;

          then n < k & y = (f . n) by A11, A12, FUNCT_1: 49, NAT_1: 44;

          hence contradiction by A8, A9;

        end;

        then x in ((f . k) \ ( union ( rng (f | k)))) by A8, XBOOLE_0:def 5;

        then

         A13: x in (( disjointify f) . k) by Th4;

        k in NAT by ORDINAL1:def 12;

        then (( disjointify f) . k) in ( rng ( disjointify f)) by A2, FUNCT_1:def 3;

        hence x in ( union ( rng ( disjointify f))) by A13, TARSKI:def 4;

      end;

      then

       A14: ( union ( rng f)) c= ( union ( rng ( disjointify f)));

      now

        let x be object;

        assume x in ( union ( rng ( disjointify f)));

        then

        consider y such that

         A15: x in y and

         A16: y in ( rng ( disjointify f)) by TARSKI:def 4;

        consider z be object such that

         A17: z in ( dom ( disjointify f)) and

         A18: y = (( disjointify f) . z) by A16, FUNCT_1:def 3;

        reconsider n = z as Element of NAT by A17, FUNCT_2:def 1;



         A19: ((f . n) \ ( union ( rng (f | n)))) c= (f . n) & (f . n) in ( rng f) by A1, FUNCT_1:def 3, XBOOLE_1: 36;

        x in ((f . n) \ ( union ( rng (f | n)))) by A15, A18, Th4;

        hence x in ( union ( rng f)) by A19, TARSKI:def 4;

      end;

      then ( union ( rng ( disjointify f))) c= ( union ( rng f));

      hence thesis by A14, XBOOLE_0:def 10;

    end;

    theorem :: DYNKIN:8



     Th7: for x,y be Subset of Omega st x misses y holds ((x,y) followed_by ( {} Omega)) is disjoint_valued

    proof

      let x,y be Subset of Omega such that

       A1: x misses y;

      reconsider r = ((x,y) followed_by ( {} Omega)) as sequence of ( bool Omega);

      now

        let n, m;



         A2: m > 1 implies (r . m) = {} by FUNCT_7: 124;

        assume

         A3: n < m;

         A4:

        now

          assume

           A5: m = 0 or m = 1;

          ( 0 + 1) = 1;

          then n <= 0 by A3, A5, NAT_1: 13;

          hence n = 0 & m = 1 by A3, A5, NAT_1: 3;

        end;

        (r . 0 ) = x by FUNCT_7: 122;

        hence (r . n) misses (r . m) by A1, A4, A2, FUNCT_7: 123, NAT_1: 25, XBOOLE_1: 65;

      end;

      hence thesis;

    end;

    theorem :: DYNKIN:9



     Th8: for f be SetSequence of Omega holds f is disjoint_valued implies for X be Subset of Omega holds ( seqIntersection (X,f)) is disjoint_valued

    proof

      let f be SetSequence of Omega;

      assume

       A1: f is disjoint_valued;

      let X be Subset of Omega;

      for n, m holds n < m implies (( seqIntersection (X,f)) . n) misses (( seqIntersection (X,f)) . m)

      proof

        let n, m;

        assume n < m;

        then (f . n) misses (f . m) by A1;

        then

         A2: (X /\ (f . n)) misses (f . m) by XBOOLE_1: 74;

        (( seqIntersection (X,f)) . n) = (X /\ (f . n)) & (( seqIntersection (X,f)) . m) = (X /\ (f . m)) by Def1;

        hence thesis by A2, XBOOLE_1: 74;

      end;

      hence thesis;

    end;

    theorem :: DYNKIN:10



     Th9: for f be SetSequence of Omega holds for X be Subset of Omega holds (X /\ ( Union f)) = ( Union ( seqIntersection (X,f)))

    proof

      let f be SetSequence of Omega;

      let X be Subset of Omega;



       A1: ( dom f) = NAT by FUNCT_2:def 1;

      now

        reconsider g = ( seqIntersection (X,f)) as SetSequence of Omega;

        let z be object;

        assume z in ( Union ( seqIntersection (X,f)));

        then

        consider u such that

         A2: z in u and

         A3: u in ( rng g) by TARSKI:def 4;

        consider v be object such that

         A4: v in ( dom g) and

         A5: u = (g . v) by A3, FUNCT_1:def 3;

        reconsider n = v as Element of NAT by A4, FUNCT_2:def 1;



         A6: z in (X /\ (f . n)) by A2, A5, Def1;

        then

         A7: z in X by XBOOLE_0:def 4;



         A8: (f . n) in ( rng f) by A1, FUNCT_1:def 3;

        z in (f . n) by A6, XBOOLE_0:def 4;

        then z in ( Union f) by A8, TARSKI:def 4;

        hence z in (X /\ ( Union f)) by A7, XBOOLE_0:def 4;

      end;

      then

       A9: ( Union ( seqIntersection (X,f))) c= (X /\ ( Union f));



       A10: ( dom ( seqIntersection (X,f))) = NAT by FUNCT_2:def 1;

      now

        let z be object;

        assume

         A11: z in (X /\ ( Union f));

        then z in ( union ( rng f)) by XBOOLE_0:def 4;

        then

        consider u such that

         A12: z in u and

         A13: u in ( rng f) by TARSKI:def 4;

        consider v be object such that

         A14: v in ( dom f) and

         A15: u = (f . v) by A13, FUNCT_1:def 3;

        reconsider n = v as Element of NAT by A14, FUNCT_2:def 1;

        (X /\ (f . n)) = (( seqIntersection (X,f)) . n) by Def1;

        then

         A16: (X /\ (f . n)) in ( rng ( seqIntersection (X,f))) by A10, FUNCT_1:def 3;

        z in X by A11, XBOOLE_0:def 4;

        then z in (X /\ (f . n)) by A12, A15, XBOOLE_0:def 4;

        hence z in ( Union ( seqIntersection (X,f))) by A16, TARSKI:def 4;

      end;

      then (X /\ ( Union f)) c= ( Union ( seqIntersection (X,f)));

      hence thesis by A9, XBOOLE_0:def 10;

    end;

    begin

    definition

      let Omega;

      :: DYNKIN:def5

      mode Dynkin_System of Omega -> Subset-Family of Omega means

      : Def5: (for f holds ( rng f) c= it & f is disjoint_valued implies ( Union f) in it ) & (for X holds X in it implies (X ` ) in it ) & {} in it ;

      existence

      proof

        reconsider D = ( bool Omega) as non empty Subset-Family of Omega;

        take D;

         {} c= Omega;

        hence thesis;

      end;

    end

    registration

      let Omega;

      cluster -> non empty for Dynkin_System of Omega;

      coherence by Def5;

    end

    theorem :: DYNKIN:11



     Th10: ( bool Omega) is Dynkin_System of Omega

    proof



       A1: {} c= Omega & ( bool Omega) c= ( bool Omega);

      (for f holds ( rng f) c= ( bool Omega) & f is disjoint_valued implies ( Union f) in ( bool Omega)) & for X holds X in ( bool Omega) implies (X ` ) in ( bool Omega);

      hence thesis by A1, Def5;

    end;

    theorem :: DYNKIN:12



     Th11: (for Y st Y in F holds Y is Dynkin_System of Omega) implies ( meet F) is Dynkin_System of Omega

    proof

      assume

       A1: for Y st Y in F holds Y is Dynkin_System of Omega;

      now

        let Y;

        assume Y in F;

        then Y is Dynkin_System of Omega by A1;

        hence {} in Y by Def5;

      end;

      then

       A2: {} in ( meet F) by SETFAM_1:def 1;

       A3:

      now

        let f;

        assume that

         A4: ( rng f) c= ( meet F) and

         A5: f is disjoint_valued;

        now

          let Y such that

           A6: Y in F;

          ( meet F) c= Y by A6, SETFAM_1: 3;

          then

           A7: ( rng f) c= Y by A4;

          Y is Dynkin_System of Omega by A1, A6;

          hence ( Union f) in Y by A5, A7, Def5;

        end;

        hence ( Union f) in ( meet F) by SETFAM_1:def 1;

      end;

       A8:

      now

        let X;

        assume

         A9: X in ( meet F);

        for Y st Y in F holds (X ` ) in Y

        proof

          let Y;

          assume Y in F;

          then Y is Dynkin_System of Omega & ( meet F) c= Y by A1, SETFAM_1: 3;

          hence thesis by A9, Def5;

        end;

        hence (X ` ) in ( meet F) by SETFAM_1:def 1;

      end;

      set Y = the Element of F;



       A10: ( meet F) c= Y by SETFAM_1: 3;

      Y is Dynkin_System of Omega by A1;

      then ( meet F) is Subset-Family of Omega by A10, XBOOLE_1: 1;

      hence thesis by A3, A8, A2, Def5;

    end;

    theorem :: DYNKIN:13



     Th12: D is Dynkin_System of Omega & D is intersection_stable implies (A in D & B in D implies (A \ B) in D)

    proof

      assume that

       A1: D is Dynkin_System of Omega and

       A2: D is intersection_stable;

      assume that

       A3: A in D and

       A4: B in D;

      (B ` ) in D by A1, A4, Def5;

      then (A /\ (B ` )) in D by A2, A3, FINSUB_1:def 2;

      hence thesis by SUBSET_1: 13;

    end;

    theorem :: DYNKIN:14



     Th13: D is Dynkin_System of Omega & D is intersection_stable implies (A in D & B in D implies (A \/ B) in D)

    proof

      assume that

       A1: D is Dynkin_System of Omega and

       A2: D is intersection_stable;

      assume A in D & B in D;

      then (A ` ) in D & (B ` ) in D by A1, Def5;

      then ((A ` ) /\ (B ` )) in D by A2, FINSUB_1:def 2;

      then ((A \/ B) ` ) in D by XBOOLE_1: 53;

      then (((A \/ B) ` ) ` ) in D by A1, Def5;

      hence thesis;

    end;

    theorem :: DYNKIN:15



     Th14: D is Dynkin_System of Omega & D is intersection_stable implies for x be finite set holds x c= D implies ( union x) in D

    proof

      assume that

       A1: D is Dynkin_System of Omega and

       A2: D is intersection_stable;

      defpred P[ set] means ( union $1) in D;

      let x be finite set;

      assume

       A3: x c= D;



       A4: for y,b be set st y in x & b c= x & P[b] holds P[(b \/ {y})]

      proof

        let y,b be set such that

         A5: y in x and b c= x and

         A6: ( union b) in D;

        y in D by A3, A5;

        then

        reconsider y1 = y as Subset of Omega;

        reconsider unionb = ( union b) as Subset of Omega by A6;

        ( union {y}) = y & (unionb \/ y1) in D by A1, A2, A3, A5, A6, Th13, ZFMISC_1: 25;

        hence thesis by ZFMISC_1: 78;

      end;



       A7: x is finite;



       A8: P[ {} ] by A1, Def5, ZFMISC_1: 2;

      thus P[x] from FINSET_1:sch 2( A7, A8, A4);

    end;

    theorem :: DYNKIN:16



     Th15: D is Dynkin_System of Omega & D is intersection_stable implies for f be SetSequence of Omega holds ( rng f) c= D implies ( rng ( disjointify f)) c= D

    proof

      assume

       A1: D is Dynkin_System of Omega & D is intersection_stable;

      let f be SetSequence of Omega;

      assume

       A2: ( rng f) c= D;



       A3: for n holds (( disjointify f) . n) in D

      proof

        let n;



         A4: ( rng (f | n)) c= ( rng f) by RELAT_1: 70;



         A5: ( union ( rng (f | n))) in D by A1, A2, A4, Th14, XBOOLE_1: 1;

        then

        reconsider urf = ( union ( rng (f | n))) as Subset of Omega;

        ( dom f) = NAT by FUNCT_2:def 1;

        then (f . n) in ( rng f) by FUNCT_1:def 3;

        then ((f . n) \ urf) in D by A1, A2, A5, Th12;

        hence thesis by Th4;

      end;

      let y be object;

      assume y in ( rng ( disjointify f));

      then

      consider x be object such that

       A6: x in ( dom ( disjointify f)) and

       A7: y = (( disjointify f) . x) by FUNCT_1:def 3;

      reconsider n = x as Element of NAT by A6, FUNCT_2:def 1;

      y = (( disjointify f) . n) by A7;

      hence y in D by A3;

    end;

    theorem :: DYNKIN:17



     Th16: D is Dynkin_System of Omega & D is intersection_stable implies for f be SetSequence of Omega holds ( rng f) c= D implies ( union ( rng f)) in D

    proof

      assume that

       A1: D is Dynkin_System of Omega and

       A2: D is intersection_stable;

      let f be SetSequence of Omega;

      assume ( rng f) c= 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 thesis by Th6;

    end;

    theorem :: DYNKIN:18



     Th17: for D be Dynkin_System of Omega holds for x,y be Element of D holds x misses y implies (x \/ y) in D

    proof

      let D be Dynkin_System of Omega;

      reconsider e = {} as Element of D by Def5;

      let x,y be Element of D;

      reconsider x1 = x as Subset of Omega;

      reconsider y1 = y as Subset of Omega;

      reconsider r = ((x1,y1) followed_by ( {} Omega)) as SetSequence of Omega;

      ((x,y) followed_by e) is sequence of D by Lm1;

      then

       A1: ( rng r) c= D by RELAT_1:def 19;

      assume x misses y;

      then r is disjoint_valued by Th7;

      then ( Union r) in D by A1, Def5;

      hence thesis by Th2;

    end;

    theorem :: DYNKIN:19



     Th18: for D be Dynkin_System of Omega holds for x,y be Element of D holds x c= y implies (y \ x) in D

    proof

      let D be Dynkin_System of Omega;

      let x,y be Element of D;



       A1: ((x \/ (y ` )) ` ) = ((x ` ) /\ ((y ` ) ` )) by XBOOLE_1: 53

      .= (y \ x) by SUBSET_1: 13;

      assume x c= y;

      then x c= ((y ` ) ` );

      then

       A2: x misses (y ` ) by SUBSET_1: 23;

      (y ` ) in D by Def5;

      then (x \/ (y ` )) in D by A2, Th17;

      hence thesis by A1, Def5;

    end;

    begin

    theorem :: DYNKIN:20



     Th19: D is Dynkin_System of Omega & D is intersection_stable implies D is SigmaField of Omega

    proof

      assume that

       A1: D is Dynkin_System of Omega and

       A2: D is intersection_stable;



       A3: for f st ( rng f) c= D holds ( Intersection f) in D

      proof

        let f such that

         A4: ( rng f) c= D;



         A5: for n holds ((f . n) ` ) in D

        proof

          let n;

          (f . n) in ( rng f) by NAT_1: 51;

          hence thesis by A1, A4, Def5;

        end;



         A6: for n holds (( Complement f) . n) in D

        proof

          let n;

          (( Complement f) . n) = ((f . n) ` ) by PROB_1:def 2;

          hence thesis by A5;

        end;

        for x be object st x in ( rng ( Complement f)) holds x in D

        proof

          let x be object;

          assume x in ( rng ( Complement f));

          then

          consider z be object such that

           A7: z in ( dom ( Complement f)) and

           A8: x = (( Complement f) . z) by FUNCT_1:def 3;

          reconsider n = z as Element of NAT by A7, FUNCT_2:def 1;

          x = (( Complement f) . n) by A8;

          hence thesis by A6;

        end;

        then ( rng ( Complement f)) c= D;

        then ( Union ( Complement f)) in D by A1, A2, Th16;

        then (( Union ( Complement f)) ` ) in D by A1, Def5;

        hence thesis by PROB_1:def 3;

      end;

      for X st X in D holds (X ` ) in D by A1, Def5;

      hence thesis by A3, PROB_1: 15;

    end;

    definition

      let Omega be non empty set;

      let E be Subset-Family of Omega;

      :: DYNKIN:def6

      func generated_Dynkin_System (E) -> Dynkin_System of Omega means

      : Def6: E c= it & for D be Dynkin_System of Omega holds (E c= D implies it c= D);

      existence

      proof

        defpred P[ set] means $1 is Dynkin_System of Omega & E c= $1;

        consider Y such that

         A1: for x holds x in Y iff x in ( bool ( bool Omega)) & P[x] from XFAMILY:sch 1;

        ( bool Omega) is Dynkin_System of Omega by Th10;

        then

        reconsider Y as non empty set by A1;

        for z st z in Y holds z is Dynkin_System of Omega by A1;

        then

        reconsider I = ( meet Y) as Dynkin_System of Omega by Th11;

        take I;

        for y be Element of Y holds E c= y by A1;

        hence E c= I by Th3;

        let D be Dynkin_System of Omega;

        assume E c= D;

        then D in Y by A1;

        hence thesis by SETFAM_1: 3;

      end;

      uniqueness

      proof

        let I1,I2 be Dynkin_System of Omega;

        assume

         A2: E c= I1 & for D be Dynkin_System of Omega holds (E c= D implies I1 c= D);

        assume E c= I2 & for D be Dynkin_System of Omega holds (E c= D implies I2 c= D);

        then I1 c= I2 & I2 c= I1 by A2;

        hence thesis by XBOOLE_0:def 10;

      end;

    end

    definition

      let Omega be non empty set;

      let G be set;

      let X be Subset of Omega;

      :: DYNKIN:def7

      func DynSys (X,G) -> Subset-Family of Omega means

      : Def7: for A be Subset of Omega holds A in it iff (A /\ X) in G;

      existence

      proof

        defpred P[ set] means ($1 /\ X) in G;

        consider I such that

         A1: for x holds x in I iff x in ( bool Omega) & P[x] from XFAMILY:sch 1;

        for x be object holds x in I implies x in ( bool Omega) by A1;

        then

        reconsider I as Subset-Family of Omega by TARSKI:def 3;

        take I;

        let A be Subset of Omega;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let I1,I2 be Subset-Family of Omega;

        assume

         A2: for A be Subset of Omega holds A in I1 iff (A /\ X) in G;

        assume

         A3: for A be Subset of Omega holds A in I2 iff (A /\ X) in G;

        now

          let A be Subset of Omega;

          A in I1 iff (A /\ X) in G by A2;

          hence A in I1 iff A in I2 by A3;

        end;

        hence thesis by SUBSET_1: 3;

      end;

    end

    definition

      let Omega be non empty set;

      let G be Dynkin_System of Omega;

      let X be Element of G;

      :: original: DynSys

      redefine

      func DynSys (X,G) -> Dynkin_System of Omega ;

      coherence

      proof



         A1: for f be SetSequence of Omega holds ( rng f) c= ( DynSys (X,G)) & f is disjoint_valued implies ( Union f) in ( DynSys (X,G))

        proof

          reconsider X1 = X as Subset of Omega;

          let f be SetSequence of Omega;

          assume that

           A2: ( rng f) c= ( DynSys (X,G)) and

           A3: f is disjoint_valued;

          now

            let x be object;

            assume x in ( rng ( seqIntersection (X1,f)));

            then

            consider n such that

             A4: x = (( seqIntersection (X1,f)) . n) by Th1;



             A5: (f . n) in ( rng f) by Th1;

            x = (X /\ (f . n)) by A4, Def1;

            hence x in G by A2, A5, Def7;

          end;

          then

           A6: ( rng ( seqIntersection (X1,f))) c= G;

          ( seqIntersection (X,f)) is disjoint_valued by A3, Th8;

          then ( Union ( seqIntersection (X1,f))) in G by A6, Def5;

          then (X /\ ( Union f)) in G by Th9;

          hence thesis by Def7;

        end;



         A7: for A be Subset of Omega holds A in ( DynSys (X,G)) implies (A ` ) in ( DynSys (X,G))

        proof

          let A be Subset of Omega;

          X misses (X ` ) by XBOOLE_1: 79;

          then

           A8: (X /\ (X ` )) = {} by XBOOLE_0:def 7;

          assume A in ( DynSys (X,G));

          then (X /\ A) in G by Def7;

          then

           A9: (X \ (X /\ A)) in G by Th18, XBOOLE_1: 17;

          (X \ (X /\ A)) = (X /\ ((X /\ A) ` )) by SUBSET_1: 13

          .= (X /\ ((X ` ) \/ (A ` ))) by XBOOLE_1: 54

          .= ((X /\ (X ` )) \/ (X /\ (A ` ))) by XBOOLE_1: 23

          .= (X /\ (A ` )) by A8;

          hence thesis by A9, Def7;

        end;

        ( {} /\ X) = {} & {} in G by Def5;

        then {} in ( DynSys (X,G)) by Def7;

        hence thesis by A1, A7, Def5;

      end;

    end

    theorem :: DYNKIN:21



     Th20: for E be Subset-Family of Omega holds for X,Y be Subset of Omega holds X in E & Y in ( generated_Dynkin_System E) & E is intersection_stable implies (X /\ Y) in ( generated_Dynkin_System E)

    proof

      let E be Subset-Family of Omega;

      let X,Y be Subset of Omega;

      assume that

       A1: X in E and

       A2: Y in ( generated_Dynkin_System E) and

       A3: E is intersection_stable;

      reconsider G = ( generated_Dynkin_System E) as Dynkin_System of Omega;

      E c= ( generated_Dynkin_System E) by Def6;

      then

      reconsider X as Element of G by A1;

      for x be object holds x in E implies x in ( DynSys (X,G))

      proof

        let x be object;

        assume

         A4: x in E;

        then

        reconsider x as Subset of Omega;



         A5: E c= G by Def6;

        (x /\ X) in E by A1, A3, A4, FINSUB_1:def 2;

        hence thesis by A5, Def7;

      end;

      then E c= ( DynSys (X,G));

      then ( generated_Dynkin_System E) c= ( DynSys (X,G)) by Def6;

      hence thesis by A2, Def7;

    end;

    theorem :: DYNKIN:22



     Th21: for E be Subset-Family of Omega holds for X,Y be Subset of Omega holds X in ( generated_Dynkin_System E) & Y in ( generated_Dynkin_System E) & E is intersection_stable implies (X /\ Y) in ( generated_Dynkin_System E)

    proof

      let E be Subset-Family of Omega;

      let X,Y be Subset of Omega;

      assume that

       A1: X in ( generated_Dynkin_System E) and

       A2: Y in ( generated_Dynkin_System E) and

       A3: E is intersection_stable;

      reconsider G = ( generated_Dynkin_System E) as Dynkin_System of Omega;

      defpred P[ set] means ex X be Element of G st $1 = ( DynSys (X,G));

      consider h such that

       A4: for x holds x in h iff x in ( bool ( bool Omega)) & P[x] from XFAMILY:sch 1;



       A5: for Y st Y in h holds Y is Dynkin_System of Omega

      proof

        let Y;

        assume Y in h;

        then ex X be Element of G st Y = ( DynSys (X,G)) by A4;

        hence thesis;

      end;

      h is non empty

      proof

        set X = the Element of G;

        ( DynSys (X,G)) in h by A4;

        hence thesis;

      end;

      then

      reconsider h as non empty set;

      ( DynSys (X,G)) in h by A1, A4;

      then

       A6: ( meet h) c= ( DynSys (X,G)) by SETFAM_1: 3;

      for x be object holds x in E implies x in ( meet h)

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume

         A7: x in E;

        for Y st Y in h holds x in Y

        proof

          let Y;

          assume Y in h;

          then

          consider X be Element of G such that

           A8: Y = ( DynSys (X,G)) by A4;

          (xx /\ X) in G by A3, A7, Th20;

          hence thesis by A7, A8, Def7;

        end;

        hence thesis by SETFAM_1:def 1;

      end;

      then

       A9: E c= ( meet h);

      ( meet h) is Dynkin_System of Omega by A5, Th11;

      then G c= ( meet h) by A9, Def6;

      then G c= ( DynSys (X,G)) by A6;

      hence thesis by A2, Def7;

    end;

    theorem :: DYNKIN:23



     Th22: for E be Subset-Family of Omega st E is intersection_stable holds ( generated_Dynkin_System E) is intersection_stable

    proof

      let E be Subset-Family of Omega such that

       A1: E is intersection_stable;

      reconsider G = ( generated_Dynkin_System E) as Subset-Family of Omega;

      for a,b be set st a in G & b in G holds (a /\ b) in G by A1, Th21;

      hence thesis by FINSUB_1:def 2;

    end;

    ::$Notion-Name

    theorem :: DYNKIN:24

    for E be Subset-Family of Omega st E is intersection_stable holds for D be Dynkin_System of Omega st E c= D holds ( sigma E) c= D

    proof

      let E be Subset-Family of Omega such that

       A1: E is intersection_stable;

      reconsider G = ( generated_Dynkin_System E) as Dynkin_System of Omega;

      G is intersection_stable by A1, Th22;

      then

       A2: G is SigmaField of Omega by Th19;

      let D be Dynkin_System of Omega;

      assume E c= D;

      then

       A3: G c= D by Def6;

      E c= G by Def6;

      then ( sigma E) c= G by A2, PROB_1:def 9;

      hence thesis by A3;

    end;