jordan5a.miz



    begin

    theorem :: JORDAN5A:1

    

     Th1: for n be Nat, p,q be Point of ( TOP-REAL n), P be Subset of ( TOP-REAL n) st P is_an_arc_of (p,q) holds P is compact

    proof

      let n be Nat;

      let p,q be Point of ( TOP-REAL n);

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

      assume P is_an_arc_of (p,q);

      then

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

       A1: f is being_homeomorphism and (f . 0 ) = p and (f . 1) = q by TOPREAL1:def 1;

      per cases ;

        suppose P <> {} ;

        then

        reconsider P9 = P as non empty Subset of ( TOP-REAL n);

        f is continuous & ( rng f) = ( [#] (( TOP-REAL n) | P9)) by A1, TOPS_2:def 5;

        then (( TOP-REAL n) | P9) is compact by COMPTS_1: 14;

        hence thesis by COMPTS_1: 3;

      end;

        suppose P = ( {} ( TOP-REAL n));

        hence thesis;

      end;

    end;

    

     Lm1: for n be Nat holds the carrier of ( Euclid n) = ( REAL n) & the carrier of ( TOP-REAL n) = ( REAL n)

    proof

      let n be Nat;

      ( Euclid n) = MetrStruct (# ( REAL n), ( Pitag_dist n) #) by EUCLID:def 7;

      hence thesis by EUCLID: 67;

    end;

    theorem :: JORDAN5A:2

    

     Th2: for n be Nat, p1,p2 be Point of ( TOP-REAL n), r1,r2 be Real st (((1 - r1) * p1) + (r1 * p2)) = (((1 - r2) * p1) + (r2 * p2)) holds r1 = r2 or p1 = p2

    proof

      let n be Nat, p1,p2 be Point of ( TOP-REAL n), r1,r2 be Real;

      assume

       A1: (((1 - r1) * p1) + (r1 * p2)) = (((1 - r2) * p1) + (r2 * p2));

      

       A2: ((1 * p1) + (( - (r1 * p1)) + (r1 * p2))) = (((1 * p1) + ( - (r1 * p1))) + (r1 * p2)) by RLVECT_1:def 3

      .= (((1 * p1) - (r1 * p1)) + (r1 * p2))

      .= (((1 - r2) * p1) + (r2 * p2)) by A1, RLVECT_1: 35

      .= (((1 * p1) - (r2 * p1)) + (r2 * p2)) by RLVECT_1: 35

      .= (((1 * p1) + ( - (r2 * p1))) + (r2 * p2))

      .= ((1 * p1) + (( - (r2 * p1)) + (r2 * p2))) by RLVECT_1:def 3;

      

       A3: (((r2 - r1) * p1) + (r1 * p2)) = (((r2 * p1) - (r1 * p1)) + (r1 * p2)) by RLVECT_1: 35

      .= (((r2 * p1) + ( - (r1 * p1))) + (r1 * p2))

      .= ((r2 * p1) + (( - (r1 * p1)) + (r1 * p2))) by RLVECT_1:def 3

      .= ((r2 * p1) + (( - (r2 * p1)) + (r2 * p2))) by A2, GOBOARD7: 4

      .= (((r2 * p1) + ( - (r2 * p1))) + (r2 * p2)) by RLVECT_1:def 3

      .= (( 0. ( TOP-REAL n)) + (r2 * p2)) by RLVECT_1: 5

      .= (r2 * p2) by RLVECT_1: 4;

      ((r2 - r1) * p1) = (((r2 - r1) * p1) + ( 0. ( TOP-REAL n))) by RLVECT_1: 4

      .= (((r2 - r1) * p1) + ((r1 * p2) - (r1 * p2))) by RLVECT_1: 5

      .= ((r2 * p2) - (r1 * p2)) by A3, RLVECT_1:def 3

      .= ((r2 - r1) * p2) by RLVECT_1: 35;

      then (r2 - r1) = 0 or p1 = p2 by RLVECT_1: 36;

      hence thesis;

    end;

    theorem :: JORDAN5A:3

    

     Th3: for n be Nat holds for p1,p2 be Point of ( TOP-REAL n) st p1 <> p2 holds ex f be Function of I[01] , (( TOP-REAL n) | ( LSeg (p1,p2))) st (for x be Real st x in [. 0 , 1.] holds (f . x) = (((1 - x) * p1) + (x * p2))) & f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = p2

    proof

      let n be Nat;

      let p1,p2 be Point of ( TOP-REAL n);

      reconsider p19 = p1, p29 = p2 as Element of ( REAL n) by Lm1;

      set P = ( LSeg (p1,p2));

      reconsider PP = P as Subset of ( Euclid n) by TOPREAL3: 8;

      reconsider PP as non empty Subset of ( Euclid n);

      defpred P[ object, object] means for x be Real st x = $1 holds $2 = (((1 - x) * p1) + (x * p2));

      

       A1: for a be object st a in [. 0 , 1.] holds ex u be object st P[a, u]

      proof

        let a be object;

        assume a in [. 0 , 1.];

        then

        reconsider x = a as Real;

        take (((1 - x) * p1) + (x * p2));

        thus thesis;

      end;

      consider f be Function such that

       A2: ( dom f) = [. 0 , 1.] and

       A3: for a be object st a in [. 0 , 1.] holds P[a, (f . a)] from CLASSES1:sch 1( A1);

      ( rng f) c= the carrier of (( TOP-REAL n) | P)

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A4: x in ( dom f) and

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

        x in { r where r be Real : 0 <= r & r <= 1 } by A2, A4, RCOMP_1:def 1;

        then

        consider r be Real such that

         A6: r = x and

         A7: 0 <= r & r <= 1;

        y = (((1 - r) * p1) + (r * p2)) by A2, A3, A4, A5, A6;

        then y in P by A7;

        then y in ( [#] (( TOP-REAL n) | P)) by PRE_TOPC:def 5;

        hence thesis;

      end;

      then

      reconsider f as Function of I[01] , (( TOP-REAL n) | P) by A2, BORSUK_1: 40, FUNCT_2:def 1, RELSET_1: 4;

      assume

       A8: p1 <> p2;

      now

        let x1,x2 be object;

        assume that

         A9: x1 in ( dom f) and

         A10: x2 in ( dom f) and

         A11: (f . x1) = (f . x2);

        x2 in { r where r be Real : 0 <= r & r <= 1 } by A2, A10, RCOMP_1:def 1;

        then

        consider r2 be Real such that

         A12: r2 = x2 and 0 <= r2 and r2 <= 1;

        

         A13: (f . x2) = (((1 - r2) * p1) + (r2 * p2)) by A2, A3, A10, A12;

        x1 in { r where r be Real : 0 <= r & r <= 1 } by A2, A9, RCOMP_1:def 1;

        then

        consider r1 be Real such that

         A14: r1 = x1 and 0 <= r1 and r1 <= 1;

        (f . x1) = (((1 - r1) * p1) + (r1 * p2)) by A2, A3, A9, A14;

        hence x1 = x2 by A8, A11, A14, A12, A13, Th2;

      end;

      then

       A15: f is one-to-one by FUNCT_1:def 4;

      

       A16: (( TOP-REAL n) | P) = ( TopSpaceMetr (( Euclid n) | PP)) by EUCLID: 63;

      for W be Point of I[01] , G be a_neighborhood of (f . W) holds ex H be a_neighborhood of W st (f .: H) c= G

      proof

        reconsider p11 = p1, p22 = p2 as Point of ( Euclid n) by TOPREAL3: 8;

        let W be Point of I[01] , G be a_neighborhood of (f . W);

        reconsider W9 = W as Point of ( Closed-Interval-MSpace ( 0 ,1)) by BORSUK_1: 40, TOPMETR: 10;

        reconsider W1 = W as Real;

        (f . W) in ( Int G) by CONNSP_2:def 1;

        then

        consider Q be Subset of (( TOP-REAL n) | P) such that

         A17: Q is open and

         A18: Q c= G and

         A19: (f . W) in Q by TOPS_1: 22;

        ( [#] (( TOP-REAL n) | P)) = P by PRE_TOPC:def 5;

        then

        reconsider Y = (f . W) as Point of (( Euclid n) | PP) by TOPMETR:def 2;

        consider r be Real such that

         A20: r > 0 and

         A21: ( Ball (Y,r)) c= Q by A16, A17, A19, TOPMETR: 15;

        reconsider r as Element of REAL by XREAL_0:def 1;

        set delta = (r / (( Pitag_dist n) . (p19,p29)));

        reconsider H = ( Ball (W9,delta)) as Subset of I[01] by BORSUK_1: 40, TOPMETR: 10;

        ( Closed-Interval-TSpace ( 0 ,1)) = ( TopSpaceMetr ( Closed-Interval-MSpace ( 0 ,1))) by TOPMETR:def 7;

        then

         A22: H is open by TOPMETR: 14, TOPMETR: 20;

        P = the carrier of (( Euclid n) | PP) by TOPMETR:def 2;

        then

        reconsider WW9 = Y as Point of ( Euclid n) by TARSKI:def 3;

        ( Euclid n) = MetrStruct (# ( REAL n), ( Pitag_dist n) #) by EUCLID:def 7;

        then

         A23: (( Pitag_dist n) . (p19,p29)) = ( dist (p11,p22)) by METRIC_1:def 1;

        

         A24: ( dist (p11,p22)) >= 0 & ( dist (p11,p22)) <> 0 by A8, METRIC_1: 2, METRIC_1: 5;

        then W in H by A20, A23, TBSP_1: 11, XREAL_1: 139;

        then W in ( Int H) by A22, TOPS_1: 23;

        then

        reconsider H as a_neighborhood of W by CONNSP_2:def 1;

        take H;

        

         A25: delta > 0 by A20, A23, A24, XREAL_1: 139;

        (f .: H) c= ( Ball (Y,r))

        proof

          reconsider WW1 = WW9 as Element of ( REAL n) by Lm1;

          let a be object;

          

           A26: ( [#] (( TOP-REAL n) | P)) = P by PRE_TOPC:def 5;

          assume a in (f .: H);

          then

          consider u be object such that

           A27: u in ( dom f) and

           A28: u in H and

           A29: a = (f . u) by FUNCT_1:def 6;

          reconsider u1 = u as Real by A27;

          

           A30: (f . W) = (((1 - W1) * p1) + (W1 * p2)) by A3, BORSUK_1: 40;

          reconsider u9 = u as Point of ( Closed-Interval-MSpace ( 0 ,1)) by A28;

          reconsider W99 = W9, u99 = u9 as Point of RealSpace by TOPMETR: 8;

          

           A31: ( dist (W9,u9)) = (the distance of ( Closed-Interval-MSpace ( 0 ,1)) . (W9,u9)) by METRIC_1:def 1

          .= (the distance of RealSpace . (W99,u99)) by TOPMETR:def 1

          .= ( dist (W99,u99)) by METRIC_1:def 1;

          ( dist (W9,u9)) < delta by A28, METRIC_1: 11;

          then |.(W1 - u1).| < delta by A31, TOPMETR: 11;

          then |.( - (u1 - W1)).| < delta;

          then

           A32: |.(u1 - W1).| < delta by COMPLEX1: 52;

          

           A33: delta <> 0 by A20, A23, A24, XREAL_1: 139;

          then (( Pitag_dist n) . (p19,p29)) = (r / delta) by XCMPLX_1: 54;

          then

           A34: |.(p19 - p29).| = (r / delta) by EUCLID:def 6;

          (f . u) in ( rng f) by A27, FUNCT_1:def 3;

          then

          reconsider aa = a as Point of (( Euclid n) | PP) by A29, A26, TOPMETR:def 2;

          P = the carrier of (( Euclid n) | PP) by TOPMETR:def 2;

          then

          reconsider aa9 = aa as Point of ( Euclid n) by TARSKI:def 3;

          reconsider aa1 = aa9 as Element of ( REAL n) by Lm1;

          aa1 = (((1 - u1) * p1) + (u1 * p2)) by A2, A3, A27, A29;

          

          then (WW1 - aa1) = ((((1 - W1) * p1) + (W1 * p2)) - (((1 - u1) * p1) + (u1 * p2))) by A30

          .= ((((W1 * p2) + ((1 - W1) * p1)) - ((1 - u1) * p1)) - (u1 * p2)) by RLVECT_1: 27

          .= (((W1 * p2) + (((1 - W1) * p1) - ((1 - u1) * p1))) - (u1 * p2)) by RLVECT_1:def 3

          .= (((W1 * p2) + (((1 - W1) - (1 - u1)) * p1)) - (u1 * p2)) by RLVECT_1: 35

          .= (((u1 - W1) * p1) + ((W1 * p2) - (u1 * p2))) by RLVECT_1:def 3

          .= (((u1 - W1) * p1) + ((W1 - u1) * p2)) by RLVECT_1: 35

          .= (((u1 - W1) * p1) + (( - (u1 - W1)) * p2))

          .= (((u1 - W1) * p1) + ( - ((u1 - W1) * p2))) by RLVECT_1: 79

          .= (((u1 - W1) * p1) - ((u1 - W1) * p2))

          .= ((u1 - W1) * (p1 - p2)) by RLVECT_1: 34

          .= ((u1 - W1) * (p19 - p29));

          then

           A35: |.(WW1 - aa1).| = ( |.(u1 - W1).| * |.(p19 - p29).|) by EUCLID: 11;

          (r / delta) > 0 by A20, A25, XREAL_1: 139;

          then |.(WW1 - aa1).| < (delta * (r / delta)) by A35, A32, A34, XREAL_1: 68;

          then ( Euclid n) = MetrStruct (# ( REAL n), ( Pitag_dist n) #) & |.(WW1 - aa1).| < r by A33, EUCLID:def 7, XCMPLX_1: 87;

          then (the distance of ( Euclid n) . (WW9,aa9)) < r by EUCLID:def 6;

          then (the distance of (( Euclid n) | PP) . (Y,aa)) < r by TOPMETR:def 1;

          then ( dist (Y,aa)) < r by METRIC_1:def 1;

          hence thesis by METRIC_1: 11;

        end;

        then (f .: H) c= Q by A21;

        hence thesis by A18;

      end;

      then

       A36: f is continuous by BORSUK_1:def 1;

      take f;

      thus for x be Real st x in [. 0 , 1.] holds (f . x) = (((1 - x) * p1) + (x * p2)) by A3;

      ( [#] (( TOP-REAL n) | P)) c= ( rng f)

      proof

        let a be object;

        assume a in ( [#] (( TOP-REAL n) | P));

        then a in { (((1 - l) * p1) + (l * p2)) where l be Real : 0 <= l & l <= 1 } by PRE_TOPC:def 5;

        then

        consider lambda be Real such that

         A37: a = (((1 - lambda) * p1) + (lambda * p2)) and

         A38: 0 <= lambda & lambda <= 1;

        lambda in { r where r be Real : 0 <= r & r <= 1 } by A38;

        then

         A39: lambda in ( dom f) by A2, RCOMP_1:def 1;

        then a = (f . lambda) by A2, A3, A37;

        hence thesis by A39, FUNCT_1:def 3;

      end;

      then ( [#] I[01] ) = [. 0 , 1.] & ( rng f) = ( [#] (( TOP-REAL n) | P)) by BORSUK_1: 40;

      hence f is being_homeomorphism by A15, A36, COMPTS_1: 17;

       0 in [. 0 , 1.] by XXREAL_1: 1;

      

      hence (f . 0 ) = (((1 - 0 ) * p1) + ( 0 * p2)) by A3

      .= (p1 + ( 0 * p2)) by RLVECT_1:def 8

      .= (p1 + ( 0. ( TOP-REAL n))) by RLVECT_1: 10

      .= p1 by RLVECT_1: 4;

      1 in [. 0 , 1.] by XXREAL_1: 1;

      

      hence (f . 1) = (((1 - 1) * p1) + (1 * p2)) by A3

      .= (( 0. ( TOP-REAL n)) + (1 * p2)) by RLVECT_1: 10

      .= (1 * p2) by RLVECT_1: 4

      .= p2 by RLVECT_1:def 8;

    end;

    

     Lm2: for n be Nat holds ( TOP-REAL n) is pathwise_connected

    proof

      let n be Nat;

      set T = ( TOP-REAL n);

      let a,b be Point of T;

      set L = ( LSeg (a,b));

      per cases ;

        suppose a <> b;

        then

        consider f be Function of I[01] , (T | L) such that for x be Real st x in [. 0 , 1.] holds (f . x) = (((1 - x) * a) + (x * b)) and

         A1: f is being_homeomorphism and

         A2: (f . 0 ) = a & (f . 1) = b by Th3;

        ( rng f) c= ( [#] (T | L));

        then ( rng f) c= L by PRE_TOPC:def 5;

        then ( dom f) = the carrier of I[01] & ( rng f) c= the carrier of T by FUNCT_2:def 1, XBOOLE_1: 1;

        then

        reconsider g = f as Function of I[01] , T by RELSET_1: 4;

        f is continuous by A1, TOPS_2:def 5;

        then g is continuous by PRE_TOPC: 26;

        hence thesis by A2;

      end;

        suppose a = b;

        hence (a,b) are_connected ;

      end;

    end;

    registration

      let n be Nat;

      cluster ( TOP-REAL n) -> pathwise_connected;

      coherence by Lm2;

    end

    registration

      let n be Nat;

      cluster compact non empty strict for SubSpace of ( TOP-REAL n);

      existence

      proof

        set A = the compact non empty Subset of ( TOP-REAL n);

        reconsider T = (( TOP-REAL n) | A) as non empty SubSpace of ( TOP-REAL n);

        T is compact;

        hence thesis;

      end;

    end

    theorem :: JORDAN5A:4

    for a,b be Point of ( TOP-REAL 2), f be Path of a, b, P be non empty compact SubSpace of ( TOP-REAL 2), g be Function of I[01] , P st f is one-to-one & g = f & ( [#] P) = ( rng f) holds g is being_homeomorphism by COMPTS_1: 17, PRE_TOPC: 27;

    

     Lm3: for X be Subset of REAL holds X is open implies X in ( Family_open_set RealSpace )

    proof

      let X be Subset of REAL ;

      reconsider V = X as Subset of RealSpace by METRIC_1:def 13;

      assume

       A1: X is open;

      for x be Element of RealSpace st x in X holds ex r be Real st r > 0 & ( Ball (x,r)) c= X

      proof

        let x be Element of RealSpace ;

        reconsider r = x as Element of REAL by METRIC_1:def 13;

        assume x in X;

        then

        consider N be Neighbourhood of r such that

         A2: N c= X by A1, RCOMP_1: 18;

        consider g be Real such that

         A3: 0 < g and

         A4: N = ].(r - g), (r + g).[ by RCOMP_1:def 6;

        reconsider g as Element of REAL by XREAL_0:def 1;

        

         A5: N c= ( Ball (x,g))

        proof

          reconsider r9 = r as Element of RealSpace ;

          let a be object;

          assume

           A6: a in N;

          then

          reconsider a9 = a as Element of REAL ;

          reconsider a1 = a9, r1 = r9 as Element of REAL ;

          a9 is Element of REAL ;

          then

          reconsider a99 = a as Element of RealSpace by METRIC_1:def 13;

           |.(a9 - r).| < g by A4, A6, RCOMP_1: 1;

          then ( real_dist . (a9,r)) < g by METRIC_1:def 12;

          then ( dist (r9,a99)) = ( real_dist . (r,a9)) & ( real_dist . (r1,a1)) < g by METRIC_1: 9, METRIC_1:def 1, METRIC_1:def 13;

          hence thesis by METRIC_1: 11;

        end;

        ( Ball (x,g)) c= N

        proof

          let a be object;

          assume a in ( Ball (x,g));

          then a in { q where q be Element of RealSpace : ( dist (x,q)) < g } by METRIC_1: 17;

          then

          consider q be Element of RealSpace such that

           A7: q = a and

           A8: ( dist (x,q)) < g;

          reconsider a9 = a as Real by A7;

          reconsider x1 = x, q1 = q as Element of REAL by METRIC_1:def 13;

          ( real_dist . (q1,x1)) < g by A8, METRIC_1:def 1, METRIC_1:def 13;

          then |.(a9 - r).| < g by A7, METRIC_1:def 12;

          hence thesis by A4, RCOMP_1: 1;

        end;

        then N = ( Ball (x,g)) by A5;

        hence thesis by A2, A3;

      end;

      then V in ( Family_open_set RealSpace ) by PCOMPS_1:def 4;

      hence thesis;

    end;

    

     Lm4: for X be Subset of REAL holds X in ( Family_open_set RealSpace ) implies X is open

    proof

      let X be Subset of REAL ;

      assume

       A1: X in ( Family_open_set RealSpace );

      for r be Element of REAL st r in X holds ex N be Neighbourhood of r st N c= X

      proof

        let r be Element of REAL ;

        assume

         A2: r in X;

        reconsider r as Element of REAL ;

        reconsider x = r as Element of RealSpace by METRIC_1:def 13;

        ex N be Neighbourhood of r st N c= X

        proof

          consider r1 be Real such that

           A3: r1 > 0 and

           A4: ( Ball (x,r1)) c= X by A1, A2, PCOMPS_1:def 4;

          reconsider N1 = ( Ball (x,r1)) as Subset of REAL by METRIC_1:def 13;

          ex g be Real st 0 < g & ( Ball (x,r1)) = ].(r - g), (r + g).[

          proof

            take g = r1;

            

             A5: ].(r - g), (r + g).[ c= N1

            proof

              let a be object;

              assume

               A6: a in ].(r - g), (r + g).[;

              then

              reconsider a9 = a as Element of REAL ;

              a9 is Element of REAL ;

              then

              reconsider a99 = a, r9 = r as Element of RealSpace by METRIC_1:def 13;

              reconsider a1 = a9, r1 = r9 as Element of REAL ;

               |.(a9 - r).| < g by A6, RCOMP_1: 1;

              then ( real_dist . (a9,r)) < g by METRIC_1:def 12;

              then ( dist (r9,a99)) = ( real_dist . (r,a9)) & ( real_dist . (r1,a1)) < g by METRIC_1: 9, METRIC_1:def 1, METRIC_1:def 13;

              hence thesis by METRIC_1: 11;

            end;

            N1 c= ].(r - g), (r + g).[

            proof

              let a be object;

              assume a in N1;

              then a in { q where q be Element of RealSpace : ( dist (x,q)) < g } by METRIC_1: 17;

              then

              consider q be Element of RealSpace such that

               A7: q = a and

               A8: ( dist (x,q)) < g;

              reconsider a9 = a as Real by A7;

              reconsider x1 = x, q1 = q as Element of REAL by METRIC_1:def 13;

              ( real_dist . (q1,x1)) < g by A8, METRIC_1:def 1, METRIC_1:def 13;

              then |.(a9 - r).| < g by A7, METRIC_1:def 12;

              hence thesis by RCOMP_1: 1;

            end;

            hence thesis by A3, A5;

          end;

          then

          reconsider N = N1 as Neighbourhood of r by RCOMP_1:def 6;

          take N;

          thus thesis by A4;

        end;

        hence thesis;

      end;

      hence thesis by RCOMP_1: 20;

    end;

    begin

    theorem :: JORDAN5A:5

    

     Th5: for X be Subset of REAL holds X in ( Family_open_set RealSpace ) iff X is open by Lm3, Lm4;

    theorem :: JORDAN5A:6

    

     Th6: for f be Function of R^1 , R^1 , x be Point of R^1 holds for g be PartFunc of REAL , REAL , x1 be Real st f is_continuous_at x & f = g & x = x1 holds g is_continuous_in x1

    proof

      let f be Function of R^1 , R^1 , x be Point of R^1 ;

      let g be PartFunc of REAL , REAL , x1 be Real;

      assume that

       A1: f is_continuous_at x and

       A2: f = g and

       A3: x = x1;

      for N1 be Neighbourhood of (g . x1) holds ex N be Neighbourhood of x1 st (g .: N) c= N1

      proof

        reconsider fx = (f . x) as Point of R^1 ;

        let N1 be Neighbourhood of (g . x1);

        reconsider N19 = N1 as Subset of R^1 by TOPMETR: 17;

        reconsider N2 = N1 as Subset of RealSpace by TOPMETR: 12, TOPMETR: 17, TOPMETR:def 6;

        N2 in ( Family_open_set RealSpace ) by Lm3;

        then N2 in the topology of ( TopSpaceMetr RealSpace ) by TOPMETR: 12;

        then N19 is open by TOPMETR:def 6;

        then

        reconsider G = N19 as a_neighborhood of fx by A2, A3, CONNSP_2: 3, RCOMP_1: 16;

        consider H be a_neighborhood of x such that

         A4: (f .: H) c= G by A1, TMAP_1:def 2;

        consider V be Subset of R^1 such that

         A5: V is open and

         A6: V c= H and

         A7: x in V by CONNSP_2: 6;

        reconsider V1 = V as Subset of REAL by TOPMETR: 17;

        V in the topology of R^1 by A5;

        then V in ( Family_open_set RealSpace ) by TOPMETR: 12, TOPMETR:def 6;

        then V1 is open by Lm4;

        then

        consider N be Neighbourhood of x1 such that

         A8: N c= V1 by A3, A7, RCOMP_1: 18;

        N c= H by A6, A8;

        then (g .: N) c= (g .: H) by RELAT_1: 123;

        hence thesis by A2, A4, XBOOLE_1: 1;

      end;

      hence thesis by FCONT_1: 5;

    end;

    theorem :: JORDAN5A:7

    

     Th7: for f be continuous Function of R^1 , R^1 , g be PartFunc of REAL , REAL st f = g holds g is continuous

    proof

      let f be continuous Function of R^1 , R^1 ;

      let g be PartFunc of REAL , REAL ;

      assume

       A1: f = g;

      for x0 be Real st x0 in ( dom g) holds g is_continuous_in x0 by A1, Th6, TMAP_1: 44, TOPMETR: 17;

      hence thesis by FCONT_1:def 2;

    end;

    

     Lm5: for f be continuous one-to-one Function of R^1 , R^1 , g be PartFunc of REAL , REAL st f = g holds (g | [. 0 , 1.]) is increasing or (g | [. 0 , 1.]) is decreasing

    proof

      let f be continuous one-to-one Function of R^1 , R^1 ;

      let g be PartFunc of REAL , REAL ;

      assume

       A1: f = g;

      then ( dom f) = REAL & g is continuous by Th7, FUNCT_2:def 1, TOPMETR: 17;

      hence thesis by A1, FCONT_2: 17;

    end;

    theorem :: JORDAN5A:8

    for f be continuous one-to-one Function of R^1 , R^1 holds (for x,y be Point of I[01] , p,q,fx,fy be Real st x = p & y = q & p < q & fx = (f . x) & fy = (f . y) holds fx < fy) or for x,y be Point of I[01] , p,q,fx,fy be Real st x = p & y = q & p < q & fx = (f . x) & fy = (f . y) holds fx > fy

    proof

      let f be continuous one-to-one Function of R^1 , R^1 ;

      

       A1: ( [. 0 , 1.] /\ ( dom f)) = ( [. 0 , 1.] /\ the carrier of R^1 ) by FUNCT_2:def 1

      .= [. 0 , 1.] by BORSUK_1: 1, BORSUK_1: 40, TOPMETR: 20, XBOOLE_1: 28;

      reconsider g = f as PartFunc of REAL , REAL by TOPMETR: 17;

      per cases by Lm5;

        suppose (g | [. 0 , 1.]) is increasing;

        hence thesis by A1, BORSUK_1: 40, RFUNCT_2: 20;

      end;

        suppose (g | [. 0 , 1.]) is decreasing;

        hence thesis by A1, BORSUK_1: 40, RFUNCT_2: 21;

      end;

    end;

    theorem :: JORDAN5A:9

    

     Th9: for r,gg,a,b be Real, x be Element of ( Closed-Interval-MSpace (a,b)) st a <= b & x = r & ].(r - gg), (r + gg).[ c= [.a, b.] holds ].(r - gg), (r + gg).[ = ( Ball (x,gg))

    proof

      let r,gg,a,b be Real, x be Element of ( Closed-Interval-MSpace (a,b));

      assume that

       A1: a <= b and

       A2: x = r and

       A3: ].(r - gg), (r + gg).[ c= [.a, b.];

      reconsider g = gg as Element of REAL by XREAL_0:def 1;

      reconsider r as Element of REAL by XREAL_0:def 1;

      set CM = ( Closed-Interval-MSpace (a,b));

      set N1 = ( Ball (x,g));

      

       A4: the carrier of CM c= the carrier of RealSpace by TOPMETR:def 1;

      

       A5: N1 c= ].(r - g), (r + g).[

      proof

        let i be object;

        assume i in N1;

        then i in { q where q be Element of CM : ( dist (x,q)) < g } by METRIC_1: 17;

        then

        consider q be Element of CM such that

         A6: q = i and

         A7: ( dist (x,q)) < g;

        reconsider a9 = i as Element of REAL by A4, A6, METRIC_1:def 13;

        reconsider x2 = x, q2 = q as Element of CM;

        reconsider x1 = x, q1 = q as Element of REAL by A4, METRIC_1:def 13;

        ( dist (x2,q2)) = (the distance of CM . (x2,q2)) by METRIC_1:def 1

        .= ( real_dist . (x2,q2)) by METRIC_1:def 13, TOPMETR:def 1;

        then ( real_dist . (q1,x1)) < g by A7, METRIC_1: 9;

        then |.(a9 - r).| < g by A2, A6, METRIC_1:def 12;

        hence thesis by RCOMP_1: 1;

      end;

       ].(r - g), (r + g).[ c= N1

      proof

        let i be object;

        assume

         A8: i in ].(r - g), (r + g).[;

        then

        reconsider a9 = i as Element of REAL ;

        reconsider a99 = i as Element of CM by A1, A3, A8, TOPMETR: 10;

         |.(a9 - r).| < g by A8, RCOMP_1: 1;

        then

         A9: ( real_dist . (a9,r)) < g by METRIC_1:def 12;

        ( dist (x,a99)) = (the distance of CM . (x,a99)) by METRIC_1:def 1

        .= ( real_dist . (x,a99)) by METRIC_1:def 13, TOPMETR:def 1;

        then ( dist (x,a99)) < g by A2, A9, METRIC_1: 9;

        hence thesis by METRIC_1: 11;

      end;

      hence thesis by A5;

    end;

    theorem :: JORDAN5A:10

    

     Th10: for a,b be Real, X be Subset of REAL st a < b & not a in X & not b in X holds X in ( Family_open_set ( Closed-Interval-MSpace (a,b))) implies X is open

    proof

      let a,b be Real, X be Subset of REAL ;

      assume that

       A1: a < b and

       A2: not a in X and

       A3: not b in X;

      assume

       A4: X in ( Family_open_set ( Closed-Interval-MSpace (a,b)));

      then

      reconsider V = X as Subset of ( Closed-Interval-MSpace (a,b));

      for r be Element of REAL st r in X holds ex N be Neighbourhood of r st N c= X

      proof

        let r be Element of REAL ;

        assume

         A5: r in X;

        reconsider r as Real;

        r in V by A5;

        then

        reconsider x = r as Element of ( Closed-Interval-MSpace (a,b));

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

        then x in [.a, b.];

        then x in { l where l be Real : a <= l & l <= b } by RCOMP_1:def 1;

        then

         A6: ex r2 be Real st r2 = x & a <= r2 & r2 <= b;

        

         A7: (r - a) <> 0 by A2, A5;

        ex N be Neighbourhood of r st N c= X

        proof

          consider r1 be Real such that

           A8: r1 > 0 and

           A9: ( Ball (x,r1)) c= X by A4, A5, PCOMPS_1:def 4;

          per cases ;

            suppose

             A10: r <= ((a + b) / 2);

            set gg = ( min ((r - a),r1));

            gg > 0

            proof

              per cases by XXREAL_0: 15;

                suppose gg = (r - a);

                hence thesis by A7, A6, XREAL_1: 48;

              end;

                suppose gg = r1;

                hence thesis by A8;

              end;

            end;

            then

            reconsider N = ].(r - gg), (r + gg).[ as Neighbourhood of r by RCOMP_1:def 6;

            take N;

             ].(r - gg), (r + gg).[ c= [.a, b.]

            proof

              (2 * r) <= (2 * ((a + b) / 2)) by A10, XREAL_1: 64;

              then

               A11: ((2 * r) - a) <= ((a + b) - a) by XREAL_1: 13;

              let i be object;

              assume i in ].(r - gg), (r + gg).[;

              then i in { l where l be Real : (r - gg) < l & l < (r + gg) } by RCOMP_1:def 2;

              then

              consider j be Real such that

               A12: j = i and

               A13: (r - gg) < j and

               A14: j < (r + gg);

              

               A15: gg <= (r - a) by XXREAL_0: 17;

              then (r + gg) <= (r + (r - a)) by XREAL_1: 6;

              then (r + gg) <= ((a + b) - a) by A11, XXREAL_0: 2;

              then

               A16: j <= b by A14, XXREAL_0: 2;

              (gg + a) <= r by A15, XREAL_1: 19;

              then (r - gg) >= a by XREAL_1: 19;

              then a <= j by A13, XXREAL_0: 2;

              then j in { l where l be Real : a <= l & l <= b } by A16;

              hence thesis by A12, RCOMP_1:def 1;

            end;

            then ].(r - gg), (r + gg).[ = ( Ball (x,gg)) by A1, Th9;

            then ].(r - gg), (r + gg).[ c= ( Ball (x,r1)) by PCOMPS_1: 1, XXREAL_0: 17;

            hence thesis by A9;

          end;

            suppose

             A17: r > ((a + b) / 2);

            set gg = ( min ((b - r),r1));

            

             A18: (b - r) <> 0 by A3, A5;

            gg > 0

            proof

              per cases by XXREAL_0: 15;

                suppose gg = (b - r);

                hence thesis by A6, A18, XREAL_1: 48;

              end;

                suppose gg = r1;

                hence thesis by A8;

              end;

            end;

            then

            reconsider N = ].(r - gg), (r + gg).[ as Neighbourhood of r by RCOMP_1:def 6;

            take N;

             ].(r - gg), (r + gg).[ c= [.a, b.]

            proof

              (2 * r) >= (((a + b) / 2) * 2) by A17, XREAL_1: 64;

              then

               A19: ((2 * r) - b) >= ((a + b) - b) by XREAL_1: 13;

              let i be object;

              assume i in ].(r - gg), (r + gg).[;

              then i in { l where l be Real : (r - gg) < l & l < (r + gg) } by RCOMP_1:def 2;

              then

              consider j be Real such that

               A20: j = i and

               A21: (r - gg) < j and

               A22: j < (r + gg);

              

               A23: gg <= (b - r) by XXREAL_0: 17;

              then (r + gg) <= b by XREAL_1: 19;

              then

               A24: j <= b by A22, XXREAL_0: 2;

              (r - gg) >= (r - (b - r)) by A23, XREAL_1: 13;

              then (r - gg) >= a by A19, XXREAL_0: 2;

              then a <= j by A21, XXREAL_0: 2;

              then j in { l where l be Real : a <= l & l <= b } by A24;

              hence thesis by A20, RCOMP_1:def 1;

            end;

            then ].(r - gg), (r + gg).[ = ( Ball (x,gg)) by A1, Th9;

            then N c= ( Ball (x,r1)) by PCOMPS_1: 1, XXREAL_0: 17;

            hence thesis by A9;

          end;

        end;

        hence thesis;

      end;

      hence thesis by RCOMP_1: 20;

    end;

    theorem :: JORDAN5A:11

    

     Th11: for X be open Subset of REAL , a,b be Real st X c= [.a, b.] holds not a in X & not b in X

    proof

      let X be open Subset of REAL , a,b be Real;

      assume

       A1: X c= [.a, b.];

      assume

       A2: a in X or b in X;

      per cases by A2;

        suppose a in X;

        then

        consider g be Real such that

         A3: 0 < g and

         A4: ].(a - g), (a + g).[ c= X by RCOMP_1: 19;

        (g / 2) <> 0 by A3;

        then

         A5: (a - (g / 2)) < (a - 0 ) by A3, XREAL_1: 15;

        g > (g / 2) by A3, XREAL_1: 216;

        then

         A6: (a - g) < (a - (g / 2)) by XREAL_1: 15;

        (a + 0 ) < (a + g) by A3, XREAL_1: 8;

        then (a - (g / 2)) < (a + g) by A5, XXREAL_0: 2;

        then (a - (g / 2)) in { l where l be Real : (a - g) < l & l < (a + g) } by A6;

        then

         A7: (a - (g / 2)) in ].(a - g), (a + g).[ by RCOMP_1:def 2;

         ].(a - g), (a + g).[ c= [.a, b.] by A1, A4;

        then (a - (g / 2)) in [.a, b.] by A7;

        then (a - (g / 2)) in { l where l be Real : a <= l & l <= b } by RCOMP_1:def 1;

        then ex l be Real st l = (a - (g / 2)) & a <= l & l <= b;

        hence thesis by A5;

      end;

        suppose b in X;

        then

        consider g be Real such that

         A8: 0 < g and

         A9: ].(b - g), (b + g).[ c= X by RCOMP_1: 19;

        (g / 2) <> 0 by A8;

        then

         A10: (b + (g / 2)) > (b + 0 ) by A8, XREAL_1: 6;

        g > (g / 2) by A8, XREAL_1: 216;

        then

         A11: (b + (g / 2)) < (b + g) by XREAL_1: 8;

        (b - g) < (b - 0 ) by A8, XREAL_1: 15;

        then (b - g) < (b + (g / 2)) by A10, XXREAL_0: 2;

        then (b + (g / 2)) in { l where l be Real : (b - g) < l & l < (b + g) } by A11;

        then

         A12: (b + (g / 2)) in ].(b - g), (b + g).[ by RCOMP_1:def 2;

         ].(b - g), (b + g).[ c= [.a, b.] by A1, A9;

        then (b + (g / 2)) in [.a, b.] by A12;

        then (b + (g / 2)) in { l where l be Real : a <= l & l <= b } by RCOMP_1:def 1;

        then ex l be Real st l = (b + (g / 2)) & a <= l & l <= b;

        hence thesis by A10;

      end;

    end;

    theorem :: JORDAN5A:12

    

     Th12: for a,b be Real, X be Subset of REAL , V be Subset of ( Closed-Interval-MSpace (a,b)) st V = X holds X is open implies V in ( Family_open_set ( Closed-Interval-MSpace (a,b)))

    proof

      let a,b be Real;

      let X be Subset of REAL , V be Subset of ( Closed-Interval-MSpace (a,b));

      assume

       A1: V = X;

      assume

       A2: X is open;

      for x be Element of ( Closed-Interval-MSpace (a,b)) st x in V holds ex r be Real st r > 0 & ( Ball (x,r)) c= V

      proof

        let x be Element of ( Closed-Interval-MSpace (a,b));

        assume

         A3: x in V;

        then

        reconsider r = x as Element of REAL by A1;

        consider N be Neighbourhood of r such that

         A4: N c= X by A1, A2, A3, RCOMP_1: 18;

        consider g be Real such that

         A5: 0 < g and

         A6: N = ].(r - g), (r + g).[ by RCOMP_1:def 6;

        reconsider g as Element of REAL by XREAL_0:def 1;

        

         A7: ( Ball (x,g)) c= N

        proof

          let aa be object;

          assume aa in ( Ball (x,g));

          then aa in { q where q be Element of ( Closed-Interval-MSpace (a,b)) : ( dist (x,q)) < g } by METRIC_1: 17;

          then

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

           A8: q = aa and

           A9: ( dist (x,q)) < g;

          

           A10: q in the carrier of ( Closed-Interval-MSpace (a,b)) & the carrier of ( Closed-Interval-MSpace (a,b)) c= the carrier of RealSpace by TOPMETR:def 1;

          then

          reconsider a9 = aa as Real by A8;

          reconsider x1 = x, q1 = q as Element of REAL by A10, METRIC_1:def 13;

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

          .= ( real_dist . (x,q)) by METRIC_1:def 13, TOPMETR:def 1;

          then ( real_dist . (q1,x1)) < g by A9, METRIC_1: 9;

          then |.(a9 - r).| < g by A8, METRIC_1:def 12;

          hence thesis by A6, RCOMP_1: 1;

        end;

        N c= ( Ball (x,g))

        proof

          let aa be object;

          assume

           A11: aa in N;

          then

          reconsider a9 = aa as Element of REAL ;

           |.(a9 - r).| < g by A6, A11, RCOMP_1: 1;

          then

           A12: ( real_dist . (a9,r)) < g by METRIC_1:def 12;

          aa in X by A4, A11;

          then

          reconsider a99 = aa, r9 = r as Element of ( Closed-Interval-MSpace (a,b)) by A1;

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

          .= ( real_dist . (r9,a99)) by METRIC_1:def 13, TOPMETR:def 1;

          then ( dist (r9,a99)) < g by A12, METRIC_1: 9;

          hence thesis by METRIC_1: 11;

        end;

        then N = ( Ball (x,g)) by A7;

        hence thesis by A1, A4, A5;

      end;

      hence thesis by PCOMPS_1:def 4;

    end;

    

     Lm6: for a,b,c be Real st a <= b holds c in the carrier of ( Closed-Interval-TSpace (a,b)) iff a <= c & c <= b

    proof

      let a,b,c be Real;

      assume a <= b;

      then

       A1: the carrier of ( Closed-Interval-TSpace (a,b)) = [.a, b.] by TOPMETR: 18;

      hereby

        assume c in the carrier of ( Closed-Interval-TSpace (a,b));

        then c in { l where l be Real : a <= l & l <= b } by A1, RCOMP_1:def 1;

        then ex c1 be Real st c1 = c & a <= c1 & c1 <= b;

        hence a <= c & c <= b;

      end;

      assume a <= c & c <= b;

      then c in { l where l be Real : a <= l & l <= b };

      hence thesis by A1, RCOMP_1:def 1;

    end;

    

     Lm7: for a,b,c,d be Real, f be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d)), x be Point of ( Closed-Interval-TSpace (a,b)) holds for g be PartFunc of REAL , REAL , x1 be Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & (f . a) = c & (f . b) = d & f is one-to-one & f = g & x = x1 holds g is_continuous_in x1

    proof

      let a,b,c,d be Real, f be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d)), x be Point of ( Closed-Interval-TSpace (a,b));

      let g be PartFunc of REAL , REAL , x1 be Real;

      assume that

       A1: a < b and

       A2: c < d and

       A3: f is_continuous_at x and

       A4: x <> a and

       A5: x <> b and

       A6: (f . a) = c and

       A7: (f . b) = d and

       A8: f is one-to-one and

       A9: f = g and

       A10: x = x1;

      

       A11: ( dom f) = the carrier of ( Closed-Interval-TSpace (a,b)) by FUNCT_2:def 1;

      for N1 be Neighbourhood of (g . x1) holds ex N be Neighbourhood of x1 st (g .: N) c= N1

      proof

        reconsider fx = (f . x) as Point of ( Closed-Interval-TSpace (c,d));

        set Rm = ( min (((g . x1) - c),(d - (g . x1))));

        let N1 be Neighbourhood of (g . x1);

        ( Closed-Interval-TSpace (c,d)) = ( TopSpaceMetr ( Closed-Interval-MSpace (c,d))) by TOPMETR:def 7;

        then

         A12: the topology of ( Closed-Interval-TSpace (c,d)) = ( Family_open_set ( Closed-Interval-MSpace (c,d))) by TOPMETR: 12;

        Rm > 0

        proof

          

           A13: b in ( dom f) by A1, A11, Lm6;

          

           A14: a in ( dom f) by A1, A11, Lm6;

          per cases by XXREAL_0: 15;

            suppose

             A15: Rm = ((g . x1) - c);

            (g . x1) in the carrier of ( Closed-Interval-TSpace (c,d)) by A9, A10, FUNCT_2: 5;

            then

             A16: (g . x1) >= c by A2, Lm6;

            Rm <> 0 by A4, A6, A8, A9, A10, A11, A14, A15, FUNCT_1:def 4;

            hence thesis by A15, A16, XREAL_1: 48;

          end;

            suppose

             A17: Rm = (d - (g . x1));

            (g . x1) in the carrier of ( Closed-Interval-TSpace (c,d)) by A9, A10, FUNCT_2: 5;

            then

             A18: (g . x1) <= d by A2, Lm6;

            (d - (g . x1)) <> (d - d) by A5, A7, A8, A9, A10, A11, A13, FUNCT_1:def 4;

            hence thesis by A17, A18, XREAL_1: 48;

          end;

        end;

        then

        reconsider Wuj = ].((g . x1) - Rm), ((g . x1) + Rm).[ as Neighbourhood of (g . x1) by RCOMP_1:def 6;

        consider Ham be Neighbourhood of (g . x1) such that

         A19: Ham c= N1 and

         A20: Ham c= Wuj by RCOMP_1: 17;

        

         A21: Wuj c= ].c, d.[

        proof

          let aa be object;

          assume aa in Wuj;

          then aa in { l where l be Real : ((g . x1) - Rm) < l & l < ((g . x1) + Rm) } by RCOMP_1:def 2;

          then

          consider A be Real such that

           A22: A = aa and

           A23: ((g . x1) - Rm) < A and

           A24: A < ((g . x1) + Rm);

          Rm <= (d - (g . x1)) by XXREAL_0: 17;

          then ((g . x1) + Rm) <= ((g . x1) + (d - (g . x1))) by XREAL_1: 6;

          then

           A25: A < d by A24, XXREAL_0: 2;

          Rm <= ((g . x1) - c) by XXREAL_0: 17;

          then (c + Rm) <= (g . x1) by XREAL_1: 19;

          then c <= ((g . x1) - Rm) by XREAL_1: 19;

          then c < A by A23, XXREAL_0: 2;

          then A in { l where l be Real : c < l & l < d } by A25;

          hence thesis by A22, RCOMP_1:def 2;

        end;

         ].c, d.[ c= [.c, d.] by XXREAL_1: 25;

        then

         A26: Wuj c= [.c, d.] by A21;

        then Wuj c= the carrier of ( Closed-Interval-MSpace (c,d)) by A2, TOPMETR: 10;

        then

        reconsider N21 = Ham as Subset of ( Closed-Interval-MSpace (c,d)) by A20, XBOOLE_1: 1;

        the carrier of ( Closed-Interval-MSpace (c,d)) = the carrier of ( TopSpaceMetr ( Closed-Interval-MSpace (c,d))) by TOPMETR: 12

        .= the carrier of ( Closed-Interval-TSpace (c,d)) by TOPMETR:def 7;

        then

        reconsider N19 = N21 as Subset of ( Closed-Interval-TSpace (c,d));

        N21 in ( Family_open_set ( Closed-Interval-MSpace (c,d))) by Th12;

        then N19 is open by A12;

        then

        reconsider G = N19 as a_neighborhood of fx by A9, A10, CONNSP_2: 3, RCOMP_1: 16;

        consider H be a_neighborhood of x such that

         A27: (f .: H) c= G by A3, TMAP_1:def 2;

        consider V be Subset of ( Closed-Interval-TSpace (a,b)) such that

         A28: V is open and

         A29: V c= H and

         A30: x in V by CONNSP_2: 6;

        

         A31: the carrier of ( Closed-Interval-MSpace (a,b)) = the carrier of ( TopSpaceMetr ( Closed-Interval-MSpace (a,b))) by TOPMETR: 12

        .= the carrier of ( Closed-Interval-TSpace (a,b)) by TOPMETR:def 7;

        then

        reconsider V2 = V as Subset of ( Closed-Interval-MSpace (a,b));

        V c= the carrier of ( Closed-Interval-MSpace (a,b)) by A31;

        then V c= [.a, b.] by A1, TOPMETR: 10;

        then

        reconsider V1 = V as Subset of REAL by XBOOLE_1: 1;

        

         A32: Ham c= [.c, d.] by A20, A26;

        

         A33: not a in V1 & not b in V1

        proof

          assume

           A34: a in V1 or b in V1;

          per cases by A34;

            suppose a in V1;

            then (f . a) in (f .: H) by A11, A29, FUNCT_1:def 6;

            hence contradiction by A6, A32, A27, Th11;

          end;

            suppose b in V1;

            then (f . b) in (f .: H) by A11, A29, FUNCT_1:def 6;

            hence contradiction by A7, A32, A27, Th11;

          end;

        end;

        ( Closed-Interval-TSpace (a,b)) = ( TopSpaceMetr ( Closed-Interval-MSpace (a,b))) by TOPMETR:def 7;

        then the topology of ( Closed-Interval-TSpace (a,b)) = ( Family_open_set ( Closed-Interval-MSpace (a,b))) by TOPMETR: 12;

        then V2 in ( Family_open_set ( Closed-Interval-MSpace (a,b))) by A28;

        then V1 is open by A1, A33, Th10;

        then

        consider N be Neighbourhood of x1 such that

         A35: N c= V1 by A10, A30, RCOMP_1: 18;

        N c= H by A29, A35;

        then

         A36: (g .: N) c= (g .: H) by RELAT_1: 123;

        (f .: H) c= N1 by A19, A27;

        hence thesis by A9, A36, XBOOLE_1: 1;

      end;

      hence thesis by FCONT_1: 5;

    end;

    theorem :: JORDAN5A:13

    

     Th13: for a,b,c,d,x1 be Real, f be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d)), x be Point of ( Closed-Interval-TSpace (a,b)), g be PartFunc of REAL , REAL st a < b & c < d & f is_continuous_at x & (f . a) = c & (f . b) = d & f is one-to-one & f = g & x = x1 holds (g | [.a, b.]) is_continuous_in x1

    proof

      let a,b,c,d,x1 be Real;

      let f be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d)), x be Point of ( Closed-Interval-TSpace (a,b));

      let g be PartFunc of REAL , REAL ;

      assume that

       A1: a < b and

       A2: c < d and

       A3: f is_continuous_at x and

       A4: (f . a) = c and

       A5: (f . b) = d and

       A6: f is one-to-one and

       A7: f = g and

       A8: x = x1;

      

       A9: for c be Element of REAL st c in ( dom g) holds (g /. c) = (g /. c);

      ( dom g) = the carrier of ( Closed-Interval-TSpace (a,b)) by A7, FUNCT_2:def 1;

      then ( dom g) = [.a, b.] by A1, TOPMETR: 18;

      then ( dom g) = (( dom g) /\ [.a, b.]);

      then

       A10: g = (g | [.a, b.]) by A9, PARTFUN2: 15;

      per cases ;

        suppose

         A11: x1 = a;

        for N1 be Neighbourhood of (g . x1) holds ex N be Neighbourhood of x1 st (g .: N) c= N1

        proof

          reconsider f0 = (f . a) as Point of ( Closed-Interval-TSpace (c,d)) by A2, A4, Lm6;

          let N1 be Neighbourhood of (g . x1);

          reconsider N2 = N1 as Subset of RealSpace by METRIC_1:def 13;

          set NN1 = (N1 /\ [.c, d.]);

          N2 in ( Family_open_set RealSpace ) by Lm3;

          then

           A12: N2 in the topology of ( TopSpaceMetr RealSpace ) by TOPMETR: 12;

          NN1 = (N1 /\ the carrier of ( Closed-Interval-TSpace (c,d))) by A2, TOPMETR: 18;

          then

          reconsider NN = NN1 as Subset of ( Closed-Interval-TSpace (c,d)) by XBOOLE_1: 17;

          NN1 = (N1 /\ ( [#] ( Closed-Interval-TSpace (c,d)))) by A2, TOPMETR: 18;

          then NN in the topology of ( Closed-Interval-TSpace (c,d)) by A12, PRE_TOPC:def 4, TOPMETR:def 6;

          then

           A13: NN is open;

          (f . a) in the carrier of ( Closed-Interval-TSpace (c,d)) by A2, A4, Lm6;

          then (g . x1) in N1 & (g . x1) in [.c, d.] by A2, A7, A11, RCOMP_1: 16, TOPMETR: 18;

          then (g . x1) in NN1 by XBOOLE_0:def 4;

          then

          reconsider N19 = NN as a_neighborhood of f0 by A7, A11, A13, CONNSP_2: 3;

          consider H be a_neighborhood of x such that

           A14: (f .: H) c= N19 by A3, A8, A11, TMAP_1:def 2;

          consider H1 be Subset of ( Closed-Interval-TSpace (a,b)) such that

           A15: H1 is open and

           A16: H1 c= H and

           A17: x in H1 by CONNSP_2: 6;

          H1 in the topology of ( Closed-Interval-TSpace (a,b)) by A15;

          then

          consider Q be Subset of R^1 such that

           A18: Q in the topology of R^1 and

           A19: H1 = (Q /\ ( [#] ( Closed-Interval-TSpace (a,b)))) by PRE_TOPC:def 4;

          reconsider Q9 = Q as Subset of RealSpace by TOPMETR: 12, TOPMETR:def 6;

          reconsider Q1 = Q9 as Subset of REAL by METRIC_1:def 13;

          Q9 in ( Family_open_set RealSpace ) by A18, TOPMETR: 12, TOPMETR:def 6;

          then

           A20: Q1 is open by Lm4;

          x1 in Q1 by A8, A17, A19, XBOOLE_0:def 4;

          then

          consider N be Neighbourhood of x1 such that

           A21: N c= Q1 by A20, RCOMP_1: 18;

          take N;

          (g .: N) c= N1

          proof

            let aa be object;

            assume

             A22: aa in (g .: N);

            then

            reconsider a9 = aa as Element of REAL ;

            consider cc be Element of REAL such that

             A23: cc in ( dom g) and

             A24: cc in N and

             A25: a9 = (g . cc) by A22, PARTFUN2: 59;

            cc in the carrier of ( Closed-Interval-TSpace (a,b)) by A7, A23, FUNCT_2:def 1;

            then cc in H1 by A19, A21, A24, XBOOLE_0:def 4;

            then (g . cc) in (f .: H) by A7, A16, FUNCT_2: 35;

            hence thesis by A14, A25, XBOOLE_0:def 4;

          end;

          hence thesis;

        end;

        hence thesis by A10, FCONT_1: 5;

      end;

        suppose

         A26: x1 = b;

        for N1 be Neighbourhood of (g . x1) holds ex N be Neighbourhood of x1 st (g .: N) c= N1

        proof

          reconsider f0 = (f . b) as Point of ( Closed-Interval-TSpace (c,d)) by A2, A5, Lm6;

          let N1 be Neighbourhood of (g . x1);

          reconsider N2 = N1 as Subset of RealSpace by METRIC_1:def 13;

          set NN1 = (N1 /\ ( [#] ( Closed-Interval-TSpace (c,d))));

          reconsider NN = NN1 as Subset of ( Closed-Interval-TSpace (c,d));

          N2 in ( Family_open_set RealSpace ) by Lm3;

          then N2 in the topology of ( TopSpaceMetr RealSpace ) by TOPMETR: 12;

          then NN in the topology of ( Closed-Interval-TSpace (c,d)) by PRE_TOPC:def 4, TOPMETR:def 6;

          then

           A27: NN is open;

          (g . x1) in N1 & (g . x1) in ( [#] ( Closed-Interval-TSpace (c,d))) by A2, A5, A7, A26, Lm6, RCOMP_1: 16;

          then (g . x1) in NN1 by XBOOLE_0:def 4;

          then

          reconsider N19 = NN as a_neighborhood of f0 by A7, A26, A27, CONNSP_2: 3;

          consider H be a_neighborhood of x such that

           A28: (f .: H) c= N19 by A3, A8, A26, TMAP_1:def 2;

          consider H1 be Subset of ( Closed-Interval-TSpace (a,b)) such that

           A29: H1 is open and

           A30: H1 c= H and

           A31: x in H1 by CONNSP_2: 6;

          H1 in the topology of ( Closed-Interval-TSpace (a,b)) by A29;

          then

          consider Q be Subset of R^1 such that

           A32: Q in the topology of R^1 and

           A33: H1 = (Q /\ ( [#] ( Closed-Interval-TSpace (a,b)))) by PRE_TOPC:def 4;

          reconsider Q9 = Q as Subset of RealSpace by TOPMETR: 12, TOPMETR:def 6;

          reconsider Q1 = Q9 as Subset of REAL by METRIC_1:def 13;

          Q9 in ( Family_open_set RealSpace ) by A32, TOPMETR: 12, TOPMETR:def 6;

          then

           A34: Q1 is open by Lm4;

          x1 in Q1 by A8, A31, A33, XBOOLE_0:def 4;

          then

          consider N be Neighbourhood of x1 such that

           A35: N c= Q1 by A34, RCOMP_1: 18;

          take N;

          (g .: N) c= N1

          proof

            let aa be object;

            assume

             A36: aa in (g .: N);

            then

            reconsider a9 = aa as Element of REAL ;

            consider cc be Element of REAL such that

             A37: cc in ( dom g) and

             A38: cc in N and

             A39: a9 = (g . cc) by A36, PARTFUN2: 59;

            cc in the carrier of ( Closed-Interval-TSpace (a,b)) by A7, A37, FUNCT_2:def 1;

            then cc in H1 by A33, A35, A38, XBOOLE_0:def 4;

            then (g . cc) in (f .: H) by A7, A30, FUNCT_2: 35;

            hence thesis by A28, A39, XBOOLE_0:def 4;

          end;

          hence thesis;

        end;

        hence thesis by A10, FCONT_1: 5;

      end;

        suppose x1 <> a & x1 <> b;

        hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, A10, Lm7;

      end;

    end;

    theorem :: JORDAN5A:14

    

     Th14: for a,b,c,d be Real, f be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d)), g be PartFunc of REAL , REAL st f is continuous one-to-one & a < b & c < d & f = g & (f . a) = c & (f . b) = d holds (g | [.a, b.]) is continuous

    proof

      let a,b,c,d be Real;

      let f be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d));

      let g be PartFunc of REAL , REAL ;

      assume that

       A1: f is continuous one-to-one and

       A2: a < b and

       A3: c < d & f = g & (f . a) = c & (f . b) = d;

      for x0 be Real st x0 in ( dom (g | [.a, b.])) holds (g | [.a, b.]) is_continuous_in x0

      proof

        let x0 be Real;

        assume x0 in ( dom (g | [.a, b.]));

        then x0 in [.a, b.] by RELAT_1: 57;

        then

        reconsider x1 = x0 as Point of ( Closed-Interval-TSpace (a,b)) by A2, TOPMETR: 18;

        f is_continuous_at x1 & x0 is Real by A1, TMAP_1: 44;

        hence thesis by A1, A2, A3, Th13;

      end;

      hence thesis by FCONT_1:def 2;

    end;

    begin

    theorem :: JORDAN5A:15

    

     Th15: for a,b,c,d be Real holds for f be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d)) st a < b & c < d & f is continuous one-to-one & (f . a) = c & (f . b) = d holds for x,y be Point of ( Closed-Interval-TSpace (a,b)), p,q,fx,fy be Real st x = p & y = q & p < q & fx = (f . x) & fy = (f . y) holds fx < fy

    proof

      let a,b,c,d be Real;

      let f be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d));

      assume that

       A1: a < b and

       A2: c < d and

       A3: f is continuous one-to-one and

       A4: (f . a) = c & (f . b) = d;

      

       A5: [.a, b.] = the carrier of ( Closed-Interval-TSpace (a,b)) by A1, TOPMETR: 18;

      

       A6: ( dom f) = the carrier of ( Closed-Interval-TSpace (a,b)) by FUNCT_2:def 1;

      ( rng f) c= REAL by MEMBERED: 3;

      then

      reconsider g = f as PartFunc of [.a, b.], REAL by A5, A6, RELSET_1: 4;

      reconsider g as PartFunc of REAL , REAL by A5, A6, RELSET_1: 5;

      

       A7: (g | [.a, b.]) is continuous by A1, A2, A3, A4, Th14;

      

       A8: ( [.a, b.] /\ ( dom f)) = ( [.a, b.] /\ the carrier of ( Closed-Interval-TSpace (a,b))) by FUNCT_2:def 1

      .= [.a, b.] by A5;

      per cases by A1, A3, A8, A7, FCONT_2: 17, XBOOLE_1: 18;

        suppose

         A9: (g | [.a, b.]) is increasing;

        for x,y be Point of ( Closed-Interval-TSpace (a,b)), p,q,fx,fy be Real st x = p & y = q & p < q & fx = (f . x) & fy = (f . y) holds fx < fy

        proof

          let x,y be Point of ( Closed-Interval-TSpace (a,b)), p,q,fx,fy be Real;

          assume that

           A10: x = p and

           A11: y = q and

           A12: p < q & fx = (f . x) & fy = (f . y);

          y in the carrier of ( Closed-Interval-TSpace (a,b));

          then

           A13: q in ( [.a, b.] /\ ( dom g)) by A1, A8, A11, TOPMETR: 18;

          x in the carrier of ( Closed-Interval-TSpace (a,b));

          then p in ( [.a, b.] /\ ( dom g)) by A1, A8, A10, TOPMETR: 18;

          hence thesis by A9, A10, A11, A12, A13, RFUNCT_2: 20;

        end;

        hence thesis;

      end;

        suppose

         A14: (g | [.a, b.]) is decreasing;

        a in ( [.a, b.] /\ ( dom g)) & b in ( [.a, b.] /\ ( dom g)) by A1, A5, A8, Lm6;

        hence thesis by A1, A2, A4, A14, RFUNCT_2: 21;

      end;

    end;

    theorem :: JORDAN5A:16

    for f be continuous one-to-one Function of I[01] , I[01] st (f . 0 ) = 0 & (f . 1) = 1 holds for x,y be Point of I[01] , p,q,fx,fy be Real st x = p & y = q & p < q & fx = (f . x) & fy = (f . y) holds fx < fy by Th15, TOPMETR: 20;

    theorem :: JORDAN5A:17

    for a,b,c,d be Real, f be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d)), P be non empty Subset of ( Closed-Interval-TSpace (a,b)), PP,QQ be Subset of R^1 st a < b & c < d & PP = P & f is continuous one-to-one & PP is compact & (f . a) = c & (f . b) = d & (f .: P) = QQ holds (f . ( lower_bound ( [#] PP))) = ( lower_bound ( [#] QQ))

    proof

      let a,b,c,d be Real;

      let f be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d)), P be non empty Subset of ( Closed-Interval-TSpace (a,b)), PP,QQ be Subset of R^1 ;

      assume that

       A1: a < b & c < d and

       A2: PP = P and

       A3: f is continuous and

       A4: f is one-to-one and

       A5: PP is compact and

       A6: (f . a) = c & (f . b) = d and

       A7: (f .: P) = QQ;

      

       A8: ( [#] ( Closed-Interval-TSpace (c,d))) = the carrier of ( Closed-Interval-TSpace (c,d));

      set IT = (f . ( lower_bound ( [#] PP)));

      

       A9: ( [#] PP) is real-bounded by A5, WEIERSTR: 11;

      ( [#] PP) <> {} by A2, WEIERSTR:def 1;

      then

       A10: ( lower_bound ( [#] PP)) in ( [#] PP) by A5, A9, RCOMP_1: 13, WEIERSTR: 12;

      then

       A11: ( lower_bound ( [#] PP)) in P by A2, WEIERSTR:def 1;

      P c= the carrier of ( Closed-Interval-TSpace (a,b));

      then

       A12: ( [#] PP) c= the carrier of ( Closed-Interval-TSpace (a,b)) by A2, WEIERSTR:def 1;

      reconsider IT as Real;

      

       A13: for r be Real st r in ( [#] QQ) holds IT <= r

      proof

        let r be Real;

        assume r in ( [#] QQ);

        then r in (f .: P) by A7, WEIERSTR:def 1;

        then r in (f .: ( [#] PP)) by A2, WEIERSTR:def 1;

        then

        consider x be object such that

         A14: x in ( dom f) and

         A15: x in ( [#] PP) and

         A16: r = (f . x) by FUNCT_1:def 6;

        reconsider x1 = x, x2 = ( lower_bound ( [#] PP)) as Point of ( Closed-Interval-TSpace (a,b)) by A11, A14;

        x1 in the carrier of ( Closed-Interval-TSpace (a,b));

        then

        reconsider r1 = x, r2 = x2 as Real;

        

         A17: r2 <= r1 by A9, A15, SEQ_4:def 2;

        reconsider fr = (f . x2), fx = (f . x1) as Real;

        per cases ;

          suppose r2 <> r1;

          then r2 < r1 by A17, XXREAL_0: 1;

          then fr < fx by A1, A3, A4, A6, Th15;

          hence thesis by A16;

        end;

          suppose r2 = r1;

          hence thesis by A16;

        end;

      end;

      ( [#] ( Closed-Interval-TSpace (a,b))) = the carrier of ( Closed-Interval-TSpace (a,b));

      then P is compact by A2, A5, COMPTS_1: 2;

      then for P1 be Subset of ( Closed-Interval-TSpace (c,d)) st P1 = QQ holds P1 is compact by A3, A7, WEIERSTR: 8;

      then QQ is compact by A7, A8, COMPTS_1: 2;

      then

       A18: ( [#] QQ) is real-bounded by WEIERSTR: 11;

      ( lower_bound ( [#] PP)) in the carrier of ( Closed-Interval-TSpace (a,b)) by A12, A10;

      then ( lower_bound ( [#] PP)) in ( dom f) by FUNCT_2:def 1;

      then IT in QQ by A7, A11, FUNCT_1:def 6;

      then

       A19: IT in ( [#] QQ) by WEIERSTR:def 1;

      for s be Real st 0 < s holds ex r be Real st r in ( [#] QQ) & r < (IT + s)

      proof

        given s be Real such that

         A20: 0 < s and

         A21: not ex r be Real st r in ( [#] QQ) & r < (IT + s);

        (IT + 0 ) < (IT + s) by A20, XREAL_1: 8;

        hence thesis by A19, A21;

      end;

      hence thesis by A18, A19, A13, SEQ_4:def 2;

    end;

    theorem :: JORDAN5A:18

    for a,b,c,d be Real, f be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d)), P,Q be non empty Subset of ( Closed-Interval-TSpace (a,b)), PP,QQ be Subset of R^1 st a < b & c < d & PP = P & QQ = Q & f is continuous one-to-one & PP is compact & (f . a) = c & (f . b) = d & (f .: P) = Q holds (f . ( upper_bound ( [#] PP))) = ( upper_bound ( [#] QQ))

    proof

      let a,b,c,d be Real;

      let f be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d)), P,Q be non empty Subset of ( Closed-Interval-TSpace (a,b)), PP,QQ be Subset of R^1 ;

      assume that

       A1: a < b & c < d and

       A2: PP = P and

       A3: QQ = Q and

       A4: f is continuous one-to-one and

       A5: PP is compact and

       A6: (f . a) = c & (f . b) = d and

       A7: (f .: P) = Q;

      

       A8: ( [#] ( Closed-Interval-TSpace (c,d))) = the carrier of ( Closed-Interval-TSpace (c,d));

      set IT = (f . ( upper_bound ( [#] PP)));

      

       A9: ( [#] PP) is real-bounded by A5, WEIERSTR: 11;

      ( [#] PP) <> {} by A2, WEIERSTR:def 1;

      then

       A10: ( upper_bound ( [#] PP)) in ( [#] PP) by A5, A9, RCOMP_1: 12, WEIERSTR: 12;

      then

       A11: ( upper_bound ( [#] PP)) in P by A2, WEIERSTR:def 1;

      P c= the carrier of ( Closed-Interval-TSpace (a,b));

      then

       A12: ( [#] PP) c= the carrier of ( Closed-Interval-TSpace (a,b)) by A2, WEIERSTR:def 1;

      reconsider IT as Real;

      

       A13: for r be Real st r in ( [#] QQ) holds IT >= r

      proof

        let r be Real;

        assume r in ( [#] QQ);

        then r in (f .: P) by A3, A7, WEIERSTR:def 1;

        then r in (f .: ( [#] PP)) by A2, WEIERSTR:def 1;

        then

        consider x be object such that

         A14: x in ( dom f) and

         A15: x in ( [#] PP) and

         A16: r = (f . x) by FUNCT_1:def 6;

        reconsider x1 = x, x2 = ( upper_bound ( [#] PP)) as Point of ( Closed-Interval-TSpace (a,b)) by A11, A14;

        x1 in the carrier of ( Closed-Interval-TSpace (a,b));

        then

        reconsider r1 = x, r2 = x2 as Real;

        

         A17: r2 >= r1 by A9, A15, SEQ_4:def 1;

        reconsider fr = (f . x2), fx = (f . x1) as Real;

        per cases ;

          suppose r2 <> r1;

          then r2 > r1 by A17, XXREAL_0: 1;

          then fr > fx by A1, A4, A6, Th15;

          hence thesis by A16;

        end;

          suppose r2 = r1;

          hence thesis by A16;

        end;

      end;

      ( [#] ( Closed-Interval-TSpace (a,b))) = the carrier of ( Closed-Interval-TSpace (a,b));

      then P is compact by A2, A5, COMPTS_1: 2;

      then for P1 be Subset of ( Closed-Interval-TSpace (c,d)) st P1 = QQ holds P1 is compact by A3, A4, A7, WEIERSTR: 8;

      then QQ is compact by A3, A7, A8, COMPTS_1: 2;

      then

       A18: ( [#] QQ) is real-bounded by WEIERSTR: 11;

      ( upper_bound ( [#] PP)) in the carrier of ( Closed-Interval-TSpace (a,b)) by A12, A10;

      then ( upper_bound ( [#] PP)) in ( dom f) by FUNCT_2:def 1;

      then IT in QQ by A3, A7, A11, FUNCT_1:def 6;

      then

       A19: IT in ( [#] QQ) by WEIERSTR:def 1;

      for s be Real st 0 < s holds ex r be Real st r in ( [#] QQ) & r > (IT - s)

      proof

        given s be Real such that

         A20: 0 < s and

         A21: not ex r be Real st r in ( [#] QQ) & r > (IT - s);

        (IT - s) < (IT - 0 ) by A20, XREAL_1: 15;

        hence thesis by A19, A21;

      end;

      hence thesis by A18, A19, A13, SEQ_4:def 1;

    end;

    theorem :: JORDAN5A:19

    for a,b be Real st a <= b holds ( lower_bound [.a, b.]) = a & ( upper_bound [.a, b.]) = b

    proof

      let a,b be Real;

      assume

       A1: a <= b;

      set X = [.a, b.];

      

       A2: a in { l where l be Real : a <= l & l <= b } by A1;

      

       A3: for s be Real st 0 < s holds ex r be Real st r in X & r < (a + s)

      proof

        let s be Real;

        assume

         A4: 0 < s;

        

         A5: a in X by A2, RCOMP_1:def 1;

        assume for r be Real st r in X holds r >= (a + s);

        hence thesis by A4, A5, XREAL_1: 29;

      end;

      

       A6: b in { l1 where l1 be Real : a <= l1 & l1 <= b } by A1;

      

       A7: for s be Real st 0 < s holds ex r be Real st r in X & (b - s) < r

      proof

        let s be Real;

        assume

         A8: 0 < s;

        

         A9: b in X by A6, RCOMP_1:def 1;

        assume for r be Real st r in X holds r <= (b - s);

        hence thesis by A8, A9, XREAL_1: 44;

      end;

      

       A10: for r be Real st r in X holds a <= r

      proof

        let r be Real;

        assume r in X;

        then r in { l where l be Real : a <= l & l <= b } by RCOMP_1:def 1;

        then ex r1 be Real st r1 = r & a <= r1 & r1 <= b;

        hence thesis;

      end;

      b is UpperBound of X

      proof

        let r be ExtReal;

        assume r in X;

        then r in { l where l be Real : a <= l & l <= b } by RCOMP_1:def 1;

        then ex r1 be Real st r1 = r & a <= r1 & r1 <= b;

        hence thesis;

      end;

      then

       A11: X is bounded_above;

      a is LowerBound of X

      proof

        let r be ExtReal;

        assume r in X;

        then r in { l where l be Real : a <= l & l <= b } by RCOMP_1:def 1;

        then ex r1 be Real st r1 = r & a <= r1 & r1 <= b;

        hence thesis;

      end;

      then

       A12: X is bounded_below;

      

       A13: for r be Real st r in X holds b >= r

      proof

        let r be Real;

        assume r in X;

        then r in { l where l be Real : a <= l & l <= b } by RCOMP_1:def 1;

        then ex r1 be Real st r1 = r & a <= r1 & r1 <= b;

        hence thesis;

      end;

      a in X by A2, RCOMP_1:def 1;

      hence thesis by A12, A11, A10, A3, A13, A7, SEQ_4:def 1, SEQ_4:def 2;

    end;

    theorem :: JORDAN5A:20

    for a,b,c,d,e,f,g,h be Real holds for F be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d)) st a < b & c < d & e < f & a <= e & f <= b & F is being_homeomorphism & (F . a) = c & (F . b) = d & g = (F . e) & h = (F . f) holds (F .: [.e, f.]) = [.g, h.]

    proof

      let a,b,c,d,e,f,g,h be Real;

      let F be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (c,d));

      assume that

       A1: a < b and

       A2: c < d and

       A3: e < f and

       A4: a <= e and

       A5: f <= b and

       A6: F is being_homeomorphism and

       A7: (F . a) = c & (F . b) = d and

       A8: g = (F . e) and

       A9: h = (F . f);

      a <= f by A3, A4, XXREAL_0: 2;

      then f in { l1 where l1 be Real : a <= l1 & l1 <= b } by A5;

      then

       A10: f in [.a, b.] by RCOMP_1:def 1;

      then f in the carrier of ( Closed-Interval-TSpace (a,b)) by A1, TOPMETR: 18;

      then h in the carrier of ( Closed-Interval-TSpace (c,d)) by A9, FUNCT_2: 5;

      then

       A11: h in [.c, d.] by A2, TOPMETR: 18;

      e <= b by A3, A5, XXREAL_0: 2;

      then e in { l1 where l1 be Real : a <= l1 & l1 <= b } by A4;

      then

       A12: e in [.a, b.] by RCOMP_1:def 1;

      then e in the carrier of ( Closed-Interval-TSpace (a,b)) by A1, TOPMETR: 18;

      then g in the carrier of ( Closed-Interval-TSpace (c,d)) by A8, FUNCT_2: 5;

      then g in [.c, d.] by A2, TOPMETR: 18;

      then [.g, h.] c= [.c, d.] by A11, XXREAL_2:def 12;

      then

       A13: [.g, h.] c= the carrier of ( Closed-Interval-TSpace (c,d)) by A2, TOPMETR: 18;

      

       A14: F is continuous one-to-one by A6, TOPS_2:def 5;

      

       A15: [.g, h.] c= (F .: [.e, f.])

      proof

        let aa be object;

        

         A16: F is one-to-one by A6, TOPS_2:def 5;

        assume aa in [.g, h.];

        then aa in { l1 where l1 be Real : g <= l1 & l1 <= h } by RCOMP_1:def 1;

        then

        consider l be Real such that

         A17: aa = l and

         A18: g <= l and

         A19: l <= h;

        

         A20: ( rng F) = ( [#] ( Closed-Interval-TSpace (c,d))) by A6, TOPS_2:def 5;

        l in { l1 where l1 be Real : g <= l1 & l1 <= h } by A18, A19;

        then

         A21: l in [.g, h.] by RCOMP_1:def 1;

        reconsider x = ((F " ) . l) as Real;

        F is onto by A20, FUNCT_2:def 3;

        then

         A22: x = ((F qua Function " ) . l) by A16, TOPS_2:def 4;

        then

         A23: x in ( dom F) by A13, A16, A20, A21, FUNCT_1: 32;

        ( dom F) = ( [#] ( Closed-Interval-TSpace (a,b))) by A6, TOPS_2:def 5;

        then

        reconsider e9 = e, f9 = f, x9 = x as Point of ( Closed-Interval-TSpace (a,b)) by A1, A12, A10, A13, A16, A20, A21, A22, FUNCT_1: 32, TOPMETR: 18;

        reconsider g9 = (F . e9), h9 = (F . f9), l9 = (F . x9) as Point of ( Closed-Interval-TSpace (c,d));

        reconsider gg = g9, hh = h9, ll = l9 as Real;

        

         A24: x <= f

        proof

          assume x > f;

          then ll > hh by A1, A2, A7, A14, Th15;

          hence thesis by A9, A13, A19, A16, A20, A21, A22, FUNCT_1: 32;

        end;

        e <= x

        proof

          assume e > x;

          then gg > ll by A1, A2, A7, A14, Th15;

          hence thesis by A8, A13, A18, A16, A20, A21, A22, FUNCT_1: 32;

        end;

        then x in { l1 where l1 be Real : e <= l1 & l1 <= f } by A24;

        then

         A25: x in [.e, f.] by RCOMP_1:def 1;

        aa = (F . x) by A13, A17, A16, A20, A21, A22, FUNCT_1: 32;

        hence thesis by A23, A25, FUNCT_1:def 6;

      end;

      (F .: [.e, f.]) c= [.g, h.]

      proof

        let aa be object;

        assume aa in (F .: [.e, f.]);

        then

        consider x be object such that

         A26: x in ( dom F) and

         A27: x in [.e, f.] and

         A28: aa = (F . x) by FUNCT_1:def 6;

        x in { l where l be Real : e <= l & l <= f } by A27, RCOMP_1:def 1;

        then

        consider x9 be Real such that

         A29: x9 = x and

         A30: e <= x9 and

         A31: x9 <= f;

        reconsider Fx = (F . x9) as Real;

        reconsider e1 = e, f1 = f, x1 = x9 as Point of ( Closed-Interval-TSpace (a,b)) by A1, A12, A10, A26, A29, TOPMETR: 18;

        reconsider gg = (F . e1), hh = (F . f1), FFx = (F . x1) as Real;

        

         A32: Fx <= h

        proof

          per cases ;

            suppose f = x;

            hence thesis by A9, A29;

          end;

            suppose f <> x;

            then f > x9 by A29, A31, XXREAL_0: 1;

            then hh > FFx by A1, A2, A7, A14, Th15;

            hence thesis by A9;

          end;

        end;

        g <= Fx

        proof

          per cases ;

            suppose e = x;

            hence thesis by A8, A29;

          end;

            suppose e <> x;

            then e < x9 by A29, A30, XXREAL_0: 1;

            then gg < FFx by A1, A2, A7, A14, Th15;

            hence thesis by A8;

          end;

        end;

        then Fx in { l1 where l1 be Real : g <= l1 & l1 <= h } by A32;

        hence thesis by A28, A29, RCOMP_1:def 1;

      end;

      hence thesis by A15;

    end;

    theorem :: JORDAN5A:21

    for P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) st P meets Q & (P /\ Q) is closed & P is_an_arc_of (p1,p2) holds ex EX be Point of ( TOP-REAL 2) st (EX in (P /\ Q) & ex g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = EX & 0 <= s2 & s2 <= 1 & for t be Real st 0 <= t & t < s2 holds not (g . t) in Q)

    proof

      let P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: P meets Q and

       A2: (P /\ Q) is closed and

       A3: P is_an_arc_of (p1,p2);

      (P /\ Q) <> {} by A1;

      then

      reconsider P as non empty Subset of ( TOP-REAL 2);

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

       A4: f is being_homeomorphism and

       A5: (f . 0 ) = p1 & (f . 1) = p2 by A3, TOPREAL1:def 1;

      

       A6: f is one-to-one by A4, TOPS_2:def 5;

      ( [#] (( TOP-REAL 2) | P)) = P by PRE_TOPC:def 5;

      then

      reconsider PQ = (P /\ Q) as non empty Subset of (( TOP-REAL 2) | P) by A1, XBOOLE_1: 17;

      reconsider P1 = P, Q1 = Q as non empty Subset of ( TOP-REAL 2) by A1;

      consider OO be object such that

       A7: OO in PQ by XBOOLE_0:def 1;

      reconsider PP = P as Subset of ( TOP-REAL 2);

      PP is compact by A3, Th1;

      then

       A8: (P /\ Q) is compact by A2, COMPTS_1: 9, XBOOLE_1: 17;

      PQ <> ( {} (( TOP-REAL 2) | P));

      then

      reconsider PQ1 = (P /\ Q) as non empty Subset of (( TOP-REAL 2) | P1);

      (( TOP-REAL 2) | (P1 /\ Q1)) = ((( TOP-REAL 2) | P1) | PQ1) by GOBOARD9: 2;

      then

       A9: PQ is compact by A8, COMPTS_1: 3;

      set g = (f " );

      reconsider g1 = g as Function;

      

       A10: ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A4, TOPS_2:def 5;

      ( [#] I[01] ) c= ( [#] R^1 ) by PRE_TOPC:def 4;

      then

      reconsider GPQ = (g .: PQ) as Subset of R^1 by XBOOLE_1: 1;

      g is continuous by A4, TOPS_2:def 5;

      then (g .: PQ) c= ( [#] I[01] ) & for P be Subset of I[01] st P = GPQ holds P is compact by A9, WEIERSTR: 8;

      then

       A11: GPQ is compact by COMPTS_1: 2;

      then

       A12: ( [#] GPQ) is real-bounded by WEIERSTR: 11;

      set Ex = ( lower_bound ( [#] GPQ));

      reconsider f1 = f as Function;

      take (f . Ex);

      

       A13: ( dom g) = the carrier of (( TOP-REAL 2) | P) by FUNCT_2:def 1;

      ( dom g) = the carrier of (( TOP-REAL 2) | P) by FUNCT_2:def 1;

      then (g . OO) in GPQ by A7, FUNCT_1:def 6;

      then ( [#] GPQ) <> {} by WEIERSTR:def 1;

      then Ex in ( [#] GPQ) by A11, A12, RCOMP_1: 13, WEIERSTR: 12;

      then

       A14: Ex in GPQ by WEIERSTR:def 1;

      then

       A15: Ex <= 1 by BORSUK_1: 43;

      

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

      

       A17: for t be Real st 0 <= t & t < Ex holds not (f . t) in Q

      proof

        let t be Real;

        assume that

         A18: 0 <= t and

         A19: t < Ex;

        

         A20: t <= 1 by A15, A19, XXREAL_0: 2;

        then t in the carrier of I[01] by A18, BORSUK_1: 43;

        then (f . t) in the carrier of (( TOP-REAL 2) | P) by FUNCT_2: 5;

        then

         A21: (f . t) in P by PRE_TOPC: 8;

        f is onto by A10, FUNCT_2:def 3;

        then

         A22: g = (f1 " ) by A6, TOPS_2:def 4;

        assume (f . t) in Q;

        then (f . t) in PQ by A21, XBOOLE_0:def 4;

        then

         A23: (g . (f . t)) in GPQ by A13, FUNCT_1:def 6;

        t in ( dom f) by A16, A18, A20, BORSUK_1: 43;

        then (g . (f . t)) = t by A6, A22, FUNCT_1: 34;

        then t in ( [#] GPQ) by A23, WEIERSTR:def 1;

        hence thesis by A12, A19, SEQ_4:def 2;

      end;

      

       A24: (f " ) is one-to-one by A10, A6, TOPS_2: 50;

      g is being_homeomorphism by A4, TOPS_2: 56;

      then ( rng g) = ( [#] I[01] ) by TOPS_2:def 5;

      then g is onto by FUNCT_2:def 3;

      then ((f " ) " ) = (g1 " ) by A24, TOPS_2:def 4;

      then

       A25: f = (g1 " ) by A10, A6, TOPS_2: 51;

      

       A26: (ex pq be object st pq in ( dom g) & pq in PQ & Ex = (g . pq)) & 0 <= Ex by A14, BORSUK_1: 43, FUNCT_1:def 6;

      g is one-to-one by A10, A6, TOPS_2: 50;

      hence thesis by A4, A5, A25, A26, A15, A17, FUNCT_1: 34;

    end;

    theorem :: JORDAN5A:22

    for P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2) st P meets Q & (P /\ Q) is closed & P is_an_arc_of (p1,p2) holds ex EX be Point of ( TOP-REAL 2) st (EX in (P /\ Q) & ex g be Function of I[01] , (( TOP-REAL 2) | P), s2 be Real st g is being_homeomorphism & (g . 0 ) = p1 & (g . 1) = p2 & (g . s2) = EX & 0 <= s2 & s2 <= 1 & for t be Real st 1 >= t & t > s2 holds not (g . t) in Q)

    proof

      let P,Q be Subset of ( TOP-REAL 2), p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: P meets Q and

       A2: (P /\ Q) is closed and

       A3: P is_an_arc_of (p1,p2);

      (P /\ Q) <> {} by A1;

      then

      reconsider P as non empty Subset of ( TOP-REAL 2);

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

       A4: f is being_homeomorphism and

       A5: (f . 0 ) = p1 & (f . 1) = p2 by A3, TOPREAL1:def 1;

      

       A6: f is one-to-one by A4, TOPS_2:def 5;

      ( [#] (( TOP-REAL 2) | P)) = P by PRE_TOPC:def 5;

      then

      reconsider PQ = (P /\ Q) as non empty Subset of (( TOP-REAL 2) | P) by A1, XBOOLE_1: 17;

      reconsider P1 = P, Q1 = Q as non empty Subset of ( TOP-REAL 2) by A1;

      consider OO be object such that

       A7: OO in PQ by XBOOLE_0:def 1;

      reconsider PP = P as Subset of ( TOP-REAL 2);

      PP is compact by A3, Th1;

      then

       A8: (P /\ Q) is compact by A2, COMPTS_1: 9, XBOOLE_1: 17;

      PQ <> ( {} (( TOP-REAL 2) | P));

      then

      reconsider PQ1 = (P /\ Q) as non empty Subset of (( TOP-REAL 2) | P1);

      (( TOP-REAL 2) | (P1 /\ Q1)) = ((( TOP-REAL 2) | P1) | PQ1) by GOBOARD9: 2;

      then

       A9: PQ is compact by A8, COMPTS_1: 3;

      set g = (f " );

      reconsider g1 = g as Function;

      

       A10: ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A4, TOPS_2:def 5;

      

       A11: (f " ) is one-to-one by A10, A6, TOPS_2: 50;

      g is being_homeomorphism by A4, TOPS_2: 56;

      then ( rng g) = ( [#] I[01] ) by TOPS_2:def 5;

      then g is onto by FUNCT_2:def 3;

      then ((f " ) " ) = (g1 " ) by A11, TOPS_2:def 4;

      then

       A12: f = (g1 " ) by A10, A6, TOPS_2: 51;

      ( [#] I[01] ) c= ( [#] R^1 ) by PRE_TOPC:def 4;

      then

      reconsider GPQ = (g .: PQ) as Subset of R^1 by XBOOLE_1: 1;

      g is continuous by A4, TOPS_2:def 5;

      then (g .: PQ) c= ( [#] I[01] ) & for P be Subset of I[01] st P = GPQ holds P is compact by A9, WEIERSTR: 8;

      then

       A13: GPQ is compact by COMPTS_1: 2;

      then

       A14: ( [#] GPQ) is real-bounded by WEIERSTR: 11;

      set Ex = ( upper_bound ( [#] GPQ));

      reconsider f1 = f as Function;

      take (f . Ex);

      

       A15: ( dom g) = the carrier of (( TOP-REAL 2) | P) by FUNCT_2:def 1;

      ( dom g) = the carrier of (( TOP-REAL 2) | P) by FUNCT_2:def 1;

      then (g . OO) in GPQ by A7, FUNCT_1:def 6;

      then ( [#] GPQ) <> {} by WEIERSTR:def 1;

      then Ex in ( [#] GPQ) by A13, A14, RCOMP_1: 12, WEIERSTR: 12;

      then

       A16: Ex in GPQ by WEIERSTR:def 1;

      then

       A17: 0 <= Ex by BORSUK_1: 43;

      

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

      

       A19: for t be Real st 1 >= t & t > Ex holds not (f . t) in Q

      proof

        let t be Real;

        assume that

         A20: 1 >= t and

         A21: t > Ex;

        t in the carrier of I[01] by A17, A20, A21, BORSUK_1: 43;

        then (f . t) in the carrier of (( TOP-REAL 2) | P) by FUNCT_2: 5;

        then

         A22: (f . t) in P by PRE_TOPC: 8;

        f is onto by A10, FUNCT_2:def 3;

        then

         A23: g = (f1 " ) by A6, TOPS_2:def 4;

        assume (f . t) in Q;

        then (f . t) in PQ by A22, XBOOLE_0:def 4;

        then

         A24: (g . (f . t)) in GPQ by A15, FUNCT_1:def 6;

        t in ( dom f) by A18, A17, A20, A21, BORSUK_1: 43;

        then (g . (f . t)) = t by A6, A23, FUNCT_1: 34;

        then t in ( [#] GPQ) by A24, WEIERSTR:def 1;

        hence thesis by A14, A21, SEQ_4:def 1;

      end;

      

       A25: (ex pq be object st pq in ( dom g) & pq in PQ & Ex = (g . pq)) & Ex <= 1 by A16, BORSUK_1: 43, FUNCT_1:def 6;

      g is one-to-one by A10, A6, TOPS_2: 50;

      hence thesis by A4, A5, A12, A17, A25, A19, FUNCT_1: 34;

    end;

    registration

      cluster non empty finite real-bounded for Subset of REAL ;

      existence

      proof

        reconsider a = { 0 } as finite Subset of REAL ;

        take a;

        thus thesis;

      end;

    end

    

     Lm8: R^1 = TopStruct (# the carrier of RealSpace , ( Family_open_set RealSpace ) #) by PCOMPS_1:def 5, TOPMETR:def 6;

    theorem :: JORDAN5A:23

    

     Th23: for A be Subset of REAL , B be Subset of R^1 st A = B holds A is closed iff B is closed

    proof

      let A be Subset of REAL , B be Subset of R^1 such that

       A1: A = B;

      thus A is closed implies B is closed

      proof

        assume A is closed;

        then ((A ` ) ` ) is closed;

        then (A ` ) is open by RCOMP_1:def 5;

        then (A ` ) in the topology of R^1 by Lm8, Th5;

        hence (( [#] R^1 ) \ B) is open by A1, TOPMETR: 17;

      end;

      assume B is closed;

      then (B ` ) in the topology of R^1 by PRE_TOPC:def 2;

      then (A ` ) is open by A1, Lm8, Th5, TOPMETR: 17;

      then ((A ` ) ` ) is closed by RCOMP_1:def 5;

      hence thesis;

    end;

    theorem :: JORDAN5A:24

    for A be Subset of REAL , B be Subset of R^1 st A = B holds ( Cl A) = ( Cl B)

    proof

      let A be Subset of REAL , B be Subset of R^1 such that

       A1: A = B;

      thus ( Cl A) c= ( Cl B)

      proof

        let a be object;

        assume

         A2: a in ( Cl A);

        for G be Subset of R^1 st G is open & a in G holds B meets G

        proof

          let G be Subset of R^1 such that

           A3: G is open and

           A4: a in G;

          reconsider H = G as Subset of REAL by TOPMETR: 17;

          G in ( Family_open_set RealSpace ) by A3, Lm8;

          then H is open by Th5;

          then (A /\ H) is non empty by A2, A4, MEASURE6: 63;

          hence thesis by A1;

        end;

        hence thesis by A2, PRE_TOPC:def 7, TOPMETR: 17;

      end;

      let a be object;

      assume

       A5: a in ( Cl B);

      for O be open Subset of REAL st a in O holds (O /\ A) is non empty

      proof

        let O be open Subset of REAL such that

         A6: a in O;

        reconsider P = O as Subset of R^1 by TOPMETR: 17;

        P in ( Family_open_set RealSpace ) by Th5;

        then P is open by Lm8;

        then P meets B by A5, A6, PRE_TOPC:def 7;

        hence thesis by A1;

      end;

      hence thesis by A5, MEASURE6: 63;

    end;

    registration

      let a,b be Real;

      cluster [.a, b.] -> compact;

      coherence by RCOMP_1: 6;

    end

    theorem :: JORDAN5A:25

    

     Th25: for A be Subset of REAL , B be Subset of R^1 st A = B holds A is compact iff B is compact

    proof

      let A be Subset of REAL , B be Subset of R^1 such that

       A1: A = B;

      thus A is compact implies B is compact

      proof

        assume

         A2: A is compact;

        per cases ;

          suppose A = {} ;

          then

          reconsider C = B as empty Subset of R^1 by A1;

          C is compact;

          hence thesis;

        end;

          suppose A <> {} ;

          then

          reconsider A as non empty real-bounded Subset of REAL by A2, RCOMP_1: 10;

          reconsider i = ( inf A), s = ( sup A) as Real;

          reconsider X = [.i, s.] as Subset of R^1 by TOPMETR: 17;

          

           A3: i <= s by XXREAL_2: 40;

          then

           A4: ( Closed-Interval-TSpace (i,s)) = ( R^1 | X) by TOPMETR: 19;

          

           A5: B is closed by A1, A2, Th23;

          

           A6: X <> {} by A3, XXREAL_1: 30;

          

           A7: B c= X by A1, XXREAL_2: 69;

          ( Closed-Interval-TSpace (i,s)) is compact by A3, HEINE: 4;

          then X is compact by A6, A4, COMPTS_1: 3;

          hence thesis by A5, A7, COMPTS_1: 9;

        end;

      end;

      assume B is compact;

      then ( [#] B) is compact by WEIERSTR: 13;

      hence thesis by A1, WEIERSTR:def 1;

    end;

    registration

      cluster finite -> compact for Subset of REAL ;

      coherence by Th25, TOPMETR: 17;

    end

    theorem :: JORDAN5A:26

    for a,b be Real holds a <> b iff ( Cl ].a, b.[) = [.a, b.]

    proof

      let a,b be Real;

      thus a <> b implies ( Cl ].a, b.[) = [.a, b.]

      proof

        assume

         A1: a <> b;

        per cases by A1, XXREAL_0: 1;

          suppose

           A2: a > b;

          

          hence ( Cl ].a, b.[) = {} by MEASURE6: 60, XXREAL_1: 28

          .= [.a, b.] by A2, XXREAL_1: 29;

        end;

          suppose

           A3: a < b;

          then

           A4: ((a + b) / 2) < b by XREAL_1: 226;

          thus ( Cl ].a, b.[) c= [.a, b.] by MEASURE6: 57, XXREAL_1: 25;

          let p be object;

          

           A5: ].a, b.[ = { w where w be Real : a < w & w < b } by RCOMP_1:def 2;

          assume

           A6: p in [.a, b.];

           [.a, b.] = { w where w be Real : a <= w & w <= b } by RCOMP_1:def 1;

          then

          consider r be Real such that

           A7: p = r and

           A8: a <= r and

           A9: r <= b by A6;

          a < ((a + b) / 2) by A3, XREAL_1: 226;

          then

           A10: ((a + b) / 2) in ].a, b.[ by A5, A4;

          now

            per cases by A8, A9, XXREAL_0: 1;

              case

               A11: a < r & r < b;

              

               A12: ].a, b.[ c= ( Cl ].a, b.[) by MEASURE6: 58;

              r in ].a, b.[ by A5, A11;

              hence thesis by A7, A12;

            end;

              case

               A13: a = r;

              for O be open Subset of REAL st a in O holds (O /\ ].a, b.[) is non empty

              proof

                let O be open Subset of REAL ;

                assume a in O;

                then

                consider g be Real such that

                 A14: 0 < g and

                 A15: ].(a - g), (a + g).[ c= O by RCOMP_1: 19;

                

                 A16: (a - g) < (a - 0 ) by A14, XREAL_1: 15;

                

                 A17: ].(a - g), (a + g).[ = { w where w be Real : (a - g) < w & w < (a + g) } by RCOMP_1:def 2;

                per cases ;

                  suppose

                   A18: (a + g) < b;

                  

                   A19: (a + 0 ) < (a + g) by A14, XREAL_1: 6;

                  then

                   A20: a < ((a + (a + g)) / 2) by XREAL_1: 226;

                  

                   A21: ((a + (a + g)) / 2) < (a + g) by A19, XREAL_1: 226;

                  then ((a + (a + g)) / 2) < b by A18, XXREAL_0: 2;

                  then

                   A22: ((a + (a + g)) / 2) in ].a, b.[ by A5, A20;

                  (a - g) < ((a + (a + g)) / 2) by A16, A20, XXREAL_0: 2;

                  then ((a + (a + g)) / 2) in ].(a - g), (a + g).[ by A17, A21;

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

                end;

                  suppose

                   A23: (a + g) >= b;

                  ((a + b) / 2) < b by A3, XREAL_1: 226;

                  then

                   A24: ((a + b) / 2) < (a + g) by A23, XXREAL_0: 2;

                  a < ((a + b) / 2) by A3, XREAL_1: 226;

                  then (a - g) < ((a + b) / 2) by A16, XXREAL_0: 2;

                  then ((a + b) / 2) in ].(a - g), (a + g).[ by A17, A24;

                  hence thesis by A10, A15, XBOOLE_0:def 4;

                end;

              end;

              hence thesis by A7, A13, MEASURE6: 63;

            end;

              case

               A25: b = r;

              for O be open Subset of REAL st b in O holds (O /\ ].a, b.[) is non empty

              proof

                let O be open Subset of REAL ;

                assume b in O;

                then

                consider g be Real such that

                 A26: 0 < g and

                 A27: ].(b - g), (b + g).[ c= O by RCOMP_1: 19;

                

                 A28: (b - g) < (b - 0 ) by A26, XREAL_1: 15;

                

                 A29: (b + 0 ) < (b + g) by A26, XREAL_1: 6;

                

                 A30: ].(b - g), (b + g).[ = { w where w be Real : (b - g) < w & w < (b + g) } by RCOMP_1:def 2;

                per cases ;

                  suppose

                   A31: (b - g) > a;

                  

                   A32: ((b + (b - g)) / 2) < b by A28, XREAL_1: 226;

                  

                   A33: (b - g) < ((b + (b - g)) / 2) by A28, XREAL_1: 226;

                  then a < ((b + (b - g)) / 2) by A31, XXREAL_0: 2;

                  then

                   A34: ((b + (b - g)) / 2) in ].a, b.[ by A5, A32;

                  ((b + (b - g)) / 2) < b by A28, XREAL_1: 226;

                  then ((b + (b - g)) / 2) < (b + g) by A29, XXREAL_0: 2;

                  then ((b + (b - g)) / 2) in ].(b - g), (b + g).[ by A30, A33;

                  hence thesis by A27, A34, XBOOLE_0:def 4;

                end;

                  suppose

                   A35: (b - g) <= a;

                  ((a + b) / 2) < b by A3, XREAL_1: 226;

                  then

                   A36: ((a + b) / 2) < (b + g) by A29, XXREAL_0: 2;

                  a < ((a + b) / 2) by A3, XREAL_1: 226;

                  then (b - g) < ((a + b) / 2) by A35, XXREAL_0: 2;

                  then ((a + b) / 2) in ].(b - g), (b + g).[ by A30, A36;

                  hence thesis by A10, A27, XBOOLE_0:def 4;

                end;

              end;

              hence thesis by A7, A25, MEASURE6: 63;

            end;

          end;

          hence thesis;

        end;

      end;

      assume that

       A37: ( Cl ].a, b.[) = [.a, b.] and

       A38: a = b;

       [.a, b.] = {a} by A38, XXREAL_1: 17;

      hence contradiction by A37, A38, MEASURE6: 60, XXREAL_1: 28;

    end;

    theorem :: JORDAN5A:27

    for T be TopStruct, f be RealMap of T, g be Function of T, R^1 st f = g holds f is continuous iff g is continuous

    proof

      let T be TopStruct, f be RealMap of T, g be Function of T, R^1 such that

       A1: f = g;

      thus f is continuous implies g is continuous

      proof

        assume

         A2: for Y be Subset of REAL st Y is closed holds (f " Y) is closed;

        let P be Subset of R^1 such that

         A3: P is closed;

        reconsider R = P as Subset of REAL by TOPMETR: 17;

        R is closed by A3, Th23;

        hence thesis by A1, A2;

      end;

      assume

       A4: for Y be Subset of R^1 st Y is closed holds (g " Y) is closed;

      let P be Subset of REAL such that

       A5: P is closed;

      reconsider R = P as Subset of R^1 by TOPMETR: 17;

      R is closed by A5, Th23;

      hence thesis by A1, A4;

    end;