kurato_2.miz



    begin

    definition

      let T be 1-sorted;

      mode SetSequence of T is SetSequence of the carrier of T;

    end

    begin

    reserve n for Nat;

    registration

      let f be FinSequence of the carrier of ( TOP-REAL 2);

      cluster ( L~ f) -> closed;

      coherence ;

    end

    theorem :: KURATO_2:1

    

     Th1: for x be Point of ( Euclid n), r be Real holds ( Ball (x,r)) is open Subset of ( TOP-REAL n) by TOPREAL3: 8, GOBOARD6: 3;

    theorem :: KURATO_2:2

    

     Th2: for p be Point of ( Euclid n), x,p9 be Point of ( TOP-REAL n), r be Real st p = p9 & x in ( Ball (p,r)) holds |.(x - p9).| < r

    proof

      let p be Point of ( Euclid n), x,p9 be Point of ( TOP-REAL n), r be Real;

      reconsider x9 = x as Point of ( Euclid n) by TOPREAL3: 8;

      assume that

       A1: p = p9 and

       A2: x in ( Ball (p,r));

      ( dist (x9,p)) < r by A2, METRIC_1: 11;

      hence thesis by A1, SPPOL_1: 39;

    end;

    theorem :: KURATO_2:3

    

     Th3: for p be Point of ( Euclid n), x,p9 be Point of ( TOP-REAL n), r be Real st p = p9 & |.(x - p9).| < r holds x in ( Ball (p,r))

    proof

      let p be Point of ( Euclid n), x,p9 be Point of ( TOP-REAL n), r be Real;

      reconsider x9 = x as Point of ( Euclid n) by TOPREAL3: 8;

      assume p = p9 & |.(x - p9).| < r;

      then ( dist (x9,p)) < r by SPPOL_1: 39;

      hence thesis by METRIC_1: 11;

    end;

    theorem :: KURATO_2:4

    for n be Nat, r be Point of ( TOP-REAL n), X be Subset of ( TOP-REAL n) st r in ( Cl X) holds ex seq be Real_Sequence of n st ( rng seq) c= X & seq is convergent & ( lim seq) = r

    proof

      let n be Nat, r be Point of ( TOP-REAL n), X be Subset of ( TOP-REAL n);

      reconsider r9 = r as Point of ( Euclid n) by TOPREAL3: 8;

      defpred P[ object, object] means ex z be Nat st $1 = z & $2 = the Element of (X /\ ( Ball (r9,(1 / (z + 1)))));

      assume

       A1: r in ( Cl X);

       A2:

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider k = x as Nat;

        set n1 = (k + 1);

        set oi = ( Ball (r9,(1 / n1)));

        reconsider oi as open Subset of ( TOP-REAL n) by Th1;

        reconsider u = the Element of (X /\ oi) as object;

        take u;

        ( dist (r9,r9)) < (1 / n1) by METRIC_1: 1;

        then r in oi by METRIC_1: 11;

        then X meets oi by A1, PRE_TOPC: 24;

        then (X /\ oi) is non empty;

        then u in (X /\ oi);

        hence u in the carrier of ( TOP-REAL n);

        thus P[x, u];

      end;

      consider seq be Function such that

       A3: ( dom seq) = NAT & ( rng seq) c= the carrier of ( TOP-REAL n) and

       A4: for x be object st x in NAT holds P[x, (seq . x)] from FUNCT_1:sch 6( A2);

      reconsider seq as Real_Sequence of n by A3, FUNCT_2:def 1, RELSET_1: 4;

      take seq;

      thus ( rng seq) c= X

      proof

        let y be object;

        assume y in ( rng seq);

        then

        consider x be object such that

         A5: x in ( dom seq) and

         A6: (seq . x) = y by FUNCT_1:def 3;

        consider k be Nat such that x = k and

         A7: (seq . x) = the Element of (X /\ ( Ball (r9,(1 / (k + 1))))) by A4, A5;

        set n1 = (k + 1);

        reconsider oi = ( Ball (r9,(1 / n1))) as open Subset of ( TOP-REAL n) by Th1;

        ( dist (r9,r9)) < (1 / n1) by METRIC_1: 1;

        then r in oi by METRIC_1: 11;

        then X meets oi by A1, PRE_TOPC: 24;

        then (X /\ oi) is non empty;

        hence thesis by A6, A7, XBOOLE_0:def 4;

      end;

       A8:

      now

        let p be Real;

        set cp = [/(1 / p)\];

        

         A9: (1 / p) <= cp by INT_1:def 7;

        assume

         A10: 0 < p;

        then

         A11: 0 < cp by INT_1:def 7;

        then

        reconsider cp as Element of NAT by INT_1: 3;

        reconsider cp as Nat;

        take k = cp;

        k < (k + 1) by NAT_1: 13;

        then

         A12: (1 / (k + 1)) < (1 / k) by A11, XREAL_1: 88;

        (1 / (1 / p)) >= (1 / cp) by A10, A9, XREAL_1: 85;

        then

         A13: (1 / (k + 1)) < p by A12, XXREAL_0: 2;

        let m be Nat;

        assume k <= m;

        then

         A14: (k + 1) <= (m + 1) by XREAL_1: 6;

        set m1 = (m + 1);

        (1 / m1) <= (1 / (k + 1)) by A14, XREAL_1: 85;

        then

         A15: (1 / m1) < p by A13, XXREAL_0: 2;

        set oi = ( Ball (r9,(1 / m1)));

        reconsider oi as open Subset of ( TOP-REAL n) by Th1;

        ( dist (r9,r9)) < (1 / m1) by METRIC_1: 1;

        then r in oi by METRIC_1: 11;

        then X meets oi by A1, PRE_TOPC: 24;

        then

         A16: (X /\ oi) is non empty;

        m in NAT by ORDINAL1:def 12;

        then ex m9 be Nat st m9 = m & (seq . m) = the Element of (X /\ ( Ball (r9,(1 / (m9 + 1))))) by A4;

        then (seq . m) in oi by A16, XBOOLE_0:def 4;

        hence |.((seq . m) - r).| < p by A15, Th2, XXREAL_0: 2;

      end;

      hence seq is convergent by TOPRNS_1:def 8;

      hence thesis by A8, TOPRNS_1:def 9;

    end;

    registration

      let M be non empty MetrSpace;

      cluster ( TopSpaceMetr M) -> first-countable;

      coherence by FRECHET: 20;

    end

    

     Lm1: for T be non empty TopSpace, x be Point of T, y be Point of the TopStruct of T, A be set st x = y holds A is Basis of x iff A is Basis of y

    proof

      let T be non empty TopSpace, x be Point of T, y be Point of the TopStruct of T, A be set such that

       A1: x = y;

      thus A is Basis of x implies A is Basis of y

      proof

        assume

         A2: A is Basis of x;

        then

        reconsider A as Subset-Family of the TopStruct of T;

        A is Basis of y

        proof

          A c= the topology of the TopStruct of T by A2, TOPS_2: 64;

          then

           A3: A is open by TOPS_2: 64;

          A is y -quasi_basis by A1, A2, YELLOW_8:def 1, PRE_TOPC: 30;

          hence thesis by A3;

        end;

        hence thesis;

      end;

      assume

       A4: A is Basis of y;

      then

      reconsider A as Subset-Family of T;

      A is Basis of x

      proof

        A c= the topology of T by A4, TOPS_2: 64;

        then

         A5: A is open by TOPS_2: 64;

        A is x -quasi_basis by A1, A4, YELLOW_8:def 1, PRE_TOPC: 30;

        hence thesis by A5;

      end;

      hence thesis;

    end;

    theorem :: KURATO_2:5

    

     Th5: for T be non empty TopSpace holds T is first-countable iff the TopStruct of T is first-countable

    proof

      let T be non empty TopSpace;

      thus T is first-countable implies the TopStruct of T is first-countable

      proof

        assume

         A1: T is first-countable;

        let x be Point of the TopStruct of T;

        reconsider y = x as Point of T;

        consider C be Basis of y such that

         A2: C is countable by A1;

        reconsider B = C as Basis of x by Lm1;

        take B;

        thus B is countable by A2;

      end;

      assume

       A3: the TopStruct of T is first-countable;

      let x be Point of T;

      reconsider y = x as Point of the TopStruct of T;

      consider C be Basis of y such that

       A4: C is countable by A3;

      reconsider B = C as Basis of x by Lm1;

      take B;

      thus B is countable by A4;

    end;

    registration

      let n be Nat;

      cluster ( TOP-REAL n) -> first-countable;

      coherence

      proof

         the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

        hence thesis by Th5;

      end;

    end

    theorem :: KURATO_2:6

    for A be Subset of ( TOP-REAL n), p be Point of ( TOP-REAL n), p9 be Point of ( Euclid n) st p = p9 holds p in ( Cl A) iff for r be Real st r > 0 holds ( Ball (p9,r)) meets A

    proof

      let A be Subset of ( TOP-REAL n), p be Point of ( TOP-REAL n), p9 be Point of ( Euclid n);

      assume

       A1: p = p9;

      hereby

        assume

         A2: p in ( Cl A);

        let r be Real;

        reconsider B = ( Ball (p9,r)) as Subset of ( TOP-REAL n) by TOPREAL3: 8;

        assume r > 0 ;

        then B is a_neighborhood of p by A1, GOBOARD6: 2;

        hence ( Ball (p9,r)) meets A by A2, CONNSP_2: 27;

      end;

      assume

       A3: for r be Real st r > 0 holds ( Ball (p9,r)) meets A;

      for G be a_neighborhood of p holds G meets A

      proof

        let G be a_neighborhood of p;

        p in ( Int G) by CONNSP_2:def 1;

        then ex r be Real st r > 0 & ( Ball (p9,r)) c= G by A1, GOBOARD6: 5;

        hence thesis by A3, XBOOLE_1: 63;

      end;

      hence thesis by CONNSP_2: 27;

    end;

    theorem :: KURATO_2:7

    for x,y be Point of ( TOP-REAL n), x9 be Point of ( Euclid n) st x9 = x & x <> y holds ex r be Real st not y in ( Ball (x9,r))

    proof

      let x,y be Point of ( TOP-REAL n), x9 be Point of ( Euclid n);

      reconsider y9 = y as Point of ( Euclid n) by TOPREAL3: 8;

      reconsider r = (( dist (x9,y9)) / 2) as Real;

      assume x9 = x & x <> y;

      then

       A1: ( dist (x9,y9)) <> 0 by METRIC_1: 2;

      take r;

      ( dist (x9,y9)) >= 0 by METRIC_1: 5;

      then ( dist (x9,y9)) > r by A1, XREAL_1: 216;

      hence thesis by METRIC_1: 11;

    end;

    theorem :: KURATO_2:8

    

     Th8: for S be Subset of ( TOP-REAL n) holds S is non bounded iff for r be Real st r > 0 holds ex x,y be Point of ( Euclid n) st x in S & y in S & ( dist (x,y)) > r

    proof

      let S be Subset of ( TOP-REAL n);

      reconsider S9 = S as Subset of ( Euclid n) by TOPREAL3: 8;

      hereby

        assume S is non bounded;

        then S9 is non bounded by JORDAN2C: 11;

        hence for r be Real st r > 0 holds ex x,y be Point of ( Euclid n) st x in S & y in S & ( dist (x,y)) > r by TBSP_1:def 7;

      end;

      assume

       A1: for r be Real st r > 0 holds ex x,y be Point of ( Euclid n) st x in S & y in S & ( dist (x,y)) > r;

      S is non bounded

      proof

        assume S is bounded;

        then S is bounded Subset of ( Euclid n) by JORDAN2C: 11;

        hence thesis by A1, TBSP_1:def 7;

      end;

      hence thesis;

    end;

    theorem :: KURATO_2:9

    

     Th9: for a,b be Real, x,y be Point of ( Euclid n) st ( Ball (x,a)) meets ( Ball (y,b)) holds ( dist (x,y)) < (a + b)

    proof

      let a,b be Real, x,y be Point of ( Euclid n);

      assume ( Ball (x,a)) meets ( Ball (y,b));

      then

      consider z be object such that

       A1: z in ( Ball (x,a)) and

       A2: z in ( Ball (y,b)) by XBOOLE_0: 3;

      reconsider z as Point of ( Euclid n) by A1;

      ( dist (y,z)) < b by A2, METRIC_1: 11;

      then

       A3: (( dist (x,z)) + ( dist (y,z))) < (( dist (x,z)) + b) by XREAL_1: 8;

      

       A4: (( dist (x,z)) + ( dist (y,z))) >= ( dist (x,y)) by METRIC_1: 4;

      ( dist (x,z)) < a by A1, METRIC_1: 11;

      then (( dist (x,z)) + b) < (a + b) by XREAL_1: 8;

      then (( dist (x,z)) + ( dist (y,z))) < (a + b) by A3, XXREAL_0: 2;

      hence thesis by A4, XXREAL_0: 2;

    end;

    theorem :: KURATO_2:10

    

     Th10: for a,b,c be Real, x,y,z be Point of ( Euclid n) st ( Ball (x,a)) meets ( Ball (z,c)) & ( Ball (z,c)) meets ( Ball (y,b)) holds ( dist (x,y)) < ((a + b) + (2 * c))

    proof

      let a,b,c be Real, x,y,z be Point of ( Euclid n);

      assume ( Ball (x,a)) meets ( Ball (z,c)) & ( Ball (z,c)) meets ( Ball (y,b));

      then (( dist (x,z)) + ( dist (z,y))) < ((a + c) + ( dist (z,y))) & ((a + c) + ( dist (z,y))) < ((a + c) + (c + b)) by Th9, XREAL_1: 8;

      then

       A1: (( dist (x,z)) + ( dist (z,y))) < ((a + c) + (c + b)) by XXREAL_0: 2;

      ( dist (x,y)) <= (( dist (x,z)) + ( dist (z,y))) by METRIC_1: 4;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: KURATO_2:11

    

     Th11: for X,Y be non empty TopSpace, x be Point of X, y be Point of Y, V be Subset of [:X, Y:] holds V is a_neighborhood of [: {x}, {y}:] iff V is a_neighborhood of [x, y]

    proof

      let X,Y be non empty TopSpace, x be Point of X, y be Point of Y, V be Subset of [:X, Y:];

      hereby

        assume V is a_neighborhood of [: {x}, {y}:];

        then V is a_neighborhood of { [x, y]} by ZFMISC_1: 29;

        hence V is a_neighborhood of [x, y] by CONNSP_2: 8;

      end;

      assume V is a_neighborhood of [x, y];

      then V is a_neighborhood of { [x, y]} by CONNSP_2: 8;

      hence thesis by ZFMISC_1: 29;

    end;

    begin

    theorem :: KURATO_2:12

    

     Th12: for T be non empty 1-sorted, F,G be SetSequence of the carrier of T, A be Subset of T st G is subsequence of F & for i be Nat holds (F . i) = A holds G = F

    proof

      let T be non empty 1-sorted, F,G be SetSequence of the carrier of T, A be Subset of T;

      assume that

       A1: G is subsequence of F and

       A2: for i be Nat holds (F . i) = A;

      consider NS be increasing sequence of NAT such that

       A3: G = (F * NS) by A1, VALUED_0:def 17;

      for i be Nat holds (G . i) = (F . i)

      proof

        let i be Nat;

        reconsider i as Element of NAT by ORDINAL1:def 12;

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

        

        then (G . i) = (F . (NS . i)) by A3, FUNCT_1: 13

        .= A by A2

        .= (F . i) by A2;

        hence thesis;

      end;

      then

       A4: for x be object st x in ( dom F) holds (F . x) = (G . x);

       NAT = ( dom G) & NAT = ( dom F) by FUNCT_2:def 1;

      hence thesis by A4, FUNCT_1: 2;

    end;

    theorem :: KURATO_2:13

    for T be non empty 1-sorted, S be SetSequence of the carrier of T, R be subsequence of S, n be Nat holds ex m be Element of NAT st m >= n & (R . n) = (S . m)

    proof

      let T be non empty 1-sorted, S be SetSequence of the carrier of T, R be subsequence of S, n be Nat;

      consider NS be increasing sequence of NAT such that

       A1: R = (S * NS) by VALUED_0:def 17;

      reconsider m = (NS . n) as Element of NAT ;

      take m;

      thus m >= n by SEQM_3: 14;

      n in NAT by ORDINAL1:def 12;

      then n in ( dom NS) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 13;

    end;

    begin

    definition

      let T be non empty TopSpace;

      let S be SetSequence of the carrier of T;

      :: KURATO_2:def1

      func Lim_inf S -> Subset of T means

      : Def1: for p be Point of T holds p in it iff for G be a_neighborhood of p holds ex k be Nat st for m be Nat st m > k holds (S . m) meets G;

      existence

      proof

        defpred P[ Point of T] means for G be a_neighborhood of $1 holds ex k be Nat st for m be Nat st m > k holds (S . m) meets G;

        thus ex IT be Subset of T st for p be Point of T holds p in IT iff P[p] from SUBSET_1:sch 3;

      end;

      uniqueness

      proof

        defpred P[ Point of T] means for G be a_neighborhood of $1 holds ex k be Nat st for m be Nat st m > k holds (S . m) meets G;

        let a,b be Subset of T such that

         A1: for p be Point of T holds p in a iff P[p] and

         A2: for p be Point of T holds p in b iff P[p];

        thus a = b from SUBSET_1:sch 2( A1, A2);

      end;

    end

    theorem :: KURATO_2:14

    

     Th14: for S be SetSequence of the carrier of ( TOP-REAL n), p be Point of ( TOP-REAL n), p9 be Point of ( Euclid n) st p = p9 holds p in ( Lim_inf S) iff for r be Real st r > 0 holds ex k be Nat st for m be Nat st m > k holds (S . m) meets ( Ball (p9,r))

    proof

      let S be SetSequence of the carrier of ( TOP-REAL n), p be Point of ( TOP-REAL n), p9 be Point of ( Euclid n);

      assume

       A1: p = p9;

      hereby

        assume

         A2: p in ( Lim_inf S);

        let r be Real;

        assume r > 0 ;

        then

        reconsider G = ( Ball (p9,r)) as a_neighborhood of p by A1, GOBOARD6: 2;

        ex k be Nat st for m be Nat st m > k holds (S . m) meets G by A2, Def1;

        hence ex k be Nat st for m be Nat st m > k holds (S . m) meets ( Ball (p9,r));

      end;

      assume

       A3: for r be Real st r > 0 holds ex k be Nat st for m be Nat st m > k holds (S . m) meets ( Ball (p9,r));

      now

        let G be a_neighborhood of p;

        

         A4: the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

        then

        reconsider G9 = ( Int G) as Subset of ( TopSpaceMetr ( Euclid n));

        

         A5: p9 in G9 by A1, CONNSP_2:def 1;

        G9 is open by A4, PRE_TOPC: 30;

        then

        consider r be Real such that

         A6: r > 0 and

         A7: ( Ball (p9,r)) c= G9 by A5, TOPMETR: 15;

        consider k be Nat such that

         A8: for m be Nat st m > k holds (S . m) meets ( Ball (p9,r)) by A3, A6;

        take k;

        let m be Nat;

        assume m > k;

        then G9 c= G & (S . m) meets ( Ball (p9,r)) by A8, TOPS_1: 16;

        hence (S . m) meets G by A7, XBOOLE_1: 1, XBOOLE_1: 63;

      end;

      hence thesis by Def1;

    end;

    theorem :: KURATO_2:15

    

     Th15: for T be non empty TopSpace, S be SetSequence of the carrier of T holds ( Cl ( Lim_inf S)) = ( Lim_inf S)

    proof

      let T be non empty TopSpace;

      let S be SetSequence of the carrier of T;

      thus ( Cl ( Lim_inf S)) c= ( Lim_inf S)

      proof

        let x be object;

        assume

         A1: x in ( Cl ( Lim_inf S));

        then

        reconsider x9 = x as Point of T;

        now

          let G be a_neighborhood of x9;

          set H = ( Int G);

          x9 in H by CONNSP_2:def 1;

          then ( Lim_inf S) meets H by A1, PRE_TOPC: 24;

          then

          consider z be object such that

           A2: z in ( Lim_inf S) and

           A3: z in H by XBOOLE_0: 3;

          reconsider z as Point of T by A2;

          z in ( Int H) by A3;

          then H is a_neighborhood of z by CONNSP_2:def 1;

          then

          consider k be Nat such that

           A4: for m be Nat st m > k holds (S . m) meets H by A2, Def1;

          take k;

          let m be Nat;

          assume m > k;

          then (S . m) meets H by A4;

          hence (S . m) meets G by TOPS_1: 16, XBOOLE_1: 63;

        end;

        hence thesis by Def1;

      end;

      thus thesis by PRE_TOPC: 18;

    end;

    registration

      let T be non empty TopSpace, S be SetSequence of the carrier of T;

      cluster ( Lim_inf S) -> closed;

      coherence

      proof

        ( Lim_inf S) = ( Cl ( Lim_inf S)) by Th15;

        hence thesis;

      end;

    end

    theorem :: KURATO_2:16

    for T be non empty TopSpace, R,S be SetSequence of the carrier of T st R is subsequence of S holds ( Lim_inf S) c= ( Lim_inf R)

    proof

      let T be non empty TopSpace, R,S be SetSequence of the carrier of T;

      assume R is subsequence of S;

      then

      consider Nseq be increasing sequence of NAT such that

       A1: R = (S * Nseq) by VALUED_0:def 17;

      let x be object;

      assume

       A2: x in ( Lim_inf S);

      then

      reconsider p = x as Point of T;

      for G be a_neighborhood of p holds ex k be Nat st for m be Nat st m > k holds (R . m) meets G

      proof

        let G be a_neighborhood of p;

        consider k be Nat such that

         A3: for m be Nat st m > k holds (S . m) meets G by A2, Def1;

        take k;

        let m1 be Nat;

        

         A4: m1 in NAT by ORDINAL1:def 12;

        

         A5: m1 <= (Nseq . m1) by SEQM_3: 14;

        assume m1 > k;

        then

         A6: (Nseq . m1) > k by A5, XXREAL_0: 2;

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

        then (R . m1) = (S . (Nseq . m1)) by A1, FUNCT_1: 13, A4;

        hence thesis by A3, A6;

      end;

      hence thesis by Def1;

    end;

    theorem :: KURATO_2:17

    

     Th17: for T be non empty TopSpace, A,B be SetSequence of the carrier of T st for i be Nat holds (A . i) c= (B . i) holds ( Lim_inf A) c= ( Lim_inf B)

    proof

      let T be non empty TopSpace, A,B be SetSequence of the carrier of T;

      assume

       A1: for i be Nat holds (A . i) c= (B . i);

      let x be object;

      assume

       A2: x in ( Lim_inf A);

      then

      reconsider p = x as Point of T;

      for G be a_neighborhood of p holds ex k be Nat st for m be Nat st m > k holds (B . m) meets G

      proof

        let G be a_neighborhood of p;

        consider k be Nat such that

         A3: for m be Nat st m > k holds (A . m) meets G by A2, Def1;

        take k;

        let m1 be Nat;

        assume m1 > k;

        then (A . m1) meets G by A3;

        hence thesis by A1, XBOOLE_1: 63;

      end;

      hence thesis by Def1;

    end;

    theorem :: KURATO_2:18

    for T be non empty TopSpace, A,B,C be SetSequence of the carrier of T st for i be Nat holds (C . i) = ((A . i) \/ (B . i)) holds (( Lim_inf A) \/ ( Lim_inf B)) c= ( Lim_inf C)

    proof

      let T be non empty TopSpace, A,B,C be SetSequence of the carrier of T;

      assume

       A1: for i be Nat holds (C . i) = ((A . i) \/ (B . i));

      let x be object;

      assume

       A2: x in (( Lim_inf A) \/ ( Lim_inf B));

      then

      reconsider p = x as Point of T;

      per cases by A2, XBOOLE_0:def 3;

        suppose

         A3: x in ( Lim_inf A);

        for H be a_neighborhood of p holds ex k be Nat st for m be Nat st m > k holds (C . m) meets H

        proof

          let H be a_neighborhood of p;

          consider k be Nat such that

           A4: for m be Nat st m > k holds (A . m) meets H by A3, Def1;

          take k;

          let m be Nat;

          assume m > k;

          then

           A5: (A . m) meets H by A4;

          (C . m) = ((A . m) \/ (B . m)) by A1;

          hence thesis by A5, XBOOLE_1: 7, XBOOLE_1: 63;

        end;

        hence thesis by Def1;

      end;

        suppose

         A6: x in ( Lim_inf B);

        for H be a_neighborhood of p holds ex k be Nat st for m be Nat st m > k holds (C . m) meets H

        proof

          let H be a_neighborhood of p;

          consider k be Nat such that

           A7: for m be Nat st m > k holds (B . m) meets H by A6, Def1;

          take k;

          let m be Nat;

          assume m > k;

          then

           A8: (B . m) meets H by A7;

          (C . m) = ((A . m) \/ (B . m)) by A1;

          hence thesis by A8, XBOOLE_1: 7, XBOOLE_1: 63;

        end;

        hence thesis by Def1;

      end;

    end;

    theorem :: KURATO_2:19

    for T be non empty TopSpace, A,B,C be SetSequence of the carrier of T st for i be Nat holds (C . i) = ((A . i) /\ (B . i)) holds ( Lim_inf C) c= (( Lim_inf A) /\ ( Lim_inf B))

    proof

      let T be non empty TopSpace, A,B,C be SetSequence of the carrier of T;

      assume

       A1: for i be Nat holds (C . i) = ((A . i) /\ (B . i));

      let x be object;

      assume

       A2: x in ( Lim_inf C);

      then

      reconsider p = x as Point of T;

      for H be a_neighborhood of p holds ex k be Nat st for m be Nat st m > k holds (B . m) meets H

      proof

        let H be a_neighborhood of p;

        consider k be Nat such that

         A3: for m be Nat st m > k holds (C . m) meets H by A2, Def1;

        take k;

        let m be Nat;

        assume m > k;

        then

         A4: (C . m) meets H by A3;

        (C . m) = ((A . m) /\ (B . m)) by A1;

        hence thesis by A4, XBOOLE_1: 17, XBOOLE_1: 63;

      end;

      then

       A5: x in ( Lim_inf B) by Def1;

      for H be a_neighborhood of p holds ex k be Nat st for m be Nat st m > k holds (A . m) meets H

      proof

        let H be a_neighborhood of p;

        consider k be Nat such that

         A6: for m be Nat st m > k holds (C . m) meets H by A2, Def1;

        take k;

        let m be Nat;

        assume m > k;

        then

         A7: (C . m) meets H by A6;

        (C . m) = ((A . m) /\ (B . m)) by A1;

        hence thesis by A7, XBOOLE_1: 17, XBOOLE_1: 63;

      end;

      then x in ( Lim_inf A) by Def1;

      hence thesis by A5, XBOOLE_0:def 4;

    end;

    theorem :: KURATO_2:20

    

     Th20: for T be non empty TopSpace, F,G be SetSequence of the carrier of T st for i be Nat holds (G . i) = ( Cl (F . i)) holds ( Lim_inf G) = ( Lim_inf F)

    proof

      let T be non empty TopSpace, F,G be SetSequence of the carrier of T;

      assume

       A1: for i be Nat holds (G . i) = ( Cl (F . i));

      thus ( Lim_inf G) c= ( Lim_inf F)

      proof

        let x be object;

        assume

         A2: x in ( Lim_inf G);

        then

        reconsider p = x as Point of T;

        for H be a_neighborhood of p holds ex k be Nat st for m be Nat st m > k holds (F . m) meets H

        proof

          let H be a_neighborhood of p;

          consider H1 be non empty Subset of T such that

           A3: H1 is a_neighborhood of p and

           A4: H1 is open and

           A5: H1 c= H by CONNSP_2: 5;

          consider k be Nat such that

           A6: for m be Nat st m > k holds (G . m) meets H1 by A2, A3, Def1;

          take k;

          let m be Nat;

          assume m > k;

          then (G . m) meets H1 by A6;

          then

          consider y be object such that

           A7: y in (G . m) and

           A8: y in H1 by XBOOLE_0: 3;

          reconsider y as Point of T by A7;

          H1 is a_neighborhood of y by A4, A8, CONNSP_2: 3;

          then

          consider H9 be non empty Subset of T such that

           A9: H9 is a_neighborhood of y and H9 is open and

           A10: H9 c= H1 by CONNSP_2: 5;

          y in ( Cl (F . m)) by A1, A7;

          then H9 meets (F . m) by A9, CONNSP_2: 27;

          then H1 meets (F . m) by A10, XBOOLE_1: 63;

          hence thesis by A5, XBOOLE_1: 63;

        end;

        hence thesis by Def1;

      end;

      for i be Nat holds (F . i) c= (G . i)

      proof

        let i be Nat;

        (G . i) = ( Cl (F . i)) by A1;

        hence thesis by PRE_TOPC: 18;

      end;

      hence ( Lim_inf F) c= ( Lim_inf G) by Th17;

    end;

    theorem :: KURATO_2:21

    for S be SetSequence of the carrier of ( TOP-REAL n), p be Point of ( TOP-REAL n) holds (ex s be Real_Sequence of n st s is convergent & (for x be Nat holds (s . x) in (S . x)) & p = ( lim s)) implies p in ( Lim_inf S)

    proof

      let S be SetSequence of the carrier of ( TOP-REAL n), p be Point of ( TOP-REAL n);

      reconsider p9 = p as Point of ( Euclid n) by TOPREAL3: 8;

      given s be Real_Sequence of n such that

       A1: s is convergent and

       A2: for x be Nat holds (s . x) in (S . x) and

       A3: p = ( lim s);

      for r be Real st r > 0 holds ex k be Nat st for m be Nat st m > k holds (S . m) meets ( Ball (p9,r))

      proof

        let r be Real;

        reconsider r9 = r as Real;

        assume r > 0 ;

        then

        consider l be Nat such that

         A4: for m be Nat st l <= m holds |.((s . m) - p).| < r9 by A1, A3, TOPRNS_1:def 9;

        reconsider v = ( max ( 0 ,l)) as Nat by TARSKI: 1;

        take v;

        let m be Nat;

        assume v < m;

        then l <= m by XXREAL_0: 30;

        then |.((s . m) - p).| < r9 by A4;

        then

         A5: (s . m) in ( Ball (p9,r)) by Th3;

        (s . m) in (S . m) by A2;

        hence thesis by A5, XBOOLE_0: 3;

      end;

      hence thesis by Th14;

    end;

    theorem :: KURATO_2:22

    

     Th22: for T be non empty TopSpace, P be Subset of T, s be SetSequence of the carrier of T st (for i be Nat holds (s . i) c= P) holds ( Lim_inf s) c= ( Cl P)

    proof

      let T be non empty TopSpace, P be Subset of T, s be SetSequence of the carrier of T;

      assume

       A1: for i be Nat holds (s . i) c= P;

      let x be object;

      assume

       A2: x in ( Lim_inf s);

      then

      reconsider p = x as Point of T;

      for G be Subset of T st G is open holds p in G implies P meets G

      proof

        let G be Subset of T;

        assume

         A3: G is open;

        assume p in G;

        then

        reconsider G9 = G as a_neighborhood of p by A3, CONNSP_2: 3;

        consider k be Nat such that

         A4: for m be Nat st m > k holds (s . m) meets G9 by A2, Def1;

        set m = (k + 1);

        m > k by NAT_1: 13;

        then (s . m) meets G9 by A4;

        hence thesis by A1, XBOOLE_1: 63;

      end;

      hence thesis by PRE_TOPC:def 7;

    end;

    theorem :: KURATO_2:23

    

     Th23: for T be non empty TopSpace, F be SetSequence of the carrier of T, A be Subset of T st for i be Nat holds (F . i) = A holds ( Lim_inf F) = ( Cl A)

    proof

      let T be non empty TopSpace, F be SetSequence of the carrier of T, A be Subset of T;

      assume

       A1: for i be Nat holds (F . i) = A;

      then for i be Nat holds (F . i) c= A;

      hence ( Lim_inf F) c= ( Cl A) by Th22;

      thus ( Cl A) c= ( Lim_inf F)

      proof

        let x be object;

        assume

         A2: x in ( Cl A);

        then

        reconsider p = x as Point of T;

        for G be a_neighborhood of p holds ex k be Nat st for m be Nat st m > k holds (F . m) meets G

        proof

          let G be a_neighborhood of p;

          take k = 1;

          let m be Nat;

          assume m > k;

          (F . m) = A by A1;

          hence thesis by A2, CONNSP_2: 27;

        end;

        hence thesis by Def1;

      end;

    end;

    theorem :: KURATO_2:24

    for T be non empty TopSpace, F be SetSequence of the carrier of T, A be closed Subset of T st for i be Nat holds (F . i) = A holds ( Lim_inf F) = A

    proof

      let T be non empty TopSpace, F be SetSequence of the carrier of T, A be closed Subset of T;

      assume for i be Nat holds (F . i) = A;

      then ( Lim_inf F) = ( Cl A) by Th23;

      hence thesis by PRE_TOPC: 22;

    end;

    theorem :: KURATO_2:25

    

     Th25: for S be SetSequence of the carrier of ( TOP-REAL n), P be Subset of ( TOP-REAL n) st P is bounded & (for i be Nat holds (S . i) c= P) holds ( Lim_inf S) is bounded

    proof

      let S be SetSequence of the carrier of ( TOP-REAL n);

      let P be Subset of ( TOP-REAL n);

      assume that

       A1: P is bounded and

       A2: for i be Nat holds (S . i) c= P;

      reconsider P9 = P as bounded Subset of ( Euclid n) by A1, JORDAN2C: 11;

      consider t be Real, z be Point of ( Euclid n) such that

       A3: 0 < t and

       A4: P9 c= ( Ball (z,t)) by METRIC_6:def 3;

      set r = 1, R = ((r + r) + (3 * t));

      assume ( Lim_inf S) is non bounded;

      then

      consider x,y be Point of ( Euclid n) such that

       A5: x in ( Lim_inf S) and

       A6: y in ( Lim_inf S) and

       A7: ( dist (x,y)) > R by A3, Th8;

      consider k1 be Nat such that

       A8: for m be Nat st m > k1 holds (S . m) meets ( Ball (x,r)) by A5, Th14;

      consider k2 be Nat such that

       A9: for m be Nat st m > k2 holds (S . m) meets ( Ball (y,r)) by A6, Th14;

      set k = (( max (k1,k2)) + 1);

      (S . k) c= P9 by A2;

      then

       A10: (S . k) c= ( Ball (z,t)) by A4;

      (2 * t) < (3 * t) by A3, XREAL_1: 68;

      then

       A11: ((r + r) + (2 * t)) < ((r + r) + (3 * t)) by XREAL_1: 8;

      ( max (k1,k2)) >= k2 by XXREAL_0: 25;

      then k > k2 by NAT_1: 13;

      then

       A12: ( Ball (z,t)) meets ( Ball (y,r)) by A9, A10, XBOOLE_1: 63;

      ( max (k1,k2)) >= k1 by XXREAL_0: 25;

      then k > k1 by NAT_1: 13;

      then ( Ball (z,t)) meets ( Ball (x,r)) by A8, A10, XBOOLE_1: 63;

      hence thesis by A7, A12, A11, Th10, XXREAL_0: 2;

    end;

    theorem :: KURATO_2:26

    for S be SetSequence of the carrier of ( TOP-REAL 2), P be Subset of ( TOP-REAL 2) st P is bounded & (for i be Nat holds (S . i) c= P) holds ( Lim_inf S) is compact by Th25, TOPREAL6: 79;

    theorem :: KURATO_2:27

    

     Th27: for A,B be SetSequence of the carrier of ( TOP-REAL n), C be SetSequence of the carrier of [:( TOP-REAL n), ( TOP-REAL n):] st for i be Nat holds (C . i) = [:(A . i), (B . i):] holds [:( Lim_inf A), ( Lim_inf B):] = ( Lim_inf C)

    proof

      let A,B be SetSequence of the carrier of ( TOP-REAL n), C be SetSequence of the carrier of [:( TOP-REAL n), ( TOP-REAL n):];

      assume

       A1: for i be Nat holds (C . i) = [:(A . i), (B . i):];

      thus [:( Lim_inf A), ( Lim_inf B):] c= ( Lim_inf C)

      proof

        let x be object;

        assume

         A2: x in [:( Lim_inf A), ( Lim_inf B):];

        then

        consider x1,x2 be object such that

         A3: x1 in ( Lim_inf A) and

         A4: x2 in ( Lim_inf B) and

         A5: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider p = x as Point of [:( TOP-REAL n), ( TOP-REAL n):] by A2;

        reconsider x1, x2 as Point of ( TOP-REAL n) by A3, A4;

        for G be a_neighborhood of p holds ex k be Nat st for m be Nat st m > k holds (C . m) meets G

        proof

          let G be a_neighborhood of p;

          G is a_neighborhood of [: {x1}, {x2}:] by A5, Th11;

          then

          consider V be a_neighborhood of {x1}, W be a_neighborhood of x2 such that

           A6: [:V, W:] c= G by BORSUK_1: 25;

          consider k2 be Nat such that

           A7: for m be Nat st m > k2 holds (B . m) meets W by A4, Def1;

          V is a_neighborhood of x1 by CONNSP_2: 8;

          then

          consider k1 be Nat such that

           A8: for m be Nat st m > k1 holds (A . m) meets V by A3, Def1;

          reconsider k = ( max (k1,k2)) as Nat by TARSKI: 1;

          take k;

          let m be Nat;

          assume

           A9: m > k;

          k >= k2 by XXREAL_0: 25;

          then m > k2 by A9, XXREAL_0: 2;

          then

           A10: (B . m) meets W by A7;

          k >= k1 by XXREAL_0: 25;

          then m > k1 by A9, XXREAL_0: 2;

          then (A . m) meets V by A8;

          then [:(A . m), (B . m):] meets [:V, W:] by A10, KURATO_0: 2;

          then (C . m) meets [:V, W:] by A1;

          hence thesis by A6, XBOOLE_1: 63;

        end;

        hence thesis by Def1;

      end;

      thus ( Lim_inf C) c= [:( Lim_inf A), ( Lim_inf B):]

      proof

        let x be object;

        assume

         A11: x in ( Lim_inf C);

        then x in the carrier of [:( TOP-REAL n), ( TOP-REAL n):];

        then

         A12: x in [:the carrier of ( TOP-REAL n), the carrier of ( TOP-REAL n):] by BORSUK_1:def 2;

        then

        reconsider p1 = (x `1 ), p2 = (x `2 ) as Point of ( TOP-REAL n) by MCART_1: 10;

        set H = the a_neighborhood of p2;

        set F = the a_neighborhood of p1;

        

         A13: x = [p1, p2] by A12, MCART_1: 21;

        for G be a_neighborhood of p2 holds ex k be Nat st for m be Nat st m > k holds (B . m) meets G

        proof

          let G be a_neighborhood of p2;

          consider k be Nat such that

           A14: for m be Nat st m > k holds (C . m) meets [:F, G:] by A11, A13, Def1;

          take k;

          let m be Nat;

          assume m > k;

          then (C . m) meets [:F, G:] by A14;

          then

          consider y be object such that

           A15: y in (C . m) and

           A16: y in [:F, G:] by XBOOLE_0: 3;

          y in [:(A . m), (B . m):] by A1, A15;

          then

           A17: (y `2 ) in (B . m) by MCART_1: 10;

          (y `2 ) in G by A16, MCART_1: 10;

          hence thesis by A17, XBOOLE_0: 3;

        end;

        then

         A18: p2 in ( Lim_inf B) by Def1;

        for G be a_neighborhood of p1 holds ex k be Nat st for m be Nat st m > k holds (A . m) meets G

        proof

          let G be a_neighborhood of p1;

          consider k be Nat such that

           A19: for m be Nat st m > k holds (C . m) meets [:G, H:] by A11, A13, Def1;

          take k;

          let m be Nat;

          assume m > k;

          then (C . m) meets [:G, H:] by A19;

          then

          consider y be object such that

           A20: y in (C . m) and

           A21: y in [:G, H:] by XBOOLE_0: 3;

          y in [:(A . m), (B . m):] by A1, A20;

          then

           A22: (y `1 ) in (A . m) by MCART_1: 10;

          (y `1 ) in G by A21, MCART_1: 10;

          hence thesis by A22, XBOOLE_0: 3;

        end;

        then p1 in ( Lim_inf A) by Def1;

        hence thesis by A13, A18, ZFMISC_1: 87;

      end;

    end;

    theorem :: KURATO_2:28

    for S be SetSequence of ( TOP-REAL 2) holds ( lim_inf S) c= ( Lim_inf S)

    proof

      let S be SetSequence of ( TOP-REAL 2);

      let x be object;

      assume

       A1: x in ( lim_inf S);

      then

      reconsider p = x as Point of ( Euclid 2) by TOPREAL3: 8;

      reconsider y = x as Point of ( TOP-REAL 2) by A1;

      consider k be Nat such that

       A2: for n be Nat holds x in (S . (k + n)) by A1, KURATO_0: 4;

      for r be Real st r > 0 holds ex k be Nat st for m be Nat st m > k holds (S . m) meets ( Ball (p,r))

      proof

        let r be Real;

        assume r > 0 ;

        then

         A3: x in ( Ball (p,r)) by GOBOARD6: 1;

        reconsider k as Nat;

        take k;

        let m be Nat;

        assume m > k;

        then

        consider h be Nat such that

         A4: m = (k + h) by NAT_1: 10;

        x in (S . m) by A2, A4;

        hence thesis by A3, XBOOLE_0: 3;

      end;

      then y in ( Lim_inf S) by Th14;

      hence thesis;

    end;

    theorem :: KURATO_2:29

    for C be Simple_closed_curve, i be Nat holds ( Fr (( UBD ( L~ ( Cage (C,i)))) ` )) = ( L~ ( Cage (C,i)))

    proof

      let C be Simple_closed_curve, i be Nat;

      set K = (( UBD ( L~ ( Cage (C,i)))) ` );

      set R = ( L~ ( Cage (C,i)));

      

       A1: (( BDD R) \/ (( BDD R) ` )) = ( [#] ( TOP-REAL 2)) by PRE_TOPC: 2;

      ( UBD R) c= (R ` ) by JORDAN2C: 26;

      then

       A2: ( UBD R) misses R by SUBSET_1: 23;

      ( UBD R) misses ( BDD R) by JORDAN2C: 24;

      then

       A3: ( UBD R) misses (( BDD R) \/ R) by A2, XBOOLE_1: 70;

      ( [#] ( TOP-REAL 2)) = ((R ` ) \/ R) by PRE_TOPC: 2

      .= ((( BDD R) \/ ( UBD R)) \/ R) by JORDAN2C: 27;

      

      then

       A4: K = ((( UBD R) \/ (( BDD R) \/ R)) \ ( UBD R)) by XBOOLE_1: 4

      .= (R \/ ( BDD R)) by A3, XBOOLE_1: 88;

      ((( BDD R) \/ ( UBD R)) ` ) = ((R ` ) ` ) by JORDAN2C: 27;

      then ((( BDD R) ` ) /\ (( UBD R) ` )) = R by XBOOLE_1: 53;

      

      then (( BDD R) \/ R) = ((( BDD R) \/ (( BDD R) ` )) /\ (( BDD R) \/ K)) by XBOOLE_1: 24

      .= (( BDD R) \/ K) by A1, XBOOLE_1: 28

      .= K by A4, XBOOLE_1: 7, XBOOLE_1: 12;

      then

       A5: ( Cl K) = (( BDD ( L~ ( Cage (C,i)))) \/ ( L~ ( Cage (C,i)))) by PRE_TOPC: 22;

      

       A6: (K ` ) = ( LeftComp ( Cage (C,i))) by GOBRD14: 36;

      ( BDD ( L~ ( Cage (C,i)))) misses ( UBD ( L~ ( Cage (C,i)))) by JORDAN2C: 24;

      then

       A7: (( BDD ( L~ ( Cage (C,i)))) /\ ( UBD ( L~ ( Cage (C,i))))) = {} ;

      ( Fr K) = (( Cl K) /\ ( Cl (K ` ))) by TOPS_1:def 2

      .= ((( BDD ( L~ ( Cage (C,i)))) \/ ( L~ ( Cage (C,i)))) /\ (( UBD ( L~ ( Cage (C,i)))) \/ ( L~ ( Cage (C,i))))) by A5, A6, GOBRD14: 22

      .= ((( BDD ( L~ ( Cage (C,i)))) /\ ( UBD ( L~ ( Cage (C,i))))) \/ ( L~ ( Cage (C,i)))) by XBOOLE_1: 24

      .= ( L~ ( Cage (C,i))) by A7;

      hence thesis;

    end;

    begin

    definition

      let T be non empty TopSpace;

      let S be SetSequence of the carrier of T;

      :: KURATO_2:def2

      func Lim_sup S -> Subset of T means

      : Def2: for x be object holds x in it iff ex A be subsequence of S st x in ( Lim_inf A);

      existence

      proof

        defpred P[ object] means ex A be subsequence of S st $1 in ( Lim_inf A);

        consider X be set such that

         A1: for x be object holds x in X iff x in the carrier of T & P[x] from XBOOLE_0:sch 1;

        X c= the carrier of T by A1;

        then

        reconsider X as Subset of T;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        defpred P[ object] means ex A be subsequence of S st $1 in ( Lim_inf A);

        let A1,A2 be Subset of T;

        assume that

         A2: for x be object holds x in A1 iff P[x] and

         A3: for x be object holds x in A2 iff P[x];

        A1 = A2 from XBOOLE_0:sch 2( A2, A3);

        hence thesis;

      end;

    end

    theorem :: KURATO_2:30

    for N be Nat, F be sequence of ( TOP-REAL N), x be Point of ( TOP-REAL N), x9 be Point of ( Euclid N) st x = x9 holds x is_a_cluster_point_of F iff for r be Real, n be Nat st r > 0 holds ex m be Nat st n <= m & (F . m) in ( Ball (x9,r))

    proof

      let N be Nat, F be sequence of ( TOP-REAL N), x be Point of ( TOP-REAL N), x9 be Point of ( Euclid N);

      assume

       A1: x = x9;

      hereby

        assume

         A2: x is_a_cluster_point_of F;

        let r be Real, n be Nat;

        reconsider O = ( Ball (x9,r)) as open Subset of ( TOP-REAL N) by Th1;

        assume r > 0 ;

        then x in O by A1, GOBOARD6: 1;

        then

        consider m be Element of NAT such that

         A3: n <= m & (F . m) in O by A2, FRECHET2:def 3;

        reconsider m as Nat;

        take m;

        thus n <= m & (F . m) in ( Ball (x9,r)) by A3;

      end;

      assume

       A4: for r be Real, n be Nat st r > 0 holds ex m be Nat st n <= m & (F . m) in ( Ball (x9,r));

      for O be Subset of ( TOP-REAL N), n be Nat st O is open & x in O holds ex m be Element of NAT st n <= m & (F . m) in O

      proof

        let O be Subset of ( TOP-REAL N), n be Nat;

        assume that

         A5: O is open and

         A6: x in O;

        reconsider n9 = n as Nat;

        

         A7: the TopStruct of ( TOP-REAL N) = ( TopSpaceMetr ( Euclid N)) by EUCLID:def 8;

        then

        reconsider G9 = O as Subset of ( TopSpaceMetr ( Euclid N));

        G9 is open by A5, A7, PRE_TOPC: 30;

        then

        consider r be Real such that

         A8: r > 0 and

         A9: ( Ball (x9,r)) c= G9 by A1, A6, TOPMETR: 15;

        consider m be Nat such that

         A10: n9 <= m & (F . m) in ( Ball (x9,r)) by A4, A8;

        reconsider m as Element of NAT by ORDINAL1:def 12;

        take m;

        thus thesis by A9, A10;

      end;

      hence thesis by FRECHET2:def 3;

    end;

    theorem :: KURATO_2:31

    

     Th31: for T be non empty TopSpace, A be SetSequence of the carrier of T holds ( Lim_inf A) c= ( Lim_sup A)

    proof

      let T be non empty TopSpace, A be SetSequence of the carrier of T;

      let x be object;

      assume

       A1: x in ( Lim_inf A);

      ex K be subsequence of A st x in ( Lim_inf K)

      proof

        reconsider B = A as subsequence of A by VALUED_0: 19;

        take B;

        thus thesis by A1;

      end;

      hence thesis by Def2;

    end;

    theorem :: KURATO_2:32

    

     Th32: for A,B,C be SetSequence of the carrier of ( TOP-REAL 2) st (for i be Nat holds (A . i) c= (B . i)) & C is subsequence of A holds ex D be subsequence of B st for i be Nat holds (C . i) c= (D . i)

    proof

      let A,B,C be SetSequence of the carrier of ( TOP-REAL 2);

      assume that

       A1: for i be Nat holds (A . i) c= (B . i) and

       A2: C is subsequence of A;

      consider NS be increasing sequence of NAT such that

       A3: C = (A * NS) by A2, VALUED_0:def 17;

      set D = (B * NS);

      reconsider D as SetSequence of ( TOP-REAL 2);

      reconsider D as subsequence of B;

      take D;

      for i be Nat holds (C . i) c= (D . i)

      proof

        let i be Nat;

        

         A4: ( dom NS) = NAT by FUNCT_2:def 1;

        (C . i) c= (D . i)

        proof

          let x be object;

          

           A5: i in NAT by ORDINAL1:def 12;

          assume x in (C . i);

          then

           A6: x in (A . (NS . i)) by A3, A4, FUNCT_1: 13, A5;

          (A . (NS . i)) c= (B . (NS . i)) by A1;

          then x in (B . (NS . i)) by A6;

          hence thesis by A4, FUNCT_1: 13, A5;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: KURATO_2:33

    for A,B,C be SetSequence of the carrier of ( TOP-REAL 2) st (for i be Nat holds (A . i) c= (B . i)) & C is subsequence of B holds ex D be subsequence of A st for i be Nat holds (D . i) c= (C . i)

    proof

      let A,B,C be SetSequence of the carrier of ( TOP-REAL 2);

      assume that

       A1: for i be Nat holds (A . i) c= (B . i) and

       A2: C is subsequence of B;

      consider NS be increasing sequence of NAT such that

       A3: C = (B * NS) by A2, VALUED_0:def 17;

      set D = (A * NS);

      reconsider D as SetSequence of ( TOP-REAL 2);

      reconsider D as subsequence of A;

      take D;

      for i be Nat holds (D . i) c= (C . i)

      proof

        let i be Nat;

        

         A4: ( dom NS) = NAT by FUNCT_2:def 1;

        (D . i) c= (C . i)

        proof

          let x be object;

          

           A5: i in NAT by ORDINAL1:def 12;

          assume x in (D . i);

          then

           A6: x in (A . (NS . i)) by A4, FUNCT_1: 13, A5;

          (A . (NS . i)) c= (B . (NS . i)) by A1;

          then x in (B . (NS . i)) by A6;

          hence thesis by A3, A4, FUNCT_1: 13, A5;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: KURATO_2:34

    

     Th34: for A,B be SetSequence of the carrier of ( TOP-REAL 2) st for i be Nat holds (A . i) c= (B . i) holds ( Lim_sup A) c= ( Lim_sup B)

    proof

      let A,B be SetSequence of the carrier of ( TOP-REAL 2);

      assume

       A1: for i be Nat holds (A . i) c= (B . i);

      ( Lim_sup A) c= ( Lim_sup B)

      proof

        let x be object;

        assume x in ( Lim_sup A);

        then

        consider A1 be subsequence of A such that

         A2: x in ( Lim_inf A1) by Def2;

        consider D be subsequence of B such that

         A3: for i be Nat holds (A1 . i) c= (D . i) by A1, Th32;

        ( Lim_inf A1) c= ( Lim_inf D) by A3, Th17;

        hence thesis by A2, Def2;

      end;

      hence thesis;

    end;

    theorem :: KURATO_2:35

    for A,B,C be SetSequence of the carrier of ( TOP-REAL 2) st for i be Nat holds (C . i) = ((A . i) \/ (B . i)) holds (( Lim_sup A) \/ ( Lim_sup B)) c= ( Lim_sup C)

    proof

      let A,B,C be SetSequence of the carrier of ( TOP-REAL 2);

      assume

       A1: for i be Nat holds (C . i) = ((A . i) \/ (B . i));

      

       A2: for i be Nat holds (B . i) c= (C . i)

      proof

        let i be Nat;

        (C . i) = ((A . i) \/ (B . i)) by A1;

        hence thesis by XBOOLE_1: 7;

      end;

      

       A3: for i be Nat holds (A . i) c= (C . i)

      proof

        let i be Nat;

        (C . i) = ((A . i) \/ (B . i)) by A1;

        hence thesis by XBOOLE_1: 7;

      end;

      thus (( Lim_sup A) \/ ( Lim_sup B)) c= ( Lim_sup C)

      proof

        let x be object;

        assume

         A4: x in (( Lim_sup A) \/ ( Lim_sup B));

        per cases by A4, XBOOLE_0:def 3;

          suppose x in ( Lim_sup A);

          then

          consider A1 be subsequence of A such that

           A5: x in ( Lim_inf A1) by Def2;

          consider C1 be subsequence of C such that

           A6: for i be Nat holds (A1 . i) c= (C1 . i) by A3, Th32;

          ( Lim_inf A1) c= ( Lim_inf C1) by A6, Th17;

          hence thesis by A5, Def2;

        end;

          suppose x in ( Lim_sup B);

          then

          consider B1 be subsequence of B such that

           A7: x in ( Lim_inf B1) by Def2;

          consider C1 be subsequence of C such that

           A8: for i be Nat holds (B1 . i) c= (C1 . i) by A2, Th32;

          ( Lim_inf B1) c= ( Lim_inf C1) by A8, Th17;

          hence thesis by A7, Def2;

        end;

      end;

    end;

    theorem :: KURATO_2:36

    for A,B,C be SetSequence of the carrier of ( TOP-REAL 2) st for i be Nat holds (C . i) = ((A . i) /\ (B . i)) holds ( Lim_sup C) c= (( Lim_sup A) /\ ( Lim_sup B))

    proof

      let A,B,C be SetSequence of the carrier of ( TOP-REAL 2);

      assume

       A1: for i be Nat holds (C . i) = ((A . i) /\ (B . i));

      let x be object;

      assume x in ( Lim_sup C);

      then

      consider C1 be subsequence of C such that

       A2: x in ( Lim_inf C1) by Def2;

      for i be Nat holds (C . i) c= (B . i)

      proof

        let i be Nat;

        (C . i) = ((A . i) /\ (B . i)) by A1;

        hence thesis by XBOOLE_1: 17;

      end;

      then

      consider E1 be subsequence of B such that

       A3: for i be Nat holds (C1 . i) c= (E1 . i) by Th32;

      ( Lim_inf C1) c= ( Lim_inf E1) by A3, Th17;

      then

       A4: x in ( Lim_sup B) by A2, Def2;

      for i be Nat holds (C . i) c= (A . i)

      proof

        let i be Nat;

        (C . i) = ((A . i) /\ (B . i)) by A1;

        hence thesis by XBOOLE_1: 17;

      end;

      then

      consider D1 be subsequence of A such that

       A5: for i be Nat holds (C1 . i) c= (D1 . i) by Th32;

      ( Lim_inf C1) c= ( Lim_inf D1) by A5, Th17;

      then x in ( Lim_sup A) by A2, Def2;

      hence thesis by A4, XBOOLE_0:def 4;

    end;

    theorem :: KURATO_2:37

    

     Th37: for A,B be SetSequence of the carrier of ( TOP-REAL 2), C,C1 be SetSequence of the carrier of [:( TOP-REAL 2), ( TOP-REAL 2):] st (for i be Nat holds (C . i) = [:(A . i), (B . i):]) & C1 is subsequence of C holds ex A1,B1 be SetSequence of the carrier of ( TOP-REAL 2) st A1 is subsequence of A & B1 is subsequence of B & for i be Nat holds (C1 . i) = [:(A1 . i), (B1 . i):]

    proof

      let A,B be SetSequence of the carrier of ( TOP-REAL 2), C,C1 be SetSequence of the carrier of [:( TOP-REAL 2), ( TOP-REAL 2):];

      assume that

       A1: for i be Nat holds (C . i) = [:(A . i), (B . i):] and

       A2: C1 is subsequence of C;

      consider NS be increasing sequence of NAT such that

       A3: C1 = (C * NS) by A2, VALUED_0:def 17;

      set B1 = (B * NS);

      set A1 = (A * NS);

      reconsider A1 as SetSequence of ( TOP-REAL 2);

      reconsider B1 as SetSequence of ( TOP-REAL 2);

      take A1, B1;

      for i be Nat holds (C1 . i) = [:(A1 . i), (B1 . i):]

      proof

        let i be Nat;

        

         A4: i in NAT by ORDINAL1:def 12;

        

         A5: ( dom NS) = NAT by FUNCT_2:def 1;

        then

         A6: (A1 . i) = (A . (NS . i)) & (B1 . i) = (B . (NS . i)) by FUNCT_1: 13, A4;

        (C1 . i) = (C . (NS . i)) by A3, A5, FUNCT_1: 13, A4

        .= [:(A1 . i), (B1 . i):] by A1, A6;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: KURATO_2:38

    for A,B be SetSequence of the carrier of ( TOP-REAL 2), C be SetSequence of the carrier of [:( TOP-REAL 2), ( TOP-REAL 2):] st for i be Nat holds (C . i) = [:(A . i), (B . i):] holds ( Lim_sup C) c= [:( Lim_sup A), ( Lim_sup B):]

    proof

      let A,B be SetSequence of the carrier of ( TOP-REAL 2), C be SetSequence of the carrier of [:( TOP-REAL 2), ( TOP-REAL 2):];

      assume

       A1: for i be Nat holds (C . i) = [:(A . i), (B . i):];

      let x be object;

      assume x in ( Lim_sup C);

      then

      consider C1 be subsequence of C such that

       A2: x in ( Lim_inf C1) by Def2;

      x in the carrier of [:( TOP-REAL 2), ( TOP-REAL 2):] by A2;

      then x in [:the carrier of ( TOP-REAL 2), the carrier of ( TOP-REAL 2):] by BORSUK_1:def 2;

      then

      consider x1,x2 be object such that

       A3: x = [x1, x2] by RELAT_1:def 1;

      consider A1,B1 be SetSequence of the carrier of ( TOP-REAL 2) such that

       A4: A1 is subsequence of A and

       A5: B1 is subsequence of B and

       A6: for i be Nat holds (C1 . i) = [:(A1 . i), (B1 . i):] by A1, Th37;

      

       A7: x in [:( Lim_inf A1), ( Lim_inf B1):] by A2, A6, Th27;

      then x2 in ( Lim_inf B1) by A3, ZFMISC_1: 87;

      then

       A8: x2 in ( Lim_sup B) by A5, Def2;

      x1 in ( Lim_inf A1) by A3, A7, ZFMISC_1: 87;

      then x1 in ( Lim_sup A) by A4, Def2;

      hence thesis by A3, A8, ZFMISC_1: 87;

    end;

    ::$Notion-Name

    theorem :: KURATO_2:39

    

     Th39: for T be non empty TopSpace, F be SetSequence of the carrier of T, A be Subset of T st for i be Nat holds (F . i) = A holds ( Lim_inf F) = ( Lim_sup F)

    proof

      let T be non empty TopSpace, F be SetSequence of the carrier of T, A be Subset of T;

      assume

       A1: for i be Nat holds (F . i) = A;

      thus ( Lim_inf F) c= ( Lim_sup F) by Th31;

      thus ( Lim_sup F) c= ( Lim_inf F)

      proof

        let x be object;

        assume x in ( Lim_sup F);

        then ex G be subsequence of F st x in ( Lim_inf G) by Def2;

        hence thesis by A1, Th12;

      end;

    end;

    theorem :: KURATO_2:40

    for F be SetSequence of the carrier of ( TOP-REAL 2), A be Subset of ( TOP-REAL 2) st for i be Nat holds (F . i) = A holds ( Lim_sup F) = ( Cl A)

    proof

      let F be SetSequence of the carrier of ( TOP-REAL 2), A be Subset of ( TOP-REAL 2);

      assume

       A1: for i be Nat holds (F . i) = A;

      then ( Lim_inf F) = ( Lim_sup F) by Th39;

      hence thesis by A1, Th23;

    end;

    theorem :: KURATO_2:41

    for F,G be SetSequence of the carrier of ( TOP-REAL 2) st for i be Nat holds (G . i) = ( Cl (F . i)) holds ( Lim_sup G) = ( Lim_sup F)

    proof

      let F,G be SetSequence of the carrier of ( TOP-REAL 2);

      assume

       A1: for i be Nat holds (G . i) = ( Cl (F . i));

      thus ( Lim_sup G) c= ( Lim_sup F)

      proof

        let x be object;

        assume x in ( Lim_sup G);

        then

        consider H be subsequence of G such that

         A2: x in ( Lim_inf H) by Def2;

        consider NS be increasing sequence of NAT such that

         A3: H = (G * NS) by VALUED_0:def 17;

        set P = (F * NS);

        reconsider P as SetSequence of ( TOP-REAL 2);

        reconsider P as subsequence of F;

        for i be Nat holds (H . i) = ( Cl (P . i))

        proof

          let i be Nat;

          

           A4: i in NAT by ORDINAL1:def 12;

          

           A5: ( dom NS) = NAT by FUNCT_2:def 1;

          

          then (H . i) = (G . (NS . i)) by A3, FUNCT_1: 13, A4

          .= ( Cl (F . (NS . i))) by A1

          .= ( Cl (P . i)) by A5, FUNCT_1: 13, A4;

          hence thesis;

        end;

        then ( Lim_inf H) = ( Lim_inf P) by Th20;

        hence thesis by A2, Def2;

      end;

      for i be Nat holds (F . i) c= (G . i)

      proof

        let i be Nat;

        (G . i) = ( Cl (F . i)) by A1;

        hence thesis by PRE_TOPC: 18;

      end;

      hence thesis by Th34;

    end;