topmetr3.miz



    begin

    theorem :: TOPMETR3:1

    

     Th1: for X be non empty MetrSpace, S be sequence of X, F be Subset of ( TopSpaceMetr X) st S is convergent & (for n be Nat holds (S . n) in F) & F is closed holds ( lim S) in F

    proof

      let X be non empty MetrSpace, S be sequence of X, F be Subset of ( TopSpaceMetr X);

      assume that

       A1: S is convergent and

       A2: for n be Nat holds (S . n) in F and

       A3: F is closed;

      

       A4: for G be Subset of ( TopSpaceMetr X) st G is open holds ( lim S) in G implies F meets G

      proof

        let G be Subset of ( TopSpaceMetr X);

        assume

         A5: G is open;

        now

          assume ( lim S) in G;

          then

          consider r1 be Real such that

           A6: r1 > 0 and

           A7: ( Ball (( lim S),r1)) c= G by A5, TOPMETR: 15;

          reconsider r2 = r1 as Real;

          consider n be Nat such that

           A8: for m be Nat st m >= n holds ( dist ((S . m),( lim S))) < r2 by A1, A6, TBSP_1:def 3;

          ( dist ((S . n),( lim S))) < r2 by A8;

          then

           A9: (S . n) in ( Ball (( lim S),r1)) by METRIC_1: 11;

          (S . n) in F by A2;

          then (S . n) in (F /\ G) by A7, A9, XBOOLE_0:def 4;

          hence F meets G by XBOOLE_0:def 7;

        end;

        hence thesis;

      end;

      reconsider F0 = F as Subset of ( TopSpaceMetr X);

      ( lim S) in the carrier of X;

      then ( lim S) in the carrier of ( TopSpaceMetr X) by TOPMETR: 12;

      then ( lim S) in ( Cl F0) by A4, PRE_TOPC:def 7;

      hence thesis by A3, PRE_TOPC: 22;

    end;

    theorem :: TOPMETR3:2

    

     Th2: for X,Y be non empty MetrSpace, f be Function of ( TopSpaceMetr X), ( TopSpaceMetr Y), S be sequence of X holds (f * S) is sequence of Y

    proof

      let X,Y be non empty MetrSpace, f be Function of ( TopSpaceMetr X), ( TopSpaceMetr Y), S be sequence of X;

      

       A1: ( dom f) = the carrier of ( TopSpaceMetr X) by FUNCT_2:def 1

      .= the carrier of X by TOPMETR: 12;

      ( dom S) = NAT & ( rng S) c= the carrier of X by FUNCT_2:def 1;

      then ( dom (f * S)) = NAT by A1, RELAT_1: 27;

      hence thesis by FUNCT_2:def 1, TOPMETR: 12;

    end;

    theorem :: TOPMETR3:3

    

     Th3: for X,Y be non empty MetrSpace, f be Function of ( TopSpaceMetr X), ( TopSpaceMetr Y), S be sequence of X, T be sequence of Y st S is convergent & T = (f * S) & f is continuous holds T is convergent

    proof

      let X,Y be non empty MetrSpace, f be Function of ( TopSpaceMetr X), ( TopSpaceMetr Y), S be sequence of X, T be sequence of Y;

      assume that

       A1: S is convergent and

       A2: T = (f * S) and

       A3: f is continuous;

      set z0 = ( lim S);

      reconsider p = z0 as Point of ( TopSpaceMetr X) by TOPMETR: 12;

      

       A4: ( dom f) = the carrier of ( TopSpaceMetr X) by FUNCT_2:def 1

      .= the carrier of X by TOPMETR: 12;

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

      then

      reconsider x0 = (f . ( lim S)) as Element of Y by TOPMETR: 12;

      for r be Real st r > 0 holds ex n be Nat st for m be Nat st n <= m holds ( dist ((T . m),x0)) < r

      proof

        let r be Real;

        reconsider V = ( Ball (x0,r)) as Subset of ( TopSpaceMetr Y) by TOPMETR: 12;

        assume r > 0 ;

        then V is open & x0 in V by GOBOARD6: 1, TOPMETR: 14;

        then

        consider W be Subset of ( TopSpaceMetr X) such that

         A5: p in W & W is open and

         A6: (f .: W) c= V by A3, JGRAPH_2: 10;

        consider r0 be Real such that

         A7: r0 > 0 and

         A8: ( Ball (z0,r0)) c= W by A5, TOPMETR: 15;

        reconsider r00 = r0 as Real;

        consider n0 be Nat such that

         A9: for m be Nat st n0 <= m holds ( dist ((S . m),z0)) < r00 by A1, A7, TBSP_1:def 3;

        for m be Nat st n0 <= m holds ( dist ((T . m),x0)) < r

        proof

          let m be Nat;

          assume n0 <= m;

          then ( dist ((S . m),z0)) < r0 by A9;

          then (S . m) in ( Ball (z0,r0)) by METRIC_1: 11;

          then

           A10: (f . (S . m)) in (f .: W) by A4, A8, FUNCT_1:def 6;

          

           A11: m in NAT by ORDINAL1:def 12;

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

          then (T . m) in (f .: W) by A2, A10, FUNCT_1: 12, A11;

          hence thesis by A6, METRIC_1: 11;

        end;

        hence thesis;

      end;

      hence thesis by TBSP_1:def 2;

    end;

    theorem :: TOPMETR3:4

    

     Th4: for s be Real_Sequence, S be sequence of RealSpace st s = S holds (s is convergent iff S is convergent) & (s is convergent implies ( lim s) = ( lim S))

    proof

      let s be Real_Sequence, S be sequence of RealSpace ;

      assume

       A1: s = S;

      

       A2: s is convergent implies S is convergent

      proof

        assume s is convergent;

        then

        consider g be Real such that

         A3: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((s . m) - g).| < p by SEQ_2:def 6;

        reconsider g0 = g as Real;

        reconsider x0 = g as Point of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

        for r be Real st r > 0 holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S . m),x0)) < r

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider n0 be Nat such that

           A4: for m be Nat st n0 <= m holds |.((s . m) - g).| < r by A3;

          for m be Nat st n0 <= m holds ( dist ((S . m),x0)) < r

          proof

            let m be Nat;

            assume

             A5: n0 <= m;

            reconsider t = (s . m) as Real;

            ( dist ((S . m),x0)) = ( real_dist . (t,g)) by A1, METRIC_1:def 1, METRIC_1:def 13

            .= |.(t - g0).| by METRIC_1:def 12;

            hence thesis by A4, A5;

          end;

          hence thesis;

        end;

        hence thesis by TBSP_1:def 2;

      end;

      S is convergent implies s is convergent

      proof

        assume S is convergent;

        then

        consider x be Element of RealSpace such that

         A6: for r be Real st r > 0 holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S . m),x)) < r by TBSP_1:def 2;

        reconsider g0 = x as Real;

        for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((s . m) - g0).| < p

        proof

          let p be Real;

          reconsider p0 = p as Real;

          assume 0 < p;

          then

          consider n0 be Nat such that

           A7: for m be Nat st n0 <= m holds ( dist ((S . m),x)) < p0 by A6;

          for m be Nat st n0 <= m holds |.((s . m) - g0).| < p

          proof

            let m be Nat;

            assume

             A8: n0 <= m;

            reconsider t = (s . m) as Real;

            ( dist ((S . m),x)) = ( real_dist . (t,g0)) by A1, METRIC_1:def 1, METRIC_1:def 13

            .= |.(t - g0).| by METRIC_1:def 12;

            hence thesis by A7, A8;

          end;

          hence thesis;

        end;

        hence thesis by SEQ_2:def 6;

      end;

      hence s is convergent iff S is convergent by A2;

      thus s is convergent implies ( lim s) = ( lim S)

      proof

        reconsider g0 = ( lim S) as Real;

        assume

         A9: s is convergent;

        for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds |.((s . n) - g0).| < r

        proof

          let r be Real;

          reconsider r0 = r as Real;

          assume 0 < r;

          then

          consider m0 be Nat such that

           A10: for n be Nat st m0 <= n holds ( dist ((S . n),( lim S))) < r0 by A2, A9, TBSP_1:def 3;

          for n be Nat st m0 <= n holds |.((s . n) - g0).| < r

          proof

            let n be Nat;

            assume

             A11: m0 <= n;

            ( dist ((S . n),( lim S))) = ( real_dist . ((s . n),g0)) by A1, METRIC_1:def 1, METRIC_1:def 13

            .= |.((s . n) - g0).| by METRIC_1:def 12;

            hence thesis by A10, A11;

          end;

          hence thesis;

        end;

        hence thesis by A9, SEQ_2:def 7;

      end;

    end;

    theorem :: TOPMETR3:5

    

     Th5: for a,b be Real, s be Real_Sequence st ( rng s) c= [.a, b.] holds s is sequence of ( Closed-Interval-MSpace (a,b))

    proof

      let a,b be Real, s be Real_Sequence;

      assume

       A1: ( rng s) c= [.a, b.];

      reconsider t = (s . 0 ) as Real;

      

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

      then (s . 0 ) in ( rng s) by FUNCT_1:def 3;

      then a <= t & t <= b by A1, XXREAL_1: 1;

      then the carrier of ( Closed-Interval-MSpace (a,b)) = [.a, b.] by TOPMETR: 10, XXREAL_0: 2;

      hence thesis by A1, A2, FUNCT_2: 2;

    end;

    theorem :: TOPMETR3:6

    

     Th6: for a,b be Real, S be sequence of ( Closed-Interval-MSpace (a,b)) st a <= b holds S is sequence of RealSpace

    proof

      let a,b be Real, S be sequence of ( Closed-Interval-MSpace (a,b));

      assume a <= b;

      then the carrier of ( Closed-Interval-MSpace (a,b)) = [.a, b.] by TOPMETR: 10;

      then ( dom S) = NAT & ( rng S) c= the carrier of RealSpace by FUNCT_2:def 1, METRIC_1:def 13, XBOOLE_1: 1;

      hence thesis by FUNCT_2: 2;

    end;

    theorem :: TOPMETR3:7

    

     Th7: for a,b be Real, S1 be sequence of ( Closed-Interval-MSpace (a,b)), S be sequence of RealSpace st S = S1 & a <= b holds (S is convergent iff S1 is convergent) & (S is convergent implies ( lim S) = ( lim S1))

    proof

      let a,b be Real, S1 be sequence of ( Closed-Interval-MSpace (a,b)), S be sequence of RealSpace ;

      assume that

       A1: S = S1 and

       A2: a <= b;

      reconsider P = [.a, b.] as Subset of R^1 by TOPMETR: 17;

      

       A3: the carrier of ( Closed-Interval-MSpace (a,b)) = [.a, b.] by A2, TOPMETR: 10;

      

       A4: S is convergent implies S1 is convergent

      proof

        

         A5: for m be Nat holds (S . m) in [.a, b.]

        proof

          let m be Nat;

          

           A6: m in NAT by ORDINAL1:def 12;

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

          then (S1 . m) in ( rng S1) by FUNCT_1:def 3, A6;

          hence thesis by A1, A3;

        end;

        

         A7: P is closed by TREAL_1: 1;

        assume

         A8: S is convergent;

        then

        consider x0 be Element of RealSpace such that

         A9: for r be Real st r > 0 holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S . m),x0)) < r by TBSP_1:def 2;

        x0 = ( lim S) by A8, A9, TBSP_1:def 3;

        then

        reconsider x1 = x0 as Element of ( Closed-Interval-MSpace (a,b)) by A3, A8, A5, A7, Th1, TOPMETR:def 6;

        for r be Real st r > 0 holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S1 . m),x1)) < r

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider n0 be Nat such that

           A10: for m be Nat st n0 <= m holds ( dist ((S . m),x0)) < r by A9;

          for m be Nat st n0 <= m holds ( dist ((S1 . m),x1)) < r

          proof

            let m be Nat;

            assume

             A11: n0 <= m;

            ( dist ((S1 . m),x1)) = (the distance of ( Closed-Interval-MSpace (a,b)) . ((S1 . m),x1)) by METRIC_1:def 1

            .= (the distance of RealSpace . ((S1 . m),x1)) by TOPMETR:def 1

            .= ( dist ((S . m),x0)) by A1, METRIC_1:def 1;

            hence thesis by A10, A11;

          end;

          hence thesis;

        end;

        hence thesis by TBSP_1:def 2;

      end;

      S1 is convergent implies S is convergent

      proof

        assume S1 is convergent;

        then

        consider x0 be Element of ( Closed-Interval-MSpace (a,b)) such that

         A12: for r be Real st r > 0 holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S1 . m),x0)) < r by TBSP_1:def 2;

        x0 in [.a, b.] by A3;

        then

        reconsider x1 = x0 as Element of RealSpace by METRIC_1:def 13;

        for r be Real st r > 0 holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S . m),x1)) < r

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider n0 be Nat such that

           A13: for m be Nat st n0 <= m holds ( dist ((S1 . m),x0)) < r by A12;

          for m be Nat st n0 <= m holds ( dist ((S . m),x1)) < r

          proof

            let m be Nat;

            assume

             A14: n0 <= m;

            ( dist ((S1 . m),x0)) = (the distance of ( Closed-Interval-MSpace (a,b)) . ((S1 . m),x0)) by METRIC_1:def 1

            .= (the distance of RealSpace . ((S1 . m),x0)) by TOPMETR:def 1

            .= ( dist ((S . m),x1)) by A1, METRIC_1:def 1;

            hence thesis by A13, A14;

          end;

          hence thesis;

        end;

        hence thesis by TBSP_1:def 2;

      end;

      hence S is convergent iff S1 is convergent by A4;

      thus S is convergent implies ( lim S) = ( lim S1)

      proof

        ( lim S1) in the carrier of ( Closed-Interval-MSpace (a,b));

        then

        reconsider t0 = ( lim S1) as Point of RealSpace by A3, METRIC_1:def 13;

        assume

         A15: S is convergent;

        for r1 be Real st 0 < r1 holds ex m1 be Nat st for n1 be Nat st m1 <= n1 holds ( dist ((S . n1),t0)) < r1

        proof

          let r1 be Real;

          assume 0 < r1;

          then

          consider m1 be Nat such that

           A16: for n1 be Nat st m1 <= n1 holds ( dist ((S1 . n1),( lim S1))) < r1 by A4, A15, TBSP_1:def 3;

          for n1 be Nat st m1 <= n1 holds ( dist ((S . n1),t0)) < r1

          proof

            let n1 be Nat;

            assume

             A17: m1 <= n1;

            ( dist ((S1 . n1),( lim S1))) = (the distance of ( Closed-Interval-MSpace (a,b)) . ((S1 . n1),( lim S1))) by METRIC_1:def 1

            .= (the distance of RealSpace . ((S1 . n1),( lim S1))) by TOPMETR:def 1

            .= ( dist ((S . n1),t0)) by A1, METRIC_1:def 1;

            hence thesis by A16, A17;

          end;

          hence thesis;

        end;

        hence thesis by A15, TBSP_1:def 3;

      end;

    end;

    theorem :: TOPMETR3:8

    

     Th8: for a,b be Real, s be Real_Sequence, S be sequence of ( Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is convergent holds S is convergent & ( lim s) = ( lim S)

    proof

      let a,b be Real, s be Real_Sequence, S be sequence of ( Closed-Interval-MSpace (a,b));

      assume that

       A1: S = s and

       A2: a <= b and

       A3: s is convergent;

      reconsider S0 = S as sequence of RealSpace by A2, Th6;

      

       A4: S0 is convergent by A1, A3, Th4;

      hence S is convergent by A2, Th7;

      ( lim S0) = ( lim S) by A2, A4, Th7;

      hence thesis by A1, A3, Th4;

    end;

    theorem :: TOPMETR3:9

    for a,b be Real, s be Real_Sequence, S be sequence of ( Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-decreasing holds S is convergent

    proof

      let a,b be Real, s be Real_Sequence, S be sequence of ( Closed-Interval-MSpace (a,b));

      assume that

       A1: S = s and

       A2: a <= b and

       A3: s is non-decreasing;

      for n be Nat holds (s . n) < (b + 1)

      proof

        let n be Nat;

        

         A4: b < (b + 1) by XREAL_1: 29;

        

         A5: n in NAT by ORDINAL1:def 12;

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

        then

         A6: (s . n) in ( rng S) by A1, FUNCT_1:def 3, A5;

        the carrier of ( Closed-Interval-MSpace (a,b)) = [.a, b.] by A2, TOPMETR: 10;

        then (s . n) <= b by A6, XXREAL_1: 1;

        hence thesis by A4, XXREAL_0: 2;

      end;

      then s is bounded_above by SEQ_2:def 3;

      hence thesis by A1, A2, A3, Th8;

    end;

    theorem :: TOPMETR3:10

    for a,b be Real, s be Real_Sequence, S be sequence of ( Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-increasing holds S is convergent

    proof

      let a,b be Real, s be Real_Sequence, S be sequence of ( Closed-Interval-MSpace (a,b));

      assume that

       A1: S = s and

       A2: a <= b and

       A3: s is non-increasing;

      for n be Nat holds (s . n) > (a - 1)

      proof

        let n be Nat;

        a < (a + 1) by XREAL_1: 29;

        then

         A4: (a - 1) < a by XREAL_1: 19;

        

         A5: n in NAT by ORDINAL1:def 12;

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

        then

         A6: (s . n) in ( rng S) by A1, FUNCT_1:def 3, A5;

        the carrier of ( Closed-Interval-MSpace (a,b)) = [.a, b.] by A2, TOPMETR: 10;

        then a <= (s . n) by A6, XXREAL_1: 1;

        hence thesis by A4, XXREAL_0: 2;

      end;

      then s is bounded_below by SEQ_2:def 4;

      hence thesis by A1, A2, A3, Th8;

    end;

    theorem :: TOPMETR3:11

    

     Th11: for R be non empty Subset of REAL st R is bounded_above holds ex s be Real_Sequence st s is non-decreasing convergent & ( rng s) c= R & ( lim s) = ( upper_bound R)

    proof

      let R be non empty Subset of REAL ;

      reconsider rs = ( upper_bound R) as Real;

      defpred X[ Nat, Real] means ($2 in R & (for r00 be Real st r00 = $2 holds (rs - (1 / ($1 + 1)) qua Real) < r00));

      assume

       A1: R is bounded_above;

      

       A2: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

      proof

        let n be Element of NAT ;

        ((n + 1) " ) > 0 ;

        then (1 / (n + 1)) > 0 by XCMPLX_1: 215;

        then

        consider r0 be Real such that

         A3: r0 in R and

         A4: (rs - (1 / (n + 1)) qua Real) < r0 by A1, SEQ_4:def 1;

        for r00 be Real st r00 = r0 holds (rs - (1 / (n + 1)) qua Real) < r00 by A4;

        hence thesis by A3;

      end;

      ex s1 be sequence of REAL st for n be Element of NAT holds X[n, (s1 . n)] from FUNCT_2:sch 3( A2);

      then

      consider s1 be sequence of REAL such that

       A5: for n be Element of NAT holds (s1 . n) in R & for r0 be Real st r0 = (s1 . n) holds (rs - (1 / (n + 1)) qua Real) < r0;

      defpred P[ set, set, set] means ($2 is Real implies (for r1,r2 be Real, n1 be Nat st r1 = $2 & r2 = (s1 . (n1 + 1)) & n1 = $1 holds (r1 >= r2 implies $3 = $2) & (r1 < r2 implies $3 = (s1 . (n1 + 1))))) & ( not $2 is Real implies $3 = 1);

      

       A6: for n be Nat holds for x be set holds ex y be set st P[n, x, y]

      proof

        let n be Nat;

        thus for x be set holds ex y be set st P[n, x, y]

        proof

          let x be set;

          now

            per cases ;

              case not x is Real;

              hence thesis;

            end;

              case

               A7: x is Real;

              then

              reconsider r10 = x as Real;

              reconsider r20 = (s1 . (n + 1)) as Real;

              now

                per cases ;

                  case r10 >= r20;

                  then for r1,r2 be Real, n1 be Nat st r1 = x & r2 = (s1 . (n1 + 1)) & n1 = n holds (r1 >= r2 implies x = x) & (r1 < r2 implies x = (s1 . (n1 + 1)));

                  hence thesis by A7;

                end;

                  case r10 < r20;

                  then for r1,r2 be Real, n1 be Nat st r1 = x & r2 = (s1 . (n1 + 1)) & n1 = n holds (r1 >= r2 implies (s1 . (n + 1)) = x) & (r1 < r2 implies (s1 . (n + 1)) = (s1 . (n1 + 1)));

                  hence thesis by A7;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      ex f be Function st ( dom f) = NAT & (f . 0 ) = (s1 . 0 ) & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 1( A6);

      then

      consider s2 be Function such that

       A8: ( dom s2) = NAT and

       A9: (s2 . 0 ) = (s1 . 0 ) and

       A10: for n be Nat holds P[n, (s2 . n), (s2 . (n + 1))];

      

       A11: ( rng s2) c= REAL

      proof

        defpred X[ Nat] means (s2 . $1) in REAL ;

        let y be object;

        assume y in ( rng s2);

        then

        consider x be object such that

         A12: x in ( dom s2) and

         A13: y = (s2 . x) by FUNCT_1:def 3;

        reconsider n = x as Nat by A8, A12;

        

         A14: for k be Nat st X[k] holds X[(k + 1)]

        proof

          let k be Nat;

          reconsider r2 = (s1 . (k + 1)) as Real;

          assume

           A15: (s2 . k) in REAL ;

          then

          reconsider r1 = (s2 . k) as Real;

          now

            per cases ;

              case r1 >= r2;

              hence thesis by A10, A15;

            end;

              case r1 < r2;

              then (s2 . (k + 1)) = (s1 . (k + 1)) by A10;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        

         A16: X[ 0 ] by A9;

        for m be Nat holds X[m] from NAT_1:sch 2( A16, A14);

        then (s2 . n) in REAL ;

        hence thesis by A13;

      end;

      then

      reconsider s3 = s2 as Real_Sequence by A8, FUNCT_2: 2;

      defpred X[ Nat] means (s1 . $1) <= (s3 . $1);

      

       A17: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat;

        

         A18: k in NAT by ORDINAL1:def 12;

        assume (s1 . k) <= (s3 . k);

        reconsider r2 = (s1 . (k + 1)) as Real;

        (s2 . k) in ( rng s2) by A8, FUNCT_1:def 3, A18;

        then

        reconsider r1 = (s2 . k) as Real by A11;

        now

          per cases ;

            case r1 >= r2;

            hence thesis by A10;

          end;

            case r1 < r2;

            hence thesis by A10;

          end;

        end;

        hence thesis;

      end;

      

       A19: X[ 0 ] by A9;

      

       A20: for n4 be Nat holds X[n4] from NAT_1:sch 2( A19, A17);

      defpred X[ Nat] means 0 <= $1 implies (s3 . 0 ) <= (s3 . $1);

      

       A21: for n4 be Nat holds (s3 . n4) <= (s3 . (n4 + 1))

      proof

        let n4 be Nat;

        reconsider r2 = (s1 . (n4 + 1)) as Real;

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

        then

        reconsider r1 = (s2 . n4) as Real;

        now

          per cases ;

            case r1 >= r2;

            hence thesis by A10;

          end;

            case r1 < r2;

            hence thesis by A10;

          end;

        end;

        hence thesis;

      end;

      

       A22: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat;

        assume

         A23: 0 <= k implies (s3 . 0 ) <= (s3 . k);

        now

          assume 0 <= (k + 1);

          

           A24: (s3 . k) <= (s3 . (k + 1)) by A21;

          now

            per cases ;

              case 0 < k;

              thus (s3 . 0 ) <= (s3 . (k + 1)) by A23, A24, XXREAL_0: 2;

            end;

              case 0 = k;

              hence (s3 . 0 ) <= (s3 . (k + 1)) by A21;

            end;

          end;

          hence (s3 . 0 ) <= (s3 . (k + 1));

        end;

        hence thesis;

      end;

      defpred Y[ Nat] means for n4 be Nat st $1 <= n4 holds (s3 . $1) <= (s3 . n4);

      

       A25: for k be Nat st Y[k] holds Y[(k + 1)]

      proof

        let k be Nat;

        assume for n5 be Nat st k <= n5 holds (s3 . k) <= (s3 . n5);

        defpred Z[ Nat] means (k + 1) <= $1 implies (s3 . (k + 1)) <= (s3 . $1);

        

         A26: for i be Nat st Z[i] holds Z[(i + 1)]

        proof

          let i be Nat;

          

           A27: i in NAT by ORDINAL1:def 12;

          reconsider r2 = (s1 . (i + 1)) as Real;

          (s2 . i) in ( rng s2) by A8, FUNCT_1:def 3, A27;

          then

          reconsider r1 = (s2 . i) as Real by A11;

           A28:

          now

            per cases ;

              case r1 >= r2;

              hence (s3 . i) <= (s3 . (i + 1)) by A10;

            end;

              case r1 < r2;

              hence (s3 . i) <= (s3 . (i + 1)) by A10;

            end;

          end;

          assume

           A29: (k + 1) <= i implies (s3 . (k + 1)) <= (s3 . i);

          now

            assume

             A30: (k + 1) <= (i + 1);

            now

              per cases by A30, XXREAL_0: 1;

                case (k + 1) < (i + 1);

                hence (s3 . (k + 1)) <= (s3 . (i + 1)) by A29, A28, NAT_1: 13, XXREAL_0: 2;

              end;

                case (k + 1) = (i + 1);

                hence (s3 . (k + 1)) <= (s3 . (i + 1));

              end;

            end;

            hence (s3 . (k + 1)) <= (s3 . (i + 1));

          end;

          hence thesis;

        end;

        

         A31: Z[ 0 ];

        for n4 be Nat holds Z[n4] from NAT_1:sch 2( A31, A26);

        hence thesis;

      end;

      

       A32: X[ 0 ];

      for n4 be Nat holds X[n4] from NAT_1:sch 2( A32, A22);

      then

       A33: Y[ 0 ];

      for m4 be Nat holds Y[m4] from NAT_1:sch 2( A33, A25);

      then for m4,n4 be Nat st m4 in ( dom s3) & n4 in ( dom s3) & m4 <= n4 holds (s3 . m4) <= (s3 . n4);

      then

       A34: s3 is non-decreasing by SEQM_3:def 3;

      

       A35: ( rng s3) c= R

      proof

        defpred X[ set] means (s3 . $1) in R;

        let y be object;

        assume y in ( rng s3);

        then

         A36: ex x be object st x in ( dom s3) & y = (s3 . x) by FUNCT_1:def 3;

        

         A37: for k be Nat st X[k] holds X[(k + 1)]

        proof

          let k be Nat;

          

           A38: k in NAT by ORDINAL1:def 12;

          reconsider r2 = (s1 . (k + 1)) as Real;

          (s2 . k) in ( rng s2) by A8, FUNCT_1:def 3, A38;

          then

          reconsider r1 = (s2 . k) as Real by A11;

          assume

           A39: (s3 . k) in R;

          now

            per cases ;

              case r1 >= r2;

              hence thesis by A10, A39;

            end;

              case r1 < r2;

              then (s2 . (k + 1)) = (s1 . (k + 1)) by A10;

              hence thesis by A5;

            end;

          end;

          hence thesis;

        end;

        

         A40: X[ 0 ] by A5, A9;

        for nn be Nat holds X[nn] from NAT_1:sch 2( A40, A37);

        hence thesis by A36;

      end;

      for n be Nat holds (s3 . n) < (( upper_bound R) + 1)

      proof

        let n be Nat;

        

         A41: n in NAT by ORDINAL1:def 12;

        (s3 . n) in ( rng s3) by A8, FUNCT_1:def 3, A41;

        then

         A42: (s3 . n) <= ( upper_bound R) by A1, A35, SEQ_4:def 1;

        ( upper_bound R) < (( upper_bound R) + 1) by XREAL_1: 29;

        hence thesis by A42, XXREAL_0: 2;

      end;

      then

       A43: s3 is bounded_above by SEQ_2:def 3;

      

       A44: for r be Real st r > 0 holds (( upper_bound R) - r) < ( lim s3)

      proof

        let r be Real;

        assume

         A45: r > 0 ;

        consider n2 be Nat such that

         A46: (1 / r) < n2 by SEQ_4: 3;

        

         A47: n2 in NAT by ORDINAL1:def 12;

        n2 < (n2 + 1) by XREAL_1: 29;

        then (1 / r) < (n2 + 1) by A46, XXREAL_0: 2;

        then ((1 / r) * r) < ((n2 + 1) * r) by A45, XREAL_1: 68;

        then 1 < ((n2 + 1) * r) by A45, XCMPLX_1: 106;

        then (1 / (n2 + 1)) < (((n2 + 1) * r) / (n2 + 1)) by XREAL_1: 74;

        then (1 / (n2 + 1)) < r by XCMPLX_1: 89;

        then (rs - (1 / (n2 + 1))) > (rs - r) by XREAL_1: 10;

        then

         A48: (rs - r) < (s1 . n2) by A5, XXREAL_0: 2, A47;

        

         A49: (s3 . n2) <= ( lim s3) by A34, A43, SEQ_4: 37;

        (s1 . n2) <= (s3 . n2) by A20;

        then (rs - r) < (s3 . n2) by A48, XXREAL_0: 2;

        hence thesis by A49, XXREAL_0: 2;

      end;

       A50:

      now

        reconsider r = (( upper_bound R) - ( lim s3)) as Real;

        assume ( upper_bound R) > ( lim s3);

        then r > 0 by XREAL_1: 50;

        then (( upper_bound R) - r) < ( lim s3) by A44;

        hence contradiction;

      end;

      

       A51: for n be Nat holds (s3 . n) <= ( upper_bound R)

      proof

        let n be Nat;

        

         A52: n in NAT by ORDINAL1:def 12;

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

        then (s3 . n) in ( rng s3) by FUNCT_1:def 3, A52;

        hence thesis by A1, A35, SEQ_4:def 1;

      end;

      for n be Nat holds (s3 . n) < (( upper_bound R) + 1)

      proof

        let n be Nat;

        ( upper_bound R) < (( upper_bound R) + 1) & (s3 . n) <= ( upper_bound R) by A51, XREAL_1: 29;

        hence thesis by XXREAL_0: 2;

      end;

      then

       A53: s3 is bounded_above by SEQ_2:def 3;

      then ( lim s3) <= ( upper_bound R) by A34, A51, PREPOWER: 2;

      hence thesis by A34, A35, A53, A50, XXREAL_0: 1;

    end;

    theorem :: TOPMETR3:12

    

     Th12: for R be non empty Subset of REAL st R is bounded_below holds ex s be Real_Sequence st s is non-increasing convergent & ( rng s) c= R & ( lim s) = ( lower_bound R)

    proof

      let R be non empty Subset of REAL ;

      reconsider rs = ( lower_bound R) as Real;

      defpred X[ Nat, Real] means ($2 in R & (for r00 be Real st r00 = $2 holds (rs + (1 / ($1 + 1)) qua Real) > r00));

      assume

       A1: R is bounded_below;

      

       A2: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

      proof

        let n be Element of NAT ;

        ((n + 1) " ) > 0 ;

        then (1 / (n + 1)) > 0 by XCMPLX_1: 215;

        then

        consider r0 be Real such that

         A3: r0 in R and

         A4: (rs + (1 / (n + 1)) qua Real) > r0 by A1, SEQ_4:def 2;

        for r00 be Real st r00 = r0 holds (rs + (1 / (n + 1)) qua Real) > r00 by A4;

        hence thesis by A3;

      end;

      ex s1 be sequence of REAL st for n be Element of NAT holds X[n, (s1 . n)] from FUNCT_2:sch 3( A2);

      then

      consider s1 be sequence of REAL such that

       A5: for n be Element of NAT holds (s1 . n) in R & for r0 be Real st r0 = (s1 . n) holds (rs + (1 / (n + 1)) qua Real) > r0;

      defpred P[ set, set, set] means ($2 is Real implies (for r1,r2 be Real, n1 be Nat st r1 = $2 & r2 = (s1 . (n1 + 1)) & n1 = $1 holds (r1 <= r2 implies $3 = $2) & (r1 > r2 implies $3 = (s1 . (n1 + 1))))) & ( not $2 is Real implies $3 = 1);

      

       A6: for n be Nat holds for x be set holds ex y be set st P[n, x, y]

      proof

        let n be Nat;

        thus for x be set holds ex y be set st P[n, x, y]

        proof

          let x be set;

          now

            per cases ;

              case not x is Real;

              hence ex y be set st (x is Real implies for r1,r2 be Real, n1 be Nat st r1 = x & r2 = (s1 . (n1 + 1)) & n1 = n holds (r1 >= r2 implies y = x) & (r1 < r2 implies y = (s1 . (n1 + 1)))) & ( not x is Real implies y = 1);

            end;

              case

               A7: x is Real;

              then

              reconsider r10 = x as Real;

              reconsider r20 = (s1 . (n + 1)) as Real;

              now

                per cases ;

                  case r10 <= r20;

                  then for r1,r2 be Real, n1 be Nat st r1 = x & r2 = (s1 . (n1 + 1)) & n1 = n holds (r1 <= r2 implies x = x) & (r1 > r2 implies x = (s1 . (n1 + 1)));

                  hence thesis by A7;

                end;

                  case r10 > r20;

                  then for r1,r2 be Real, n1 be Nat st r1 = x & r2 = (s1 . (n1 + 1)) & n1 = n holds (r1 <= r2 implies (s1 . (n + 1)) = x) & (r1 > r2 implies (s1 . (n + 1)) = (s1 . (n1 + 1)));

                  hence thesis by A7;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      ex f be Function st ( dom f) = NAT & (f . 0 ) = (s1 . 0 ) & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 1( A6);

      then

      consider s2 be Function such that

       A8: ( dom s2) = NAT and

       A9: (s2 . 0 ) = (s1 . 0 ) and

       A10: for n be Nat holds P[n, (s2 . n), (s2 . (n + 1))];

      

       A11: ( rng s2) c= REAL

      proof

        defpred X[ Nat] means (s2 . $1) in REAL ;

        let y be object;

        assume y in ( rng s2);

        then

        consider x be object such that

         A12: x in ( dom s2) and

         A13: y = (s2 . x) by FUNCT_1:def 3;

        reconsider n = x as Nat by A8, A12;

        

         A14: for k be Nat st X[k] holds X[(k + 1)]

        proof

          let k be Nat;

          reconsider r2 = (s1 . (k + 1)) as Real;

          assume

           A15: (s2 . k) in REAL ;

          then

          reconsider r1 = (s2 . k) as Real;

          now

            per cases ;

              case r1 <= r2;

              hence thesis by A10, A15;

            end;

              case r1 > r2;

              then (s2 . (k + 1)) = (s1 . (k + 1)) by A10;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        

         A16: X[ 0 ] by A9;

        for m be Nat holds X[m] from NAT_1:sch 2( A16, A14);

        then (s2 . n) in REAL ;

        hence thesis by A13;

      end;

      then

      reconsider s3 = s2 as Real_Sequence by A8, FUNCT_2: 2;

      defpred X[ Nat] means (s1 . $1) >= (s3 . $1);

      

       A17: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat;

        

         A18: k in NAT by ORDINAL1:def 12;

        assume (s1 . k) >= (s3 . k);

        reconsider r2 = (s1 . (k + 1)) as Real;

        (s2 . k) in ( rng s2) by A8, FUNCT_1:def 3, A18;

        then

        reconsider r1 = (s2 . k) as Real by A11;

        now

          per cases ;

            case r1 <= r2;

            hence thesis by A10;

          end;

            case r1 > r2;

            hence thesis by A10;

          end;

        end;

        hence thesis;

      end;

      

       A19: X[ 0 ] by A9;

      

       A20: for n4 be Nat holds X[n4] from NAT_1:sch 2( A19, A17);

      defpred X[ Nat] means 0 <= $1 implies (s3 . 0 ) >= (s3 . $1);

      

       A21: for n4 be Nat holds (s3 . n4) >= (s3 . (n4 + 1))

      proof

        let n4 be Nat;

        reconsider r2 = (s1 . (n4 + 1)) as Real;

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

        then

        reconsider r1 = (s2 . n4) as Real;

        now

          per cases ;

            case r1 <= r2;

            hence thesis by A10;

          end;

            case r1 > r2;

            hence thesis by A10;

          end;

        end;

        hence thesis;

      end;

      

       A22: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat;

        assume

         A23: 0 <= k implies (s3 . 0 ) >= (s3 . k);

        now

          assume 0 <= (k + 1);

          

           A24: (s3 . k) >= (s3 . (k + 1)) by A21;

          now

            per cases ;

              case 0 < (k + 1);

              thus (s3 . 0 ) >= (s3 . (k + 1)) by A23, A24, XXREAL_0: 2;

            end;

              case 0 = (k + 1);

              hence (s3 . 0 ) >= (s3 . (k + 1));

            end;

          end;

          hence (s3 . 0 ) >= (s3 . (k + 1));

        end;

        hence thesis;

      end;

      defpred Y[ Nat] means for n4 be Nat st $1 <= n4 holds (s3 . $1) >= (s3 . n4);

      

       A25: for k be Nat st Y[k] holds Y[(k + 1)]

      proof

        let k be Nat;

        assume for n5 be Nat st k <= n5 holds (s3 . k) >= (s3 . n5);

        defpred X[ Nat] means (k + 1) <= $1 implies (s3 . (k + 1)) >= (s3 . $1);

        

         A26: for i be Nat st X[i] holds X[(i + 1)]

        proof

          let i be Nat;

          

           A27: i in NAT by ORDINAL1:def 12;

          reconsider r2 = (s1 . (i + 1)) as Real;

          (s2 . i) in ( rng s2) by A8, FUNCT_1:def 3, A27;

          then

          reconsider r1 = (s2 . i) as Real by A11;

           A28:

          now

            per cases ;

              case r1 <= r2;

              hence (s3 . i) >= (s3 . (i + 1)) by A10;

            end;

              case r1 > r2;

              hence (s3 . i) >= (s3 . (i + 1)) by A10;

            end;

          end;

          assume

           A29: (k + 1) <= i implies (s3 . (k + 1)) >= (s3 . i);

          now

            assume

             A30: (k + 1) <= (i + 1);

            now

              per cases by A30, XXREAL_0: 1;

                case (k + 1) < (i + 1);

                hence (s3 . (k + 1)) >= (s3 . (i + 1)) by A29, A28, NAT_1: 13, XXREAL_0: 2;

              end;

                case (k + 1) = (i + 1);

                hence (s3 . (k + 1)) >= (s3 . (i + 1));

              end;

            end;

            hence (s3 . (k + 1)) >= (s3 . (i + 1));

          end;

          hence thesis;

        end;

        

         A31: X[ 0 ];

        thus for n4 be Nat holds X[n4] from NAT_1:sch 2( A31, A26);

      end;

      

       A32: X[ 0 ];

      for n4 be Nat holds X[n4] from NAT_1:sch 2( A32, A22);

      then

       A33: Y[ 0 ];

      for m4 be Nat holds Y[m4] from NAT_1:sch 2( A33, A25);

      then for m4,n4 be Nat st m4 in ( dom s3) & n4 in ( dom s3) & m4 <= n4 holds (s3 . m4) >= (s3 . n4);

      then

       A34: s3 is non-increasing by SEQM_3:def 4;

      

       A35: ( rng s3) c= R

      proof

        defpred Z[ Nat] means (s3 . $1) in R;

        let y be object;

        assume y in ( rng s3);

        then

         A36: ex x be object st x in ( dom s3) & y = (s3 . x) by FUNCT_1:def 3;

        

         A37: for k be Nat st Z[k] holds Z[(k + 1)]

        proof

          let k be Nat;

          

           A38: k in NAT by ORDINAL1:def 12;

          reconsider r2 = (s1 . (k + 1)) as Real;

          (s2 . k) in ( rng s2) by A8, FUNCT_1:def 3, A38;

          then

          reconsider r1 = (s2 . k) as Real by A11;

          assume

           A39: (s3 . k) in R;

          now

            per cases ;

              case r1 <= r2;

              hence thesis by A10, A39;

            end;

              case r1 > r2;

              then (s2 . (k + 1)) = (s1 . (k + 1)) by A10;

              hence thesis by A5;

            end;

          end;

          hence thesis;

        end;

        

         A40: Z[ 0 ] by A5, A9;

        for nn be Nat holds Z[nn] from NAT_1:sch 2( A40, A37);

        hence thesis by A36;

      end;

      for n be Nat holds (s3 . n) > (( lower_bound R) - 1)

      proof

        let n be Nat;

        

         A41: n in NAT by ORDINAL1:def 12;

        ( lower_bound R) < (( lower_bound R) + 1) by XREAL_1: 29;

        then

         A42: ( lower_bound R) > (( lower_bound R) - 1) by XREAL_1: 19;

        (s3 . n) in ( rng s3) by A8, FUNCT_1:def 3, A41;

        then (s3 . n) >= ( lower_bound R) by A1, A35, SEQ_4:def 2;

        hence thesis by A42, XXREAL_0: 2;

      end;

      then

       A43: s3 is bounded_below by SEQ_2:def 4;

      

       A44: for r be Real st r > 0 holds (( lower_bound R) + r) > ( lim s3)

      proof

        let r be Real;

        assume

         A45: r > 0 ;

        consider n2 be Nat such that

         A46: (1 / r) < n2 by SEQ_4: 3;

        

         A47: n2 in NAT by ORDINAL1:def 12;

        n2 < (n2 + 1) by XREAL_1: 29;

        then (1 / r) < (n2 + 1) by A46, XXREAL_0: 2;

        then ((1 / r) * r) < ((n2 + 1) * r) by A45, XREAL_1: 68;

        then 1 < ((n2 + 1) * r) by A45, XCMPLX_1: 106;

        then (1 / (n2 + 1)) < (((n2 + 1) * r) / (n2 + 1)) by XREAL_1: 74;

        then (1 / (n2 + 1)) < r by XCMPLX_1: 89;

        then (rs + (1 / (n2 + 1))) < (rs + r) by XREAL_1: 8;

        then

         A48: (rs + r) > (s1 . n2) by A5, XXREAL_0: 2, A47;

        

         A49: (s3 . n2) >= ( lim s3) by A34, A43, SEQ_4: 38;

        (s1 . n2) >= (s3 . n2) by A20;

        then (rs + r) > (s3 . n2) by A48, XXREAL_0: 2;

        hence thesis by A49, XXREAL_0: 2;

      end;

       A50:

      now

        reconsider r = (( lim s3) - ( lower_bound R)) as Real;

        assume ( lower_bound R) < ( lim s3);

        then r > 0 by XREAL_1: 50;

        then (( lower_bound R) + (( lim s3) + ( - ( lower_bound R)))) > ( lim s3) by A44;

        hence contradiction;

      end;

      

       A51: for n be Nat holds (s3 . n) >= ( lower_bound R)

      proof

        let n be Nat;

        

         A52: n in NAT by ORDINAL1:def 12;

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

        then (s3 . n) in ( rng s3) by FUNCT_1:def 3, A52;

        hence thesis by A1, A35, SEQ_4:def 2;

      end;

      for n be Nat holds (s3 . n) > (( lower_bound R) - 1)

      proof

        let n be Nat;

        ( lower_bound R) < (( lower_bound R) + 1) by XREAL_1: 29;

        then

         A53: ( lower_bound R) > (( lower_bound R) - 1) by XREAL_1: 19;

        (s3 . n) >= ( lower_bound R) by A51;

        hence thesis by A53, XXREAL_0: 2;

      end;

      then

       A54: s3 is bounded_below by SEQ_2:def 4;

      then ( lim s3) >= ( lower_bound R) by A34, A51, PREPOWER: 1;

      hence thesis by A34, A35, A54, A50, XXREAL_0: 1;

    end;

    theorem :: TOPMETR3:13

    

     Th13: for X be non empty MetrSpace, f be Function of I[01] , ( TopSpaceMetr X), F1,F2 be Subset of ( TopSpaceMetr X), r1,r2 be Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & (f . r1) in F1 & (f . r2) in F2 & F1 is closed & F2 is closed & f is continuous & (F1 \/ F2) = the carrier of X holds ex r be Real st r1 <= r & r <= r2 & (f . r) in (F1 /\ F2)

    proof

      let X be non empty MetrSpace, f be Function of I[01] , ( TopSpaceMetr X), F1,F2 be Subset of ( TopSpaceMetr X), r1,r2 be Real;

      assume that

       A1: 0 <= r1 and

       A2: r2 <= 1 and

       A3: r1 <= r2 & (f . r1) in F1 and

       A4: (f . r2) in F2 and

       A5: F1 is closed and

       A6: F2 is closed and

       A7: f is continuous and

       A8: (F1 \/ F2) = the carrier of X;

      

       A9: r1 in { r3 where r3 be Real : r1 <= r3 & r3 <= r2 & (f . r3) in F1 } by A3;

      { r3 where r3 be Real : r1 <= r3 & r3 <= r2 & (f . r3) in F1 } c= REAL

      proof

        let x be object;

        assume x in { r3 where r3 be Real : r1 <= r3 & r3 <= r2 & (f . r3) in F1 };

        then ex r3 be Real st r3 = x & r1 <= r3 & r3 <= r2 & (f . r3) in F1;

        hence thesis by XREAL_0:def 1;

      end;

      then

      reconsider R = { r3 where r3 be Real : r1 <= r3 & r3 <= r2 & (f . r3) in F1 } as non empty Subset of REAL by A9;

      

       A10: for r be Real st r in R holds r <= r2

      proof

        let r be Real;

        assume r in R;

        then ex r3 be Real st r3 = r & r1 <= r3 & r3 <= r2 & (f . r3) in F1;

        hence thesis;

      end;

      r2 is UpperBound of R

      proof

        let r be ExtReal;

        assume r in R;

        then ex r3 be Real st r3 = r & r1 <= r3 & r3 <= r2 & (f . r3) in F1;

        hence thesis;

      end;

      then

       A11: R is bounded_above;

      then

      consider s1 be Real_Sequence such that

       A12: s1 is non-decreasing convergent and

       A13: ( rng s1) c= R and

       A14: ( lim s1) = ( upper_bound R) by Th11;

      { r3 where r3 be Real : r1 <= r3 & r3 <= r2 & (f . r3) in F1 } c= [. 0 , 1.]

      proof

        let x be object;

        assume x in { r3 where r3 be Real : r1 <= r3 & r3 <= r2 & (f . r3) in F1 };

        then

        consider r3 be Real such that

         A15: r3 = x & r1 <= r3 and

         A16: r3 <= r2 and (f . r3) in F1;

        r3 <= 1 by A2, A16, XXREAL_0: 2;

        hence thesis by A1, A15, XXREAL_1: 1;

      end;

      then

      reconsider S1 = s1 as sequence of ( Closed-Interval-MSpace ( 0 ,1)) by A13, Th5, XBOOLE_1: 1;

      

       A17: I[01] = ( TopSpaceMetr ( Closed-Interval-MSpace ( 0 ,1))) by TOPMETR: 20, TOPMETR:def 7;

      then

      reconsider S00 = (f * S1) as sequence of X by Th2;

      

       A18: S00 is convergent by A7, A12, A17, Th3, Th8;

      ( dom f) = the carrier of I[01] by FUNCT_2:def 1

      .= the carrier of ( Closed-Interval-MSpace ( 0 ,1)) by A17, TOPMETR: 12;

      then (f . ( lim S1)) in ( rng f) by FUNCT_1: 3;

      then

      reconsider t1 = (f . ( lim S1)) as Point of X by TOPMETR: 12;

      reconsider S2 = s1 as sequence of RealSpace by METRIC_1:def 13;

      

       A19: S1 is convergent by A12, Th8;

      then S2 is convergent by Th7;

      then ( lim S2) = ( lim S1) by Th7;

      then

       A20: ( lim s1) = ( lim S1) by A12, Th4;

      

       A21: for r be Real st r > 0 holds ex n be Nat st for m be Nat st m >= n holds ( dist ((S00 . m),t1)) < r

      proof

        let r be Real;

        assume r > 0 ;

        then

        consider r7 be Real such that

         A22: r7 > 0 and

         A23: for w be Point of ( Closed-Interval-MSpace ( 0 ,1)), w1 be Point of X st w1 = (f . w) & ( dist (( lim S1),w)) < r7 holds ( dist (t1,w1)) < r by A7, A17, UNIFORM1: 4;

        consider n0 be Nat such that

         A24: for m be Nat st m >= n0 holds ( dist ((S1 . m),( lim S1))) < r7 by A19, A22, TBSP_1:def 3;

        for m be Nat st m >= n0 holds ( dist ((S00 . m),t1)) < r

        proof

          let m be Nat;

          

           A25: m in NAT by ORDINAL1:def 12;

          ( dom S00) = NAT by TBSP_1: 4;

          then

           A26: (S00 . m) = (f . (S1 . m)) by FUNCT_1: 12, A25;

          assume m >= n0;

          then ( dist (( lim S1),(S1 . m))) < r7 by A24;

          hence thesis by A23, A26;

        end;

        hence thesis;

      end;

      

       A27: r2 >= ( upper_bound R) by A10, SEQ_4: 144;

      then

       A28: r2 in { r3 where r3 be Real : ( upper_bound R) <= r3 & r3 <= r2 & (f . r3) in F2 } by A4;

      { r3 where r3 be Real : ( upper_bound R) <= r3 & r3 <= r2 & (f . r3) in F2 } c= REAL

      proof

        let x be object;

        assume x in { r3 where r3 be Real : ( upper_bound R) <= r3 & r3 <= r2 & (f . r3) in F2 };

        then ex r3 be Real st r3 = x & ( upper_bound R) <= r3 & r3 <= r2 & (f . r3) in F2;

        hence thesis by XREAL_0:def 1;

      end;

      then

      reconsider R2 = { r3 where r3 be Real : ( upper_bound R) <= r3 & r3 <= r2 & (f . r3) in F2 } as non empty Subset of REAL by A28;

      

       A29: for r be Real st r in R2 holds r >= ( upper_bound R)

      proof

        let r be Real;

        assume r in R2;

        then ex r3 be Real st r3 = r & ( upper_bound R) <= r3 & r3 <= r2 & (f . r3) in F2;

        hence thesis;

      end;

      ( upper_bound R) is LowerBound of R2

      proof

        let r be ExtReal;

        assume r in R2;

        then ex r3 be Real st r3 = r & ( upper_bound R) <= r3 & r3 <= r2 & (f . r3) in F2;

        hence thesis;

      end;

      then

       A30: R2 is bounded_below;

      then

      consider s2 be Real_Sequence such that

       A31: s2 is non-increasing convergent and

       A32: ( rng s2) c= R2 and

       A33: ( lim s2) = ( lower_bound R2) by Th12;

      

       A34: 0 <= ( upper_bound R) by A1, A9, A11, SEQ_4:def 1;

      { r3 where r3 be Real : ( upper_bound R) <= r3 & r3 <= r2 & (f . r3) in F2 } c= [. 0 , 1.]

      proof

        let x be object;

        assume x in { r3 where r3 be Real : ( upper_bound R) <= r3 & r3 <= r2 & (f . r3) in F2 };

        then

        consider r3 be Real such that

         A35: r3 = x & ( upper_bound R) <= r3 and

         A36: r3 <= r2 and (f . r3) in F2;

        r3 <= 1 by A2, A36, XXREAL_0: 2;

        hence thesis by A34, A35, XXREAL_1: 1;

      end;

      then

      reconsider S1 = s2 as sequence of ( Closed-Interval-MSpace ( 0 ,1)) by A32, Th5, XBOOLE_1: 1;

      reconsider S2 = s2 as sequence of RealSpace by METRIC_1:def 13;

      

       A37: S1 is convergent by A31, Th8;

      then S2 is convergent by Th7;

      then ( lim S2) = ( lim S1) by Th7;

      then

       A38: ( lim s2) = ( lim S1) by A31, Th4;

      for n4 be Nat holds (S00 . n4) in F1

      proof

        let n4 be Nat;

        

         A39: n4 in NAT by ORDINAL1:def 12;

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

        then (s1 . n4) in ( rng s1) by FUNCT_1:def 3, A39;

        then (s1 . n4) in R by A13;

        then ( dom S00) = NAT & ex r3 be Real st r3 = (s1 . n4) & r1 <= r3 & r3 <= r2 & (f . r3) in F1 by TBSP_1: 4;

        hence thesis by FUNCT_1: 12, A39;

      end;

      then ( lim S00) in F1 by A5, A7, A19, A17, Th1, Th3;

      then

       A40: (f . ( lim s1)) in F1 by A20, A18, A21, TBSP_1:def 3;

      

       A41: I[01] = ( TopSpaceMetr ( Closed-Interval-MSpace ( 0 ,1))) by TOPMETR: 20, TOPMETR:def 7;

      then

      reconsider S00 = (f * S1) as sequence of X by Th2;

      ( dom f) = the carrier of I[01] by FUNCT_2:def 1

      .= the carrier of ( Closed-Interval-MSpace ( 0 ,1)) by A41, TOPMETR: 12;

      then (f . ( lim S1)) in ( rng f) by FUNCT_1: 3;

      then

      reconsider t1 = (f . ( lim S1)) as Point of X by TOPMETR: 12;

      

       A42: for r be Real st r > 0 holds ex n be Nat st for m be Nat st m >= n holds ( dist ((S00 . m),t1)) < r

      proof

        let r be Real;

        assume r > 0 ;

        then

        consider r7 be Real such that

         A43: r7 > 0 and

         A44: for w be Point of ( Closed-Interval-MSpace ( 0 ,1)), w1 be Point of X st w1 = (f . w) & ( dist (( lim S1),w)) < r7 holds ( dist (t1,w1)) < r by A7, A41, UNIFORM1: 4;

        consider n0 be Nat such that

         A45: for m be Nat st m >= n0 holds ( dist ((S1 . m),( lim S1))) < r7 by A37, A43, TBSP_1:def 3;

        for m be Nat st m >= n0 holds ( dist ((S00 . m),t1)) < r

        proof

          let m be Nat;

          

           A46: m in NAT by ORDINAL1:def 12;

          ( dom S00) = NAT by TBSP_1: 4;

          then

           A47: (S00 . m) = (f . (S1 . m)) by FUNCT_1: 12, A46;

          assume m >= n0;

          then ( dist (( lim S1),(S1 . m))) < r7 by A45;

          hence thesis by A44, A47;

        end;

        hence thesis;

      end;

      

       A48: r1 <= ( upper_bound R) by A9, A11, SEQ_4:def 1;

      for s be Real st 0 < s holds ex r be Real st r in R2 & r < (( upper_bound R) + s)

      proof

        let s be Real;

        assume

         A49: 0 < s;

        now

          assume

           A50: for r be Real st r < (( upper_bound R) + s) holds not r in R2;

          now

            per cases by A27, XREAL_1: 48;

              case (r2 - ( upper_bound R)) = 0 ;

              hence contradiction by A28, A49, A50, XREAL_1: 29;

            end;

              case

               A51: (r2 - ( upper_bound R)) > 0 ;

              set rs0 = ( min ((r2 - ( upper_bound R)),s));

              set r0 = (( upper_bound R) + (rs0 / 2));

              

               A52: rs0 > 0 by A49, A51, XXREAL_0: 21;

              then

               A53: ( upper_bound R) < r0 by XREAL_1: 29, XREAL_1: 215;

              rs0 <= (r2 - ( upper_bound R)) by XXREAL_0: 17;

              then

               A54: (( upper_bound R) + rs0) <= (( upper_bound R) + (r2 - ( upper_bound R))) by XREAL_1: 7;

              

               A55: (rs0 / 2) < rs0 by A52, XREAL_1: 216;

              then (( upper_bound R) + (rs0 / 2)) < (( upper_bound R) + rs0) by XREAL_1: 8;

              then

               A56: r0 <= r2 by A54, XXREAL_0: 2;

              then r0 <= 1 by A2, XXREAL_0: 2;

              then r0 in the carrier of I[01] by A1, A48, A52, BORSUK_1: 40, XXREAL_1: 1;

              then r0 in ( dom f) by FUNCT_2:def 1;

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

              then (f . r0) in the carrier of ( TopSpaceMetr X);

              then (f . r0) in the carrier of X by TOPMETR: 12;

              then

               A57: (f . r0) in F1 or (f . r0) in F2 by A8, XBOOLE_0:def 3;

              ( upper_bound R) <= (( upper_bound R) + (rs0 / 2)) by A52, XREAL_1: 29, XREAL_1: 215;

              then

               A58: r1 <= r0 by A48, XXREAL_0: 2;

              rs0 <= s by XXREAL_0: 17;

              then (rs0 / 2) < s by A55, XXREAL_0: 2;

              then r0 < (( upper_bound R) + s) by XREAL_1: 8;

              then

               A59: not r0 in R2 by A50;

              ( upper_bound R) < r0 by A52, XREAL_1: 29, XREAL_1: 215;

              then r0 in R by A59, A58, A56, A57;

              hence contradiction by A11, A53, SEQ_4:def 1;

            end;

          end;

          hence contradiction;

        end;

        hence thesis;

      end;

      then

       A60: ( upper_bound R) = ( lower_bound R2) by A29, A30, SEQ_4:def 2;

      S00 is convergent by A7, A31, A41, Th3, Th8;

      then

       A61: (f . ( lim S1)) = ( lim S00) by A42, TBSP_1:def 3;

      for n4 be Nat holds (S00 . n4) in F2

      proof

        let n4 be Nat;

        

         A62: n4 in NAT by ORDINAL1:def 12;

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

        then (s2 . n4) in ( rng s2) by FUNCT_1:def 3, A62;

        then (s2 . n4) in R2 by A32;

        then ( dom S00) = NAT & ex r3 be Real st r3 = (s2 . n4) & ( upper_bound R) <= r3 & r3 <= r2 & (f . r3) in F2 by TBSP_1: 4;

        hence thesis by FUNCT_1: 12, A62;

      end;

      then ( lim S00) in F2 by A6, A7, A37, A41, Th1, Th3;

      then (f . ( lim s1)) in (F1 /\ F2) by A60, A14, A40, A33, A38, A61, XBOOLE_0:def 4;

      hence thesis by A27, A48, A14;

    end;

    theorem :: TOPMETR3:14

    

     Th14: for n be Nat, p1,p2 be Point of ( TOP-REAL n), P,P1 be non empty Subset of ( TOP-REAL n) st P is_an_arc_of (p1,p2) & P1 is_an_arc_of (p2,p1) & P1 c= P holds P1 = P

    proof

      let n be Nat, p1,p2 be Point of ( TOP-REAL n), P,P1 be non empty Subset of ( TOP-REAL n);

      assume that

       A1: P is_an_arc_of (p1,p2) and

       A2: P1 is_an_arc_of (p2,p1) and

       A3: P1 c= P;

      P1 is_an_arc_of (p1,p2) by A2, JORDAN5B: 14;

      hence thesis by A1, A3, JORDAN6: 46;

    end;

    theorem :: TOPMETR3:15

    for P,P1 be compact non empty Subset of ( TOP-REAL 2) st P is being_simple_closed_curve & P1 is_an_arc_of (( W-min P),( E-max P)) & P1 c= P holds P1 = ( Upper_Arc P) or P1 = ( Lower_Arc P)

    proof

      let P,P1 be compact non empty Subset of ( TOP-REAL 2);

      assume that

       A1: P is being_simple_closed_curve and

       A2: P1 is_an_arc_of (( W-min P),( E-max P)) and

       A3: P1 c= P;

      

       A4: ( Upper_Arc P) is_an_arc_of (( W-min P),( E-max P)) by A1, JORDAN6:def 8;

      

       A5: the carrier of (( TOP-REAL 2) | P) = ( [#] (( TOP-REAL 2) | P))

      .= P by PRE_TOPC:def 5;

      then

      reconsider U2 = ( Upper_Arc P) as Subset of (( TOP-REAL 2) | P) by A1, JORDAN6: 61;

      reconsider U3 = ( Lower_Arc P) as Subset of (( TOP-REAL 2) | P) by A1, A5, JORDAN6: 61;

      

       A6: ( Lower_Arc P) is_an_arc_of (( E-max P),( W-min P)) by A1, JORDAN6:def 9;

      U2 = (( Upper_Arc P) /\ P) by A1, JORDAN6: 61, XBOOLE_1: 28;

      then

       A7: U2 is closed by A4, JORDAN6: 2, JORDAN6: 11;

      

       A8: (( Upper_Arc P) \/ ( Lower_Arc P)) = P by A1, JORDAN6:def 9;

      U3 = (( Lower_Arc P) /\ P) by A1, JORDAN6: 61, XBOOLE_1: 28;

      then

       A9: U3 is closed by A6, JORDAN6: 2, JORDAN6: 11;

      

       A10: (( Upper_Arc P) /\ ( Lower_Arc P)) = {( W-min P), ( E-max P)} by A1, JORDAN6:def 9;

      then

       A11: ( E-max P) in (( Upper_Arc P) /\ ( Lower_Arc P)) by TARSKI:def 2;

      

       A12: ( W-min P) in (( Upper_Arc P) /\ ( Lower_Arc P)) by A10, TARSKI:def 2;

      consider f be Function of I[01] , (( TOP-REAL 2) | P1) such that

       A13: f is being_homeomorphism and

       A14: (f . 0 ) = ( W-min P) and

       A15: (f . 1) = ( E-max P) by A2, TOPREAL1:def 1;

      

       A16: f is one-to-one by A13, TOPS_2:def 5;

      

       A17: ( dom f) = ( [#] I[01] ) by A13, TOPS_2:def 5;

      

       A18: ( rng f) = ( [#] (( TOP-REAL 2) | P1)) by A13, TOPS_2:def 5

      .= P1 by PRE_TOPC:def 5;

      

       A19: f is continuous by A13, TOPS_2:def 5;

      now

        per cases ;

          case

           A20: for r be Real st 0 < r & r < 1 holds (f . r) in ( Lower_Arc P);

          P1 c= ( Lower_Arc P)

          proof

            let y be object;

            assume y in P1;

            then

            consider x be object such that

             A21: x in ( dom f) and

             A22: y = (f . x) by A18, FUNCT_1:def 3;

            reconsider r = x as Real by A21;

            

             A23: r <= 1 by A21, BORSUK_1: 40, XXREAL_1: 1;

            now

              per cases by A21, A23, BORSUK_1: 40, XXREAL_0: 1, XXREAL_1: 1;

                case 0 < r & r < 1;

                hence thesis by A20, A22;

              end;

                case r = 0 ;

                hence thesis by A12, A14, A22, XBOOLE_0:def 4;

              end;

                case r = 1;

                hence thesis by A11, A15, A22, XBOOLE_0:def 4;

              end;

            end;

            hence thesis;

          end;

          hence thesis by A2, A6, Th14;

        end;

          case

           A24: ex r be Real st 0 < r & r < 1 & not (f . r) in ( Lower_Arc P);

          now

            per cases ;

              case

               A25: for r be Real st 0 < r & r < 1 holds (f . r) in ( Upper_Arc P);

              P1 c= ( Upper_Arc P)

              proof

                let y be object;

                assume y in P1;

                then

                consider x be object such that

                 A26: x in ( dom f) and

                 A27: y = (f . x) by A18, FUNCT_1:def 3;

                reconsider r = x as Real by A26;

                

                 A28: r <= 1 by A26, BORSUK_1: 40, XXREAL_1: 1;

                now

                  per cases by A26, A28, BORSUK_1: 40, XXREAL_0: 1, XXREAL_1: 1;

                    case 0 < r & r < 1;

                    hence thesis by A25, A27;

                  end;

                    case r = 0 ;

                    hence thesis by A12, A14, A27, XBOOLE_0:def 4;

                  end;

                    case r = 1;

                    hence thesis by A11, A15, A27, XBOOLE_0:def 4;

                  end;

                end;

                hence thesis;

              end;

              hence thesis by A2, A4, JORDAN6: 46;

            end;

              case ex r be Real st 0 < r & r < 1 & not (f . r) in ( Upper_Arc P);

              then

              consider r2 be Real such that

               A29: 0 < r2 and

               A30: r2 < 1 and

               A31: not (f . r2) in ( Upper_Arc P);

              r2 in [. 0 , 1.] by A29, A30, XXREAL_1: 1;

              then (f . r2) in ( rng f) by A17, BORSUK_1: 40, FUNCT_1:def 3;

              then

               A32: (f . r2) in ( Lower_Arc P) by A3, A8, A18, A31, XBOOLE_0:def 3;

              consider r1 be Real such that

               A33: 0 < r1 and

               A34: r1 < 1 and

               A35: not (f . r1) in ( Lower_Arc P) by A24;

              r1 in [. 0 , 1.] by A33, A34, XXREAL_1: 1;

              then

               A36: (f . r1) in ( rng f) by A17, BORSUK_1: 40, FUNCT_1:def 3;

              then

               A37: (f . r1) in ( Upper_Arc P) by A3, A8, A18, A35, XBOOLE_0:def 3;

              now

                per cases ;

                  case

                   A38: r1 <= r2;

                  now

                    per cases by A38, XXREAL_0: 1;

                      case r1 = r2;

                      hence contradiction by A3, A8, A18, A31, A35, A36, XBOOLE_0:def 3;

                    end;

                      case

                       A39: r1 < r2;

                      reconsider Q = P as non empty Subset of ( Euclid 2) by TOPREAL3: 8;

                      

                       A40: the carrier of (( TOP-REAL 2) | P1) = ( [#] (( TOP-REAL 2) | P1))

                      .= P1 by PRE_TOPC:def 5;

                      the carrier of (( TOP-REAL 2) | P) = ( [#] (( TOP-REAL 2) | P))

                      .= P by PRE_TOPC:def 5;

                      then ( rng f) c= the carrier of (( TOP-REAL 2) | P) by A3, A40;

                      then

                      reconsider g = f as Function of I[01] , (( TOP-REAL 2) | P) by A17, FUNCT_2: 2;

                      P = (P1 \/ P) by A3, XBOOLE_1: 12;

                      then

                       A41: (( TOP-REAL 2) | P1) is SubSpace of (( TOP-REAL 2) | P) by TOPMETR: 4;

                      (U2 \/ U3) = the carrier of (( Euclid 2) | Q) & (( TOP-REAL 2) | P) = ( TopSpaceMetr (( Euclid 2) | Q)) by A8, EUCLID: 63, TOPMETR:def 2;

                      then

                      consider r0 be Real such that

                       A42: r1 <= r0 and

                       A43: r0 <= r2 and

                       A44: (g . r0) in (U2 /\ U3) by A19, A7, A9, A30, A33, A32, A37, A39, A41, Th13, PRE_TOPC: 26;

                      r0 < 1 by A30, A43, XXREAL_0: 2;

                      then

                       A45: r0 in ( dom f) by A17, A33, A42, BORSUK_1: 40, XXREAL_1: 1;

                      

                       A46: 1 in ( dom f) by A17, BORSUK_1: 40, XXREAL_1: 1;

                      

                       A47: 0 in ( dom f) by A17, BORSUK_1: 40, XXREAL_1: 1;

                      now

                        per cases by A10, A44, TARSKI:def 2;

                          case (g . r0) = ( W-min P);

                          hence contradiction by A14, A16, A33, A42, A45, A47, FUNCT_1:def 4;

                        end;

                          case (g . r0) = ( E-max P);

                          hence contradiction by A15, A16, A30, A43, A45, A46, FUNCT_1:def 4;

                        end;

                      end;

                      hence contradiction;

                    end;

                  end;

                  hence contradiction;

                end;

                  case

                   A48: r1 > r2;

                  reconsider Q = P as non empty Subset of ( Euclid 2) by TOPREAL3: 8;

                  

                   A49: the carrier of (( TOP-REAL 2) | P1) = ( [#] (( TOP-REAL 2) | P1))

                  .= P1 by PRE_TOPC:def 5;

                  the carrier of (( TOP-REAL 2) | P) = ( [#] (( TOP-REAL 2) | P))

                  .= P by PRE_TOPC:def 5;

                  then ( rng f) c= the carrier of (( TOP-REAL 2) | P) by A3, A49;

                  then

                  reconsider g = f as Function of I[01] , (( TOP-REAL 2) | P) by A17, FUNCT_2: 2;

                  P = (P1 \/ P) by A3, XBOOLE_1: 12;

                  then

                   A50: (( TOP-REAL 2) | P1) is SubSpace of (( TOP-REAL 2) | P) by TOPMETR: 4;

                  (U2 \/ U3) = the carrier of (( Euclid 2) | Q) & (( TOP-REAL 2) | P) = ( TopSpaceMetr (( Euclid 2) | Q)) by A8, EUCLID: 63, TOPMETR:def 2;

                  then

                  consider r0 be Real such that

                   A51: r2 <= r0 and

                   A52: r0 <= r1 and

                   A53: (g . r0) in (U2 /\ U3) by A19, A7, A9, A29, A34, A32, A37, A48, A50, Th13, PRE_TOPC: 26;

                  r0 < 1 by A34, A52, XXREAL_0: 2;

                  then

                   A54: r0 in ( dom f) by A17, A29, A51, BORSUK_1: 40, XXREAL_1: 1;

                  

                   A55: 1 in ( dom f) by A17, BORSUK_1: 40, XXREAL_1: 1;

                  

                   A56: 0 in ( dom f) by A17, BORSUK_1: 40, XXREAL_1: 1;

                  now

                    per cases by A10, A53, TARSKI:def 2;

                      case (g . r0) = ( W-min P);

                      hence contradiction by A14, A16, A29, A51, A54, A56, FUNCT_1:def 4;

                    end;

                      case (g . r0) = ( E-max P);

                      hence contradiction by A15, A16, A34, A52, A54, A55, FUNCT_1:def 4;

                    end;

                  end;

                  hence contradiction;

                end;

              end;

              hence contradiction;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;