treal_1.miz



    begin

    reserve a,b,c,d for Real;

    

     Lm1: for x be set st x in [.a, b.] holds x is Element of REAL ;

    

     Lm2: for x be Point of ( Closed-Interval-TSpace (a,b)) st a <= b holds x is Element of REAL

    proof

      let x be Point of ( Closed-Interval-TSpace (a,b));

      assume a <= b;

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

      hence thesis by Lm1;

    end;

    theorem :: TREAL_1:1

    

     Th1: for A be Subset of R^1 st A = [.a, b.] holds A is closed

    proof

      let A be Subset of R^1 ;

      assume

       A1: A = [.a, b.];

      reconsider B = (A ` ) as Subset of ( TopSpaceMetr RealSpace ) by TOPMETR:def 6;

      reconsider a, b as Real;

      reconsider D = B as Subset of RealSpace by TOPMETR: 12;

      set C = (D ` );

      

       A2: the carrier of RealSpace = the carrier of ( TopSpaceMetr RealSpace ) by TOPMETR: 12;

      for c be Point of RealSpace st c in B holds ex r be Real st r > 0 & ( Ball (c,r)) c= B

      proof

        let c be Point of RealSpace ;

        reconsider n = c as Element of REAL by METRIC_1:def 13;

        assume c in B;

        then not n in [.a, b.] by A1, XBOOLE_0:def 5;

        then

         A3: not n in { p where p be Real : a <= p & p <= b } by RCOMP_1:def 1;

        now

          per cases by A3;

            suppose

             A4: not a <= n;

            take r = (a - n);

            now

              let x be object;

              assume

               A5: x in ( Ball (c,r));

              then

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

              reconsider u = x as Point of RealSpace by A5;

              ( Ball (c,r)) = { q where q be Element of RealSpace : ( dist (c,q)) < r } by METRIC_1: 17;

              then ex v be Element of RealSpace st v = u & ( dist (c,v)) < r by A5;

              then ( real_dist . (t,n)) < r by METRIC_1:def 1, METRIC_1:def 13;

              then

               A6: |.(t - n).| < r by METRIC_1:def 12;

              (t - n) <= |.(t - n).| by ABSVALUE: 4;

              then (t - n) < (a - n) by A6, XXREAL_0: 2;

              then not ex q be Real st q = t & a <= q & q <= b by XREAL_1: 9;

              then not t in { p where p be Real : a <= p & p <= b };

              then not u in C by A1, A2, RCOMP_1:def 1, TOPMETR:def 6;

              hence x in B by SUBSET_1: 29;

            end;

            hence r > 0 & ( Ball (c,r)) c= B by A4, XREAL_1: 50;

          end;

            suppose

             A7: not n <= b;

            take r = (n - b);

            now

              let x be object;

              assume

               A8: x in ( Ball (c,r));

              then

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

              reconsider u = x as Point of RealSpace by A8;

              ( Ball (c,r)) = { q where q be Element of RealSpace : ( dist (c,q)) < r } by METRIC_1: 17;

              then ex v be Element of RealSpace st v = u & ( dist (c,v)) < r by A8;

              then ( real_dist . (n,t)) < r by METRIC_1:def 1, METRIC_1:def 13;

              then

               A9: |.(n - t).| < r by METRIC_1:def 12;

              (n - t) <= |.(n - t).| by ABSVALUE: 4;

              then (n - t) < (n - b) by A9, XXREAL_0: 2;

              then not ex q be Real st q = t & a <= q & q <= b by XREAL_1: 10;

              then not t in { p where p be Real : a <= p & p <= b };

              then not u in C by A1, A2, RCOMP_1:def 1, TOPMETR:def 6;

              hence x in B by SUBSET_1: 29;

            end;

            hence r > 0 & ( Ball (c,r)) c= B by A7, XREAL_1: 50;

          end;

        end;

        hence ex r be Real st r > 0 & ( Ball (c,r)) c= B;

      end;

      then (A ` ) is open by TOPMETR: 15, TOPMETR:def 6;

      hence thesis by TOPS_1: 3;

    end;

    theorem :: TREAL_1:2

    

     Th2: a <= b implies ( Closed-Interval-TSpace (a,b)) is closed

    proof

      assume a <= b;

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

      then for A be Subset of R^1 holds A = the carrier of ( Closed-Interval-TSpace (a,b)) implies A is closed by Th1;

      hence thesis by BORSUK_1:def 11;

    end;

    theorem :: TREAL_1:3

    a <= c & d <= b & c <= d implies ( Closed-Interval-TSpace (c,d)) is closed SubSpace of ( Closed-Interval-TSpace (a,b))

    proof

      assume that

       A1: a <= c and

       A2: d <= b and

       A3: c <= d;

       [.c, d.] c= [.a, b.] by A1, A2, XXREAL_1: 34;

      then

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

      

       A5: ( Closed-Interval-TSpace (c,d)) is closed SubSpace of R^1 by A3, Th2;

      a <= d by A1, A3, XXREAL_0: 2;

      then the carrier of ( Closed-Interval-TSpace (c,d)) c= the carrier of ( Closed-Interval-TSpace (a,b)) by A2, A4, TOPMETR: 18, XXREAL_0: 2;

      hence thesis by A5, TSEP_1: 14;

    end;

    theorem :: TREAL_1:4

    a <= c & b <= d & c <= b implies ( Closed-Interval-TSpace (a,d)) = (( Closed-Interval-TSpace (a,b)) union ( Closed-Interval-TSpace (c,d))) & ( Closed-Interval-TSpace (c,b)) = (( Closed-Interval-TSpace (a,b)) meet ( Closed-Interval-TSpace (c,d)))

    proof

      assume that

       A1: a <= c and

       A2: b <= d and

       A3: c <= b;

      

       A4: the carrier of ( Closed-Interval-TSpace (a,b)) = [.a, b.] & the carrier of ( Closed-Interval-TSpace (c,d)) = [.c, d.] by A1, A2, A3, TOPMETR: 18, XXREAL_0: 2;

      a <= b by A1, A3, XXREAL_0: 2;

      then

       A5: the carrier of ( Closed-Interval-TSpace (a,d)) = [.a, d.] by A2, TOPMETR: 18, XXREAL_0: 2;

      

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

      ( [.a, b.] \/ [.c, d.]) = [.a, d.] by A1, A2, A3, XXREAL_1: 174;

      hence ( Closed-Interval-TSpace (a,d)) = (( Closed-Interval-TSpace (a,b)) union ( Closed-Interval-TSpace (c,d))) by A4, A5, TSEP_1:def 2;

      

       A7: ( [.a, b.] /\ [.c, d.]) = [.c, b.] by A1, A2, XXREAL_1: 143;

      then (the carrier of ( Closed-Interval-TSpace (a,b)) /\ the carrier of ( Closed-Interval-TSpace (c,d))) <> {} by A3, A4, XXREAL_1: 1;

      then the carrier of ( Closed-Interval-TSpace (a,b)) meets the carrier of ( Closed-Interval-TSpace (c,d)) by XBOOLE_0:def 7;

      then ( Closed-Interval-TSpace (a,b)) meets ( Closed-Interval-TSpace (c,d)) by TSEP_1:def 3;

      hence thesis by A4, A6, A7, TSEP_1:def 4;

    end;

    definition

      let a,b be Real;

      assume

       A1: a <= b;

      :: TREAL_1:def1

      func (#) (a,b) -> Point of ( Closed-Interval-TSpace (a,b)) equals

      : Def1: a;

      coherence

      proof

        a in [.a, b.] by A1, XXREAL_1: 1;

        hence thesis by A1, TOPMETR: 18;

      end;

      correctness ;

      :: TREAL_1:def2

      func (a,b) (#) -> Point of ( Closed-Interval-TSpace (a,b)) equals

      : Def2: b;

      coherence

      proof

        b in [.a, b.] by A1, XXREAL_1: 1;

        hence thesis by A1, TOPMETR: 18;

      end;

      correctness ;

    end

    theorem :: TREAL_1:5

     0[01] = ( (#) ( 0 ,1)) & 1[01] = (( 0 ,1) (#) ) by Def1, Def2, BORSUK_1:def 14, BORSUK_1:def 15;

    theorem :: TREAL_1:6

    a <= b & b <= c implies ( (#) (a,b)) = ( (#) (a,c)) & ((b,c) (#) ) = ((a,c) (#) )

    proof

      assume that

       A1: a <= b and

       A2: b <= c;

      

      thus ( (#) (a,b)) = a by A1, Def1

      .= ( (#) (a,c)) by A1, A2, Def1, XXREAL_0: 2;

      

      thus ((b,c) (#) ) = c by A2, Def2

      .= ((a,c) (#) ) by A1, A2, Def2, XXREAL_0: 2;

    end;

    begin

    definition

      let a,b be Real;

      let t1,t2 be Point of ( Closed-Interval-TSpace (a,b));

      :: TREAL_1:def3

      func L[01] (t1,t2) -> Function of ( Closed-Interval-TSpace ( 0 ,1)), ( Closed-Interval-TSpace (a,b)) means

      : Def3: for s be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds (it . s) = (((1 - s) * t1) + (s * t2));

      existence

      proof

        reconsider r1 = t1, r2 = t2 as Element of REAL by A1, Lm2;

        deffunc U( Real) = ( In ((((1 - $1) * r1) + ($1 * r2)), REAL ));

        consider LI be Function of REAL , REAL such that

         A2: for r be Element of REAL holds (LI . r) = U(r) from FUNCT_2:sch 4;

        

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

        now

          let y be object;

          assume

           A4: y in ( rng (LI | [. 0 , 1.]));

          then

          reconsider d = y as Element of REAL ;

          y in (LI .: [. 0 , 1.]) by A4, RELAT_1: 115;

          then

          consider x be object such that x in ( dom LI) and

           A5: x in [. 0 , 1.] and

           A6: y = (LI . x) by FUNCT_1:def 6;

          reconsider c = x as Element of REAL by A5;

          

           A7: d = U(c) by A2, A6;

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

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

          then

           A8: ex v1 be Real st v1 = r1 & a <= v1 & v1 <= b;

          c in { p where p be Real : 0 <= p & p <= 1 } by A5, RCOMP_1:def 1;

          then

           A9: ex u be Real st u = c & 0 <= u & u <= 1;

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

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

          then

           A10: ex v2 be Real st v2 = r2 & a <= v2 & v2 <= b;

          then

           A11: (c * a) <= (c * r2) by A9, XREAL_1: 64;

          

           A12: (c * r2) <= (c * b) by A9, A10, XREAL_1: 64;

          

           A13: 0 <= (1 - c) by A9, XREAL_1: 48;

          then ((1 - c) * r1) <= ((1 - c) * b) by A8, XREAL_1: 64;

          then

           A14: d <= (((1 - c) * b) + (c * b)) by A7, A12, XREAL_1: 7;

          ((1 - c) * a) <= ((1 - c) * r1) by A8, A13, XREAL_1: 64;

          then (((1 - c) * a) + (c * a)) <= d by A7, A11, XREAL_1: 7;

          then y in { q where q be Real : a <= q & q <= b } by A14;

          hence y in [.a, b.] by RCOMP_1:def 1;

        end;

        then

         A15: ( rng (LI | [. 0 , 1.])) c= the carrier of ( Closed-Interval-TSpace (a,b)) by A3;

        

         A16: ( dom (LI | [. 0 , 1.])) = (( dom LI) /\ [. 0 , 1.]) by RELAT_1: 61;

         [. 0 , 1.] = ( REAL /\ [. 0 , 1.]) & ( dom LI) = REAL by FUNCT_2:def 1, XBOOLE_1: 28;

        then ( dom (LI | [. 0 , 1.])) = the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by A16, TOPMETR: 18;

        then

        reconsider F = (LI | [. 0 , 1.]) as Function of ( Closed-Interval-TSpace ( 0 ,1)), ( Closed-Interval-TSpace (a,b)) by A15, FUNCT_2:def 1, RELSET_1: 4;

        take F;

        let s be Point of ( Closed-Interval-TSpace ( 0 ,1));

        

         A17: s in REAL by XREAL_0:def 1;

        the carrier of ( Closed-Interval-TSpace ( 0 ,1)) = [. 0 , 1.] by TOPMETR: 18;

        

        hence (F . s) = (LI . s) by FUNCT_1: 49

        .= U(s) by A2, A17

        .= (((1 - s) * t1) + (s * t2));

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( Closed-Interval-TSpace ( 0 ,1)), ( Closed-Interval-TSpace (a,b));

        assume

         A18: for s be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds (F1 . s) = (((1 - s) * t1) + (s * t2));

        assume

         A19: for s be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds (F2 . s) = (((1 - s) * t1) + (s * t2));

        for s be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds (F1 . s) = (F2 . s)

        proof

          reconsider r1 = t1, r2 = t2 as Real;

          let s be Point of ( Closed-Interval-TSpace ( 0 ,1));

          reconsider r = s as Real;

          

          thus (F1 . s) = (((1 - r) * r1) + (r * r2)) by A18

          .= (F2 . s) by A19;

        end;

        hence F1 = F2;

      end;

    end

    theorem :: TREAL_1:7

    

     Th7: a <= b implies for t1,t2 be Point of ( Closed-Interval-TSpace (a,b)) holds for s be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds (( L[01] (t1,t2)) . s) = (((t2 - t1) * s) + t1)

    proof

      assume

       A1: a <= b;

      let t1,t2 be Point of ( Closed-Interval-TSpace (a,b));

      let s be Point of ( Closed-Interval-TSpace ( 0 ,1));

      

      thus (( L[01] (t1,t2)) . s) = (((1 - s) * t1) + (s * t2)) by A1, Def3

      .= (((t2 - t1) * s) + t1);

    end;

    theorem :: TREAL_1:8

    

     Th8: a <= b implies for t1,t2 be Point of ( Closed-Interval-TSpace (a,b)) holds ( L[01] (t1,t2)) is continuous

    proof

      assume

       A1: a <= b;

      let t1,t2 be Point of ( Closed-Interval-TSpace (a,b));

      reconsider r1 = t1, r2 = t2 as Real;

      deffunc U( Real) = ( In ((((r2 - r1) * $1) + r1), REAL ));

      consider L be Function of REAL , REAL such that

       A2: for r be Element of REAL holds (L . r) = U(r) from FUNCT_2:sch 4;

      

       A3: for r be Real holds (L . r) = (((r2 - r1) * r) + r1)

      proof

        let r be Real;

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

        (L . r) = U(r) by A2;

        hence thesis;

      end;

      reconsider f = L as Function of R^1 , R^1 by TOPMETR: 17;

      

       A4: for s be Point of ( Closed-Interval-TSpace ( 0 ,1)), w be Point of R^1 st s = w holds (( L[01] (t1,t2)) . s) = (f . w)

      proof

        let s be Point of ( Closed-Interval-TSpace ( 0 ,1)), w be Point of R^1 ;

        reconsider r = s as Real;

        assume

         A5: s = w;

        

        thus (( L[01] (t1,t2)) . s) = U(r) by A1, Th7

        .= (f . w) by A3, A5;

      end;

      

       A6: [. 0 , 1.] = the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by TOPMETR: 18;

      

       A7: f is continuous by A3, TOPMETR: 21;

      for s be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds ( L[01] (t1,t2)) is_continuous_at s

      proof

        let s be Point of ( Closed-Interval-TSpace ( 0 ,1));

        reconsider w = s as Point of R^1 by A6, TARSKI:def 3, TOPMETR: 17;

        for G be Subset of ( Closed-Interval-TSpace (a,b)) st G is open & (( L[01] (t1,t2)) . s) in G holds ex H be Subset of ( Closed-Interval-TSpace ( 0 ,1)) st H is open & s in H & (( L[01] (t1,t2)) .: H) c= G

        proof

          let G be Subset of ( Closed-Interval-TSpace (a,b));

          assume G is open;

          then

          consider G0 be Subset of R^1 such that

           A8: G0 is open and

           A9: (G0 /\ ( [#] ( Closed-Interval-TSpace (a,b)))) = G by TOPS_2: 24;

          

           A10: f is_continuous_at w by A7, TMAP_1: 44;

          assume (( L[01] (t1,t2)) . s) in G;

          then (f . w) in G by A4;

          then (f . w) in G0 by A9, XBOOLE_0:def 4;

          then

          consider H0 be Subset of R^1 such that

           A11: H0 is open and

           A12: w in H0 and

           A13: (f .: H0) c= G0 by A8, A10, TMAP_1: 43;

          now

            reconsider H = (H0 /\ ( [#] ( Closed-Interval-TSpace ( 0 ,1)))) as Subset of ( Closed-Interval-TSpace ( 0 ,1));

            take H;

            thus H is open by A11, TOPS_2: 24;

            thus s in H by A12, XBOOLE_0:def 4;

            thus (( L[01] (t1,t2)) .: H) c= G

            proof

              let t be object;

              assume t in (( L[01] (t1,t2)) .: H);

              then

              consider r be object such that r in ( dom ( L[01] (t1,t2))) and

               A14: r in H and

               A15: t = (( L[01] (t1,t2)) . r) by FUNCT_1:def 6;

              

               A16: r in the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by A14;

              reconsider r as Point of ( Closed-Interval-TSpace ( 0 ,1)) by A14;

              r in ( dom ( L[01] (t1,t2))) by A16, FUNCT_2:def 1;

              then

               A17: t in (( L[01] (t1,t2)) .: the carrier of ( Closed-Interval-TSpace ( 0 ,1))) by A15, FUNCT_1:def 6;

              reconsider p = r as Point of R^1 by A6, TARSKI:def 3, TOPMETR: 17;

              p in ( [#] R^1 );

              then

               A18: p in ( dom f) by FUNCT_2:def 1;

              t = (f . p) & p in H0 by A4, A14, A15, XBOOLE_0:def 4;

              then t in (f .: H0) by A18, FUNCT_1:def 6;

              hence thesis by A9, A13, A17, XBOOLE_0:def 4;

            end;

          end;

          hence thesis;

        end;

        hence thesis by TMAP_1: 43;

      end;

      hence thesis by TMAP_1: 44;

    end;

    theorem :: TREAL_1:9

    a <= b implies for t1,t2 be Point of ( Closed-Interval-TSpace (a,b)) holds (( L[01] (t1,t2)) . ( (#) ( 0 ,1))) = t1 & (( L[01] (t1,t2)) . (( 0 ,1) (#) )) = t2

    proof

      assume

       A1: a <= b;

      let t1,t2 be Point of ( Closed-Interval-TSpace (a,b));

      reconsider r1 = t1, r2 = t2 as Real;

       0 = ( (#) ( 0 ,1)) by Def1;

      

      hence (( L[01] (t1,t2)) . ( (#) ( 0 ,1))) = (((1 - 0 ) * r1) + ( 0 * r2)) by A1, Def3

      .= t1;

      1 = (( 0 ,1) (#) ) by Def2;

      

      hence (( L[01] (t1,t2)) . (( 0 ,1) (#) )) = (((1 - 1) * r1) + (1 * r2)) by A1, Def3

      .= t2;

    end;

    theorem :: TREAL_1:10

    ( L[01] (( (#) ( 0 ,1)),(( 0 ,1) (#) ))) = ( id ( Closed-Interval-TSpace ( 0 ,1)))

    proof

      for x be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds (( L[01] (( (#) ( 0 ,1)),(( 0 ,1) (#) ))) . x) = x

      proof

        let x be Point of ( Closed-Interval-TSpace ( 0 ,1));

        reconsider y = x as Real;

        ( (#) ( 0 ,1)) = 0 & (( 0 ,1) (#) ) = 1 by Def1, Def2;

        

        hence (( L[01] (( (#) ( 0 ,1)),(( 0 ,1) (#) ))) . x) = (((1 - y) * 0 ) + (y * 1)) by Def3

        .= x;

      end;

      hence thesis by FUNCT_2: 124;

    end;

    definition

      let a,b be Real;

      let t1,t2 be Point of ( Closed-Interval-TSpace ( 0 ,1));

      :: TREAL_1:def4

      func P[01] (a,b,t1,t2) -> Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace ( 0 ,1)) means

      : Def4: for s be Point of ( Closed-Interval-TSpace (a,b)) holds (it . s) = ((((b - s) * t1) + ((s - a) * t2)) / (b - a));

      existence

      proof

        reconsider a1 = a, b1 = b as Real;

        reconsider r1 = t1, r2 = t2 as Real;

        deffunc U( Real) = ( In (((((b1 - $1) * r1) + (($1 - a1) * r2)) / (b1 - a1)), REAL ));

        consider PI be Function of REAL , REAL such that

         A2: for r be Element of REAL holds (PI . r) = U(r) from FUNCT_2:sch 4;

        

         A3: [. 0 , 1.] = the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by TOPMETR: 18;

        now

          let y be object;

          assume

           A4: y in ( rng (PI | [.a, b.]));

          then

          reconsider d = y as Real;

          y in (PI .: [.a, b.]) by A4, RELAT_1: 115;

          then

          consider x be object such that x in ( dom PI) and

           A5: x in [.a, b.] and

           A6: y = (PI . x) by FUNCT_1:def 6;

          reconsider c = x as Element of REAL by A5;

          

           A7: d = U(c) by A2, A6;

          r1 in [. 0 , 1.] by A3;

          then r1 in { p where p be Real : 0 <= p & p <= 1 } by RCOMP_1:def 1;

          then

           A8: ex v1 be Real st v1 = r1 & 0 <= v1 & v1 <= 1;

          c in { p where p be Real : a <= p & p <= b } by A5, RCOMP_1:def 1;

          then

           A9: ex u be Real st u = c & a <= u & u <= b;

          then

           A10: 0 <= (c - a) by XREAL_1: 48;

          r2 in [. 0 , 1.] by A3;

          then r2 in { p where p be Real : 0 <= p & p <= 1 } by RCOMP_1:def 1;

          then

           A11: ex v2 be Real st v2 = r2 & 0 <= v2 & v2 <= 1;

          then

           A12: ((c - a) * r2) <= (c - a) by A10, XREAL_1: 153;

          

           A13: 0 < (b - a) by A1, XREAL_1: 50;

          

           A14: 0 <= (b - c) by A9, XREAL_1: 48;

          then ((b - c) * r1) <= (b - c) by A8, XREAL_1: 153;

          then (((b - c) * r1) + ((c - a) * r2)) <= ((b + ( - c)) + (c - a)) by A12, XREAL_1: 7;

          then d <= ((b - a) / (b - a)) by A13, A7, XREAL_1: 72;

          then d <= 1 by A13, XCMPLX_1: 60;

          then y in { q where q be Real : 0 <= q & q <= 1 } by A8, A11, A13, A7, A14, A10;

          hence y in [. 0 , 1.] by RCOMP_1:def 1;

        end;

        then

         A15: ( rng (PI | [.a, b.])) c= the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by A3;

        

         A16: ( dom (PI | [.a, b.])) = (( dom PI) /\ [.a, b.]) by RELAT_1: 61;

         [.a, b.] = ( REAL /\ [.a, b.]) & ( dom PI) = REAL by FUNCT_2:def 1, XBOOLE_1: 28;

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

        then

        reconsider F = (PI | [.a, b.]) as Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace ( 0 ,1)) by A15, FUNCT_2:def 1, RELSET_1: 4;

        take F;

        let s be Point of ( Closed-Interval-TSpace (a,b));

        

         A17: s in REAL by XREAL_0:def 1;

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

        

        hence (F . s) = (PI . s) by FUNCT_1: 49

        .= U(s) by A2, A17

        .= ((((b - s) * t1) + ((s - a) * t2)) / (b - a));

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace ( 0 ,1));

        assume

         A18: for s be Point of ( Closed-Interval-TSpace (a,b)) holds (F1 . s) = ((((b - s) * t1) + ((s - a) * t2)) / (b - a));

        assume

         A19: for s be Point of ( Closed-Interval-TSpace (a,b)) holds (F2 . s) = ((((b - s) * t1) + ((s - a) * t2)) / (b - a));

        let s be Point of ( Closed-Interval-TSpace (a,b));

        reconsider r = s as Real;

        reconsider r1 = t1, r2 = t2 as Real;

        

        thus (F1 . s) = ((((b - r) * r1) + ((r - a) * r2)) / (b - a)) by A18

        .= (F2 . s) by A19;

      end;

    end

    theorem :: TREAL_1:11

    

     Th11: a < b implies for t1,t2 be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds for s be Point of ( Closed-Interval-TSpace (a,b)) holds (( P[01] (a,b,t1,t2)) . s) = ((((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a)))

    proof

      assume

       A1: a < b;

      let t1,t2 be Point of ( Closed-Interval-TSpace ( 0 ,1));

      let s be Point of ( Closed-Interval-TSpace (a,b));

      

      thus (( P[01] (a,b,t1,t2)) . s) = ((((b - s) * t1) + ((s - a) * t2)) / (b - a)) by A1, Def4

      .= (((s * (t2 - t1)) + ((b * t1) - (a * t2))) / (b - a))

      .= (((s * (t2 - t1)) / (b - a)) + (((b * t1) - (a * t2)) / (b - a))) by XCMPLX_1: 62

      .= (((s * (t2 - t1)) * (1 / (b - a))) + (((b * t1) - (a * t2)) / (b - a))) by XCMPLX_1: 99

      .= ((((t2 - t1) * (1 / (b - a))) * s) + (((b * t1) - (a * t2)) / (b - a)))

      .= ((((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a))) by XCMPLX_1: 99;

    end;

    theorem :: TREAL_1:12

    

     Th12: a < b implies for t1,t2 be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds ( P[01] (a,b,t1,t2)) is continuous

    proof

      assume

       A1: a < b;

      reconsider a, b as Real;

      

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

      let t1,t2 be Point of ( Closed-Interval-TSpace ( 0 ,1));

      reconsider r1 = t1, r2 = t2 as Real;

      deffunc U( Real) = ( In (((((r2 - r1) / (b - a)) * $1) + (((b * r1) - (a * r2)) / (b - a))), REAL ));

      consider P be Function of REAL , REAL such that

       A3: for r be Element of REAL holds (P . r) = U(r) from FUNCT_2:sch 4;

      

       A4: for r be Real holds (P . r) = ((((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (b - a)))

      proof

        let r be Real;

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

        (P . r) = U(r) by A3;

        hence thesis;

      end;

      reconsider f = P as Function of R^1 , R^1 by TOPMETR: 17;

      

       A5: for s be Point of ( Closed-Interval-TSpace (a,b)), w be Point of R^1 st s = w holds (( P[01] (a,b,t1,t2)) . s) = (f . w)

      proof

        let s be Point of ( Closed-Interval-TSpace (a,b)), w be Point of R^1 ;

        reconsider r = s as Real;

        assume

         A6: s = w;

        

        thus (( P[01] (a,b,t1,t2)) . s) = ((((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (b - a))) by A1, Th11

        .= U(r)

        .= (f . w) by A4, A6;

      end;

      

       A7: f is continuous by A4, TOPMETR: 21;

      for s be Point of ( Closed-Interval-TSpace (a,b)) holds ( P[01] (a,b,t1,t2)) is_continuous_at s

      proof

        let s be Point of ( Closed-Interval-TSpace (a,b));

        reconsider w = s as Point of R^1 by A2, TARSKI:def 3, TOPMETR: 17;

        for G be Subset of ( Closed-Interval-TSpace ( 0 ,1)) st G is open & (( P[01] (a,b,t1,t2)) . s) in G holds ex H be Subset of ( Closed-Interval-TSpace (a,b)) st H is open & s in H & (( P[01] (a,b,t1,t2)) .: H) c= G

        proof

          let G be Subset of ( Closed-Interval-TSpace ( 0 ,1));

          assume G is open;

          then

          consider G0 be Subset of R^1 such that

           A8: G0 is open and

           A9: (G0 /\ ( [#] ( Closed-Interval-TSpace ( 0 ,1)))) = G by TOPS_2: 24;

          

           A10: f is_continuous_at w by A7, TMAP_1: 44;

          assume (( P[01] (a,b,t1,t2)) . s) in G;

          then (f . w) in G by A5;

          then (f . w) in G0 by A9, XBOOLE_0:def 4;

          then

          consider H0 be Subset of R^1 such that

           A11: H0 is open and

           A12: w in H0 and

           A13: (f .: H0) c= G0 by A8, A10, TMAP_1: 43;

          now

            reconsider H = (H0 /\ ( [#] ( Closed-Interval-TSpace (a,b)))) as Subset of ( Closed-Interval-TSpace (a,b));

            take H;

            thus H is open by A11, TOPS_2: 24;

            thus s in H by A12, XBOOLE_0:def 4;

            thus (( P[01] (a,b,t1,t2)) .: H) c= G

            proof

              let t be object;

              assume t in (( P[01] (a,b,t1,t2)) .: H);

              then

              consider r be object such that r in ( dom ( P[01] (a,b,t1,t2))) and

               A14: r in H and

               A15: t = (( P[01] (a,b,t1,t2)) . r) by FUNCT_1:def 6;

              

               A16: r in the carrier of ( Closed-Interval-TSpace (a,b)) by A14;

              reconsider r as Point of ( Closed-Interval-TSpace (a,b)) by A14;

              r in ( dom ( P[01] (a,b,t1,t2))) by A16, FUNCT_2:def 1;

              then

               A17: t in (( P[01] (a,b,t1,t2)) .: the carrier of ( Closed-Interval-TSpace (a,b))) by A15, FUNCT_1:def 6;

              reconsider p = r as Point of R^1 by A2, TARSKI:def 3, TOPMETR: 17;

              p in ( [#] R^1 );

              then

               A18: p in ( dom f) by FUNCT_2:def 1;

              t = (f . p) & p in H0 by A5, A14, A15, XBOOLE_0:def 4;

              then t in (f .: H0) by A18, FUNCT_1:def 6;

              hence thesis by A9, A13, A17, XBOOLE_0:def 4;

            end;

          end;

          hence thesis;

        end;

        hence thesis by TMAP_1: 43;

      end;

      hence thesis by TMAP_1: 44;

    end;

    theorem :: TREAL_1:13

    a < b implies for t1,t2 be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds (( P[01] (a,b,t1,t2)) . ( (#) (a,b))) = t1 & (( P[01] (a,b,t1,t2)) . ((a,b) (#) )) = t2

    proof

      assume

       A1: a < b;

      then

       A2: (b - a) <> 0 ;

      let t1,t2 be Point of ( Closed-Interval-TSpace ( 0 ,1));

      reconsider r1 = t1, r2 = t2 as Real;

      a = ( (#) (a,b)) by A1, Def1;

      

      hence (( P[01] (a,b,t1,t2)) . ( (#) (a,b))) = ((((b - a) * r1) + ((a - a) * r2)) / (b - a)) by A1, Def4

      .= t1 by A2, XCMPLX_1: 89;

      b = ((a,b) (#) ) by A1, Def2;

      

      hence (( P[01] (a,b,t1,t2)) . ((a,b) (#) )) = ((((b - b) * r1) + ((b - a) * r2)) / (b - a)) by A1, Def4

      .= t2 by A2, XCMPLX_1: 89;

    end;

    theorem :: TREAL_1:14

    ( P[01] ( 0 ,1,( (#) ( 0 ,1)),(( 0 ,1) (#) ))) = ( id ( Closed-Interval-TSpace ( 0 ,1)))

    proof

      for x be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds (( P[01] ( 0 ,1,( (#) ( 0 ,1)),(( 0 ,1) (#) ))) . x) = x

      proof

        let x be Point of ( Closed-Interval-TSpace ( 0 ,1));

        reconsider y = x as Real;

        ( (#) ( 0 ,1)) = 0 & (( 0 ,1) (#) ) = 1 by Def1, Def2;

        

        hence (( P[01] ( 0 ,1,( (#) ( 0 ,1)),(( 0 ,1) (#) ))) . x) = ((((1 - y) * 0 ) + ((y - 0 ) * 1)) / (1 - 0 )) by Def4

        .= x;

      end;

      hence thesis by FUNCT_2: 124;

    end;

    theorem :: TREAL_1:15

    

     Th15: a < b implies ( id ( Closed-Interval-TSpace (a,b))) = (( L[01] (( (#) (a,b)),((a,b) (#) ))) * ( P[01] (a,b,( (#) ( 0 ,1)),(( 0 ,1) (#) )))) & ( id ( Closed-Interval-TSpace ( 0 ,1))) = (( P[01] (a,b,( (#) ( 0 ,1)),(( 0 ,1) (#) ))) * ( L[01] (( (#) (a,b)),((a,b) (#) ))))

    proof

      

       A1: 0 = ( (#) ( 0 ,1)) & 1 = (( 0 ,1) (#) ) by Def1, Def2;

      set L = ( L[01] (( (#) (a,b)),((a,b) (#) ))), P = ( P[01] (a,b,( (#) ( 0 ,1)),(( 0 ,1) (#) )));

      assume

       A2: a < b;

      then

       A3: (b - a) <> 0 ;

      

       A4: a = ( (#) (a,b)) & b = ((a,b) (#) ) by A2, Def1, Def2;

      for c be Point of ( Closed-Interval-TSpace (a,b)) holds ((L * P) . c) = c

      proof

        let c be Point of ( Closed-Interval-TSpace (a,b));

        reconsider r = c as Real;

        

         A5: (P . c) = ((((b - r) * 0 ) + ((r - a) * 1)) / (b - a)) by A2, A1, Def4

        .= ((r - a) / (b - a));

        

        thus ((L * P) . c) = (L . (P . c)) by FUNCT_2: 15

        .= (((1 - ((r - a) / (b - a))) * a) + (((r - a) / (b - a)) * b)) by A2, A4, A5, Def3

        .= (((((1 * (b - a)) - (r - a)) / (b - a)) * a) + (((r - a) / (b - a)) * b)) by A3, XCMPLX_1: 127

        .= ((((b - r) / (b - a)) * (a / 1)) + (((r - a) / (b - a)) * b))

        .= ((((b - r) * a) / (1 * (b - a))) + (((r - a) / (b - a)) * b)) by XCMPLX_1: 76

        .= ((((b - r) * a) / (b - a)) + (((r - a) / (b - a)) * (b / 1)))

        .= ((((b - r) * a) / (b - a)) + (((r - a) * b) / (1 * (b - a)))) by XCMPLX_1: 76

        .= ((((a * b) - (a * r)) + ((r - a) * b)) / (b - a)) by XCMPLX_1: 62

        .= (((b - a) * r) / (b - a))

        .= c by A3, XCMPLX_1: 89;

      end;

      hence ( id ( Closed-Interval-TSpace (a,b))) = (L * P) by FUNCT_2: 124;

      for c be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds ((P * L) . c) = c

      proof

        let c be Point of ( Closed-Interval-TSpace ( 0 ,1));

        reconsider r = c as Real;

        

         A6: (L . c) = (((1 - r) * a) + (r * b)) by A2, A4, Def3

        .= ((r * (b - a)) + a);

        

        thus ((P * L) . c) = (P . (L . c)) by FUNCT_2: 15

        .= ((((b - ((r * (b - a)) + a)) * 0 ) + ((((r * (b - a)) + a) - a) * 1)) / (b - a)) by A2, A1, A6, Def4

        .= c by A3, XCMPLX_1: 89;

      end;

      hence thesis by FUNCT_2: 124;

    end;

    theorem :: TREAL_1:16

    

     Th16: a < b implies ( id ( Closed-Interval-TSpace (a,b))) = (( L[01] (((a,b) (#) ),( (#) (a,b)))) * ( P[01] (a,b,(( 0 ,1) (#) ),( (#) ( 0 ,1))))) & ( id ( Closed-Interval-TSpace ( 0 ,1))) = (( P[01] (a,b,(( 0 ,1) (#) ),( (#) ( 0 ,1)))) * ( L[01] (((a,b) (#) ),( (#) (a,b)))))

    proof

      

       A1: 0 = ( (#) ( 0 ,1)) & 1 = (( 0 ,1) (#) ) by Def1, Def2;

      set L = ( L[01] (((a,b) (#) ),( (#) (a,b)))), P = ( P[01] (a,b,(( 0 ,1) (#) ),( (#) ( 0 ,1))));

      assume

       A2: a < b;

      then

       A3: (b - a) <> 0 ;

      

       A4: a = ( (#) (a,b)) & b = ((a,b) (#) ) by A2, Def1, Def2;

      for c be Point of ( Closed-Interval-TSpace (a,b)) holds ((L * P) . c) = c

      proof

        let c be Point of ( Closed-Interval-TSpace (a,b));

        reconsider r = c as Real;

        

         A5: (P . c) = ((((b - r) * 1) + ((r - a) * 0 )) / (b - a)) by A2, A1, Def4

        .= ((b - r) / (b - a));

        

        thus ((L * P) . c) = (L . (P . c)) by FUNCT_2: 15

        .= (((1 - ((b - r) / (b - a))) * b) + (((b - r) / (b - a)) * a)) by A2, A4, A5, Def3

        .= (((((1 * (b - a)) - (b - r)) / (b - a)) * b) + (((b - r) / (b - a)) * a)) by A3, XCMPLX_1: 127

        .= ((((r - a) / (b - a)) * (b / 1)) + (((b - r) / (b - a)) * a))

        .= ((((r - a) * b) / (1 * (b - a))) + (((b - r) / (b - a)) * a)) by XCMPLX_1: 76

        .= ((((r - a) * b) / (b - a)) + (((b - r) / (b - a)) * (a / 1)))

        .= ((((r - a) * b) / (b - a)) + (((b - r) * a) / (1 * (b - a)))) by XCMPLX_1: 76

        .= ((((b * r) - (b * a)) + ((b - r) * a)) / (b - a)) by XCMPLX_1: 62

        .= (((b - a) * r) / (b - a))

        .= c by A3, XCMPLX_1: 89;

      end;

      hence ( id ( Closed-Interval-TSpace (a,b))) = (L * P) by FUNCT_2: 124;

      for c be Point of ( Closed-Interval-TSpace ( 0 ,1)) holds ((P * L) . c) = c

      proof

        let c be Point of ( Closed-Interval-TSpace ( 0 ,1));

        reconsider r = c as Real;

        

         A6: (L . c) = (((1 - r) * b) + (r * a)) by A2, A4, Def3

        .= ((r * (a - b)) + b);

        

        thus ((P * L) . c) = (P . (L . c)) by FUNCT_2: 15

        .= ((((b - ((r * (a - b)) + b)) * 1) + ((((r * (a - b)) + b) - a) * 0 )) / (b - a)) by A2, A1, A6, Def4

        .= ((r * ( - (a - b))) / (b - a))

        .= c by A3, XCMPLX_1: 89;

      end;

      hence thesis by FUNCT_2: 124;

    end;

    theorem :: TREAL_1:17

    

     Th17: a < b implies ( L[01] (( (#) (a,b)),((a,b) (#) ))) is being_homeomorphism & (( L[01] (( (#) (a,b)),((a,b) (#) ))) " ) = ( P[01] (a,b,( (#) ( 0 ,1)),(( 0 ,1) (#) ))) & ( P[01] (a,b,( (#) ( 0 ,1)),(( 0 ,1) (#) ))) is being_homeomorphism & (( P[01] (a,b,( (#) ( 0 ,1)),(( 0 ,1) (#) ))) " ) = ( L[01] (( (#) (a,b)),((a,b) (#) )))

    proof

      set L = ( L[01] (( (#) (a,b)),((a,b) (#) ))), P = ( P[01] (a,b,( (#) ( 0 ,1)),(( 0 ,1) (#) )));

      assume

       A1: a < b;

      then

       A2: ( id the carrier of ( Closed-Interval-TSpace ( 0 ,1))) = (P * L) by Th15;

      then

       A3: L is one-to-one by FUNCT_2: 23;

      

       A4: L is continuous & P is continuous Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace ( 0 ,1)) by A1, Th8, Th12;

      

       A5: ( id the carrier of ( Closed-Interval-TSpace (a,b))) = ( id ( Closed-Interval-TSpace (a,b)))

      .= (L * P) by A1, Th15;

      then

       A6: L is onto by FUNCT_2: 23;

      then

       A7: ( rng L) = ( [#] ( Closed-Interval-TSpace (a,b)));

      

       A8: (L " ) = (L qua Function " ) by A3, A6, TOPS_2:def 4;

      ( dom L) = ( [#] ( Closed-Interval-TSpace ( 0 ,1))) & P = (L qua Function " ) by A2, A3, A7, FUNCT_2: 30, FUNCT_2:def 1;

      hence ( L[01] (( (#) (a,b)),((a,b) (#) ))) is being_homeomorphism by A3, A7, A8, A4, TOPS_2:def 5;

      thus (( L[01] (( (#) (a,b)),((a,b) (#) ))) " ) = ( P[01] (a,b,( (#) ( 0 ,1)),(( 0 ,1) (#) ))) by A2, A3, A7, A8, FUNCT_2: 30;

      

       A9: P is onto by A2, FUNCT_2: 23;

      then

       A10: ( rng P) = ( [#] ( Closed-Interval-TSpace ( 0 ,1)));

      

       A11: L is continuous Function of ( Closed-Interval-TSpace ( 0 ,1)), ( Closed-Interval-TSpace (a,b)) & P is continuous by A1, Th8, Th12;

      

       A12: P is one-to-one by A5, FUNCT_2: 23;

      

       A13: (P " ) = (P qua Function " ) by A12, A9, TOPS_2:def 4;

      ( dom P) = ( [#] ( Closed-Interval-TSpace (a,b))) & L = (P qua Function " ) by A10, A5, A12, FUNCT_2: 30, FUNCT_2:def 1;

      hence ( P[01] (a,b,( (#) ( 0 ,1)),(( 0 ,1) (#) ))) is being_homeomorphism by A10, A12, A13, A11, TOPS_2:def 5;

      thus thesis by A10, A5, A12, A13, FUNCT_2: 30;

    end;

    theorem :: TREAL_1:18

    a < b implies ( L[01] (((a,b) (#) ),( (#) (a,b)))) is being_homeomorphism & (( L[01] (((a,b) (#) ),( (#) (a,b)))) " ) = ( P[01] (a,b,(( 0 ,1) (#) ),( (#) ( 0 ,1)))) & ( P[01] (a,b,(( 0 ,1) (#) ),( (#) ( 0 ,1)))) is being_homeomorphism & (( P[01] (a,b,(( 0 ,1) (#) ),( (#) ( 0 ,1)))) " ) = ( L[01] (((a,b) (#) ),( (#) (a,b))))

    proof

      set L = ( L[01] (((a,b) (#) ),( (#) (a,b)))), P = ( P[01] (a,b,(( 0 ,1) (#) ),( (#) ( 0 ,1))));

      assume

       A1: a < b;

      then

       A2: ( id the carrier of ( Closed-Interval-TSpace ( 0 ,1))) = (P * L) by Th16;

      then

       A3: L is one-to-one by FUNCT_2: 23;

      

       A4: L is continuous & P is continuous Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace ( 0 ,1)) by A1, Th8, Th12;

      

       A5: ( id the carrier of ( Closed-Interval-TSpace (a,b))) = ( id ( Closed-Interval-TSpace (a,b)))

      .= (L * P) by A1, Th16;

      then

       A6: L is onto by FUNCT_2: 23;

      then

       A7: ( rng L) = ( [#] ( Closed-Interval-TSpace (a,b)));

      

       A8: (L " ) = (L qua Function " ) by A3, A6, TOPS_2:def 4;

      ( dom L) = ( [#] ( Closed-Interval-TSpace ( 0 ,1))) & P = (L qua Function " ) by A2, A3, A7, FUNCT_2: 30, FUNCT_2:def 1;

      hence ( L[01] (((a,b) (#) ),( (#) (a,b)))) is being_homeomorphism by A3, A7, A8, A4, TOPS_2:def 5;

      thus (( L[01] (((a,b) (#) ),( (#) (a,b)))) " ) = ( P[01] (a,b,(( 0 ,1) (#) ),( (#) ( 0 ,1)))) by A2, A3, A7, A8, FUNCT_2: 30;

      

       A9: P is onto by A2, FUNCT_2: 23;

      then

       A10: ( rng P) = ( [#] ( Closed-Interval-TSpace ( 0 ,1)));

      

       A11: L is continuous Function of ( Closed-Interval-TSpace ( 0 ,1)), ( Closed-Interval-TSpace (a,b)) & P is continuous by A1, Th8, Th12;

      

       A12: P is one-to-one by A5, FUNCT_2: 23;

      

       A13: (P " ) = (P qua Function " ) by A12, A9, TOPS_2:def 4;

      ( dom P) = ( [#] ( Closed-Interval-TSpace (a,b))) & L = (P qua Function " ) by A10, A5, A12, FUNCT_2: 30, FUNCT_2:def 1;

      hence ( P[01] (a,b,(( 0 ,1) (#) ),( (#) ( 0 ,1)))) is being_homeomorphism by A10, A12, A13, A11, TOPS_2:def 5;

      thus thesis by A10, A5, A12, A13, FUNCT_2: 30;

    end;

    begin

    theorem :: TREAL_1:19

    

     Th19: I[01] is connected

    proof

      for A,B be Subset of I[01] st ( [#] I[01] ) = (A \/ B) & A <> ( {} I[01] ) & B <> ( {} I[01] ) & A is closed & B is closed holds A meets B

      proof

        let A,B be Subset of I[01] ;

        assume that

         A1: ( [#] I[01] ) = (A \/ B) and

         A2: A <> ( {} I[01] ) and

         A3: B <> ( {} I[01] ) and

         A4: A is closed and

         A5: B is closed;

        reconsider P = A, Q = B as Subset of REAL by BORSUK_1: 40, XBOOLE_1: 1;

        assume

         A6: A misses B;

        set x = the Element of P;

        reconsider x as Real;

         A7:

        now

          take x;

          thus x in P by A2;

        end;

        set x = the Element of Q;

        reconsider x as Real;

         A8:

        now

          take x;

          thus x in Q by A3;

        end;

        

         A9: the carrier of RealSpace = the carrier of ( TopSpaceMetr RealSpace ) by TOPMETR: 12;

         0 is LowerBound of P

        proof

          let r be ExtReal;

          assume r in P;

          then r in [. 0 , 1.] by BORSUK_1: 40;

          then r in { w where w be Real : 0 <= w & w <= 1 } by RCOMP_1:def 1;

          then ex u be Real st u = r & 0 <= u & u <= 1;

          hence 0 <= r;

        end;

        then

         A10: P is bounded_below;

         0 is LowerBound of Q

        proof

          let r be ExtReal;

          assume r in Q;

          then r in [. 0 , 1.] by BORSUK_1: 40;

          then r in { w where w be Real : 0 <= w & w <= 1 } by RCOMP_1:def 1;

          then ex u be Real st u = r & 0 <= u & u <= 1;

          hence 0 <= r;

        end;

        then

         A11: Q is bounded_below;

        reconsider A0 = P, B0 = Q as Subset of R^1 by METRIC_1:def 13, TOPMETR: 12, TOPMETR:def 6;

        

         A12: I[01] is closed SubSpace of R^1 by Th2, TOPMETR: 20;

        then

         A13: A0 is closed by A4, TSEP_1: 12;

        

         A14: B0 is closed by A5, A12, TSEP_1: 12;

         0 in { w where w be Real : 0 <= w & w <= 1 };

        then

         A15: 0 in [. 0 , 1.] by RCOMP_1:def 1;

        now

          per cases by A1, A15, BORSUK_1: 40, XBOOLE_0:def 3;

            suppose

             A16: 0 in P;

            reconsider B00 = (B0 ` ) as Subset of R^1 ;

            set l = ( lower_bound Q);

            l in REAL by XREAL_0:def 1;

            then

            reconsider m = l as Point of RealSpace by METRIC_1:def 13;

            reconsider t = m as Point of R^1 by TOPMETR: 12, TOPMETR:def 6;

            set W = { w where w be Real : 0 <= w & w < l };

            

             A17: l in Q

            proof

              assume not l in Q;

              then

               A18: t in B00 by SUBSET_1: 29;

              B00 is open by A14, TOPS_1: 3;

              then

              consider s be Real such that

               A19: s > 0 and

               A20: ( Ball (m,s)) c= (B0 ` ) by A18, TOPMETR: 15, TOPMETR:def 6;

              consider r be Real such that

               A21: r in Q and

               A22: r < (l + s) by A8, A11, A19, SEQ_4:def 2;

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

              l <= r by A11, A21, SEQ_4:def 2;

              then (l - r) <= 0 by XREAL_1: 47;

              then

               A23: ( - s) < ( - (l - r)) by A19, XREAL_1: 24;

              reconsider rm = r as Point of RealSpace by METRIC_1:def 13;

              (r - l) < s by A22, XREAL_1: 19;

              then |.(r - l).| < s by A23, SEQ_2: 1;

              then (the distance of RealSpace . (rm,m)) < s by METRIC_1:def 12, METRIC_1:def 13;

              then ( dist (m,rm)) < s by METRIC_1:def 1;

              then rm in { q where q be Element of RealSpace : ( dist (m,q)) < s };

              then rm in ( Ball (m,s)) by METRIC_1: 17;

              hence contradiction by A20, A21, XBOOLE_0:def 5;

            end;

            then l in [. 0 , 1.] by BORSUK_1: 40;

            then l in { u where u be Real : 0 <= u & u <= 1 } by RCOMP_1:def 1;

            then

             A24: ex u0 be Real st u0 = l & 0 <= u0 & u0 <= 1;

            now

              let x be object;

              assume x in W;

              then

              consider w0 be Real such that

               A25: w0 = x and

               A26: 0 <= w0 and

               A27: w0 < l;

              w0 <= 1 by A24, A27, XXREAL_0: 2;

              then w0 in { u where u be Real : 0 <= u & u <= 1 } by A26;

              then w0 in (P \/ Q) by A1, BORSUK_1: 40, RCOMP_1:def 1;

              then w0 in P or w0 in Q by XBOOLE_0:def 3;

              hence x in P by A11, A25, A27, SEQ_4:def 2;

            end;

            then

             A28: W c= P;

            then

            reconsider D = W as Subset of R^1 by A9, METRIC_1:def 13, TOPMETR:def 6, XBOOLE_1: 1;

            

             A29: not 0 in Q by A6, A16, XBOOLE_0: 3;

            now

              let G be Subset of R^1 ;

              assume

               A30: G is open;

              assume t in G;

              then

              consider e be Real such that

               A31: e > 0 and

               A32: ( Ball (m,e)) c= G by A30, TOPMETR: 15, TOPMETR:def 6;

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

              reconsider e0 = ( max ( 0 ,(l - (e / 2)))) as Element of REAL by XREAL_0:def 1;

              reconsider e1 = e0 as Point of RealSpace by METRIC_1:def 13;

              

               A33: (e * (1 / 2)) < (e * 1) by A31, XREAL_1: 68;

              now

                per cases by XXREAL_0: 16;

                  suppose

                   A34: e0 = 0 ;

                  then l <= (e / 2) by XREAL_1: 50, XXREAL_0: 25;

                  then l < e by A33, XXREAL_0: 2;

                  hence |.(l - e0).| < e by A24, A34, ABSVALUE:def 1;

                end;

                  suppose e0 = (l - (e / 2));

                  hence |.(l - e0).| < e by A31, A33, ABSVALUE:def 1;

                end;

              end;

              then (the distance of RealSpace . (m,e1)) < e by METRIC_1:def 12, METRIC_1:def 13;

              then ( dist (m,e1)) < e by METRIC_1:def 1;

              then e1 in { z where z be Element of RealSpace : ( dist (m,z)) < e };

              then

               A35: e1 in ( Ball (m,e)) by METRIC_1: 17;

              e0 = 0 or e0 = (l - (e / 2)) by XXREAL_0: 16;

              then 0 <= e0 & e0 < l by A29, A17, A24, A31, XREAL_1: 44, XREAL_1: 139, XXREAL_0: 25;

              then e0 in W;

              hence D meets G by A32, A35, XBOOLE_0: 3;

            end;

            then

             A36: t in ( Cl D) by PRE_TOPC: 24;

            

             A37: ( Cl A0) = A0 by A13, PRE_TOPC: 22;

            ( Cl D) c= ( Cl A0) by A28, PRE_TOPC: 19;

            hence contradiction by A6, A17, A36, A37, XBOOLE_0: 3;

          end;

            suppose

             A38: 0 in Q;

            reconsider A00 = (A0 ` ) as Subset of R^1 ;

            set l = ( lower_bound P);

            l in REAL by XREAL_0:def 1;

            then

            reconsider m = l as Point of RealSpace by METRIC_1:def 13;

            reconsider t = m as Point of R^1 by TOPMETR: 12, TOPMETR:def 6;

            set W = { w where w be Real : 0 <= w & w < l };

            

             A39: l in P

            proof

              assume not l in P;

              then

               A40: t in A00 by SUBSET_1: 29;

              A00 is open by A13, TOPS_1: 3;

              then

              consider s be Real such that

               A41: s > 0 and

               A42: ( Ball (m,s)) c= (A0 ` ) by A40, TOPMETR: 15, TOPMETR:def 6;

              consider r be Real such that

               A43: r in P and

               A44: r < (l + s) by A7, A10, A41, SEQ_4:def 2;

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

              l <= r by A10, A43, SEQ_4:def 2;

              then (l - r) <= 0 by XREAL_1: 47;

              then

               A45: ( - s) < ( - (l - r)) by A41, XREAL_1: 24;

              reconsider rm = r as Point of RealSpace by METRIC_1:def 13;

              

               A46: ( real_dist . (r,l)) = ( dist (rm,m)) by METRIC_1:def 1, METRIC_1:def 13;

              (r - l) < s by A44, XREAL_1: 19;

              then |.(r - l).| < s by A45, SEQ_2: 1;

              then ( dist (rm,m)) < s by METRIC_1:def 12, A46;

              then rm in { q where q be Element of RealSpace : ( dist (m,q)) < s };

              then rm in ( Ball (m,s)) by METRIC_1: 17;

              hence contradiction by A42, A43, XBOOLE_0:def 5;

            end;

            then l in [. 0 , 1.] by BORSUK_1: 40;

            then l in { u where u be Real : 0 <= u & u <= 1 } by RCOMP_1:def 1;

            then

             A47: ex u0 be Real st u0 = l & 0 <= u0 & u0 <= 1;

            now

              let x be object;

              assume x in W;

              then

              consider w0 be Real such that

               A48: w0 = x and

               A49: 0 <= w0 and

               A50: w0 < l;

              w0 <= 1 by A47, A50, XXREAL_0: 2;

              then w0 in { u where u be Real : 0 <= u & u <= 1 } by A49;

              then w0 in (P \/ Q) by A1, BORSUK_1: 40, RCOMP_1:def 1;

              then w0 in P or w0 in Q by XBOOLE_0:def 3;

              hence x in Q by A10, A48, A50, SEQ_4:def 2;

            end;

            then

             A51: W c= Q;

            then

            reconsider D = W as Subset of R^1 by A9, METRIC_1:def 13, TOPMETR:def 6, XBOOLE_1: 1;

            

             A52: not 0 in P by A6, A38, XBOOLE_0: 3;

            now

              let G be Subset of R^1 ;

              assume

               A53: G is open;

              assume t in G;

              then

              consider e be Real such that

               A54: e > 0 and

               A55: ( Ball (m,e)) c= G by A53, TOPMETR: 15, TOPMETR:def 6;

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

              reconsider e0 = ( max ( 0 ,(l - (e / 2)))) as Element of REAL by XREAL_0:def 1;

              reconsider e1 = e0 as Point of RealSpace by METRIC_1:def 13;

              

               A56: (e * (1 / 2)) < (e * 1) by A54, XREAL_1: 68;

              

               A57: ( real_dist . (l,e0)) = ( dist (m,e1)) by METRIC_1:def 1, METRIC_1:def 13;

              now

                per cases by XXREAL_0: 16;

                  suppose

                   A58: e0 = 0 ;

                  then l <= (e / 2) by XREAL_1: 50, XXREAL_0: 25;

                  then l < e by A56, XXREAL_0: 2;

                  hence |.(l - e0).| < e by A47, A58, ABSVALUE:def 1;

                end;

                  suppose e0 = (l - (e / 2));

                  hence |.(l - e0).| < e by A54, A56, ABSVALUE:def 1;

                end;

              end;

              then ( dist (m,e1)) < e by METRIC_1:def 12, A57;

              then e1 in { z where z be Element of RealSpace : ( dist (m,z)) < e };

              then

               A59: e1 in ( Ball (m,e)) by METRIC_1: 17;

              e0 = 0 or e0 = (l - (e / 2)) by XXREAL_0: 16;

              then 0 <= e0 & e0 < l by A52, A39, A47, A54, XREAL_1: 44, XREAL_1: 139, XXREAL_0: 25;

              then e0 in W;

              hence D meets G by A55, A59, XBOOLE_0: 3;

            end;

            then

             A60: t in ( Cl D) by PRE_TOPC: 24;

            

             A61: ( Cl B0) = B0 by A14, PRE_TOPC: 22;

            ( Cl D) c= ( Cl B0) by A51, PRE_TOPC: 19;

            hence contradiction by A6, A39, A60, A61, XBOOLE_0: 3;

          end;

        end;

        hence contradiction;

      end;

      hence thesis by CONNSP_1: 10;

    end;

    theorem :: TREAL_1:20

    a <= b implies ( Closed-Interval-TSpace (a,b)) is connected

    proof

      assume

       A1: a <= b;

      now

        per cases by A1, XXREAL_0: 1;

          suppose a < b;

          then ( L[01] (( (#) (a,b)),((a,b) (#) ))) is being_homeomorphism by Th17;

          then

           A2: ( rng ( L[01] (( (#) (a,b)),((a,b) (#) )))) = ( [#] ( Closed-Interval-TSpace (a,b))) & ( L[01] (( (#) (a,b)),((a,b) (#) ))) is continuous by TOPS_2:def 5;

          set A = the carrier of ( Closed-Interval-TSpace ( 0 ,1));

          A = ( [#] ( Closed-Interval-TSpace ( 0 ,1))) & (( L[01] (( (#) (a,b)),((a,b) (#) ))) .: A) = ( rng ( L[01] (( (#) (a,b)),((a,b) (#) )))) by RELSET_1: 22;

          hence thesis by A2, Th19, CONNSP_1: 14, TOPMETR: 20;

        end;

          suppose

           A3: a = b;

          then [.a, b.] = {a} & a = ( (#) (a,b)) by Def1, XXREAL_1: 17;

          then ( [#] ( Closed-Interval-TSpace (a,b))) = {( (#) (a,b))} by A3, TOPMETR: 18;

          hence thesis by CONNSP_1: 27;

        end;

      end;

      hence thesis;

    end;

    theorem :: TREAL_1:21

    

     Th21: for f be continuous Function of I[01] , I[01] holds ex x be Point of I[01] st (f . x) = x

    proof

      let f be continuous Function of I[01] , I[01] ;

      reconsider F = f as Function of [. 0 , 1.], [. 0 , 1.] by BORSUK_1: 40;

      set A = { a where a be Real : a in [. 0 , 1.] & (F . a) in [. 0 , a.] }, B = { b where b be Real : b in [. 0 , 1.] & (F . b) in [.b, 1.] };

      A c= REAL

      proof

        let x be object;

        assume x in A;

        then ex a be Real st a = x & a in [. 0 , 1.] & (F . a) in [. 0 , a.];

        hence thesis;

      end;

      then

      reconsider A as Subset of REAL ;

      

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

      

       A2: A c= [. 0 , 1.]

      proof

        let x be object;

        assume

         A3: x in A;

        then

        reconsider x as Real;

        ex a0 be Real st a0 = x & a0 in [. 0 , 1.] & (F . a0) in [. 0 , a0.] by A3;

        hence thesis;

      end;

      B c= REAL

      proof

        let x be object;

        assume x in B;

        then ex b be Real st b = x & b in [. 0 , 1.] & (F . b) in [.b, 1.];

        hence thesis;

      end;

      then

      reconsider B as Subset of REAL ;

      

       A4: the carrier of ( Closed-Interval-MSpace ( 0 ,1)) = [. 0 , 1.] by TOPMETR: 10;

       0 in { w where w be Real : 0 <= w & w <= 1 };

      then

       A5: 0 in [. 0 , 1.] by RCOMP_1:def 1;

      

       A6: [. 0 , 1.] <> {} by XXREAL_1: 1;

      then [. 0 , 1.] = ( dom F) by FUNCT_2:def 1;

      then (F . 0 ) in ( rng F) by A5, FUNCT_1:def 3;

      then

       A7: 0 in B by A5;

      

       A8: [. 0 , 1.] = { q where q be Real : 0 <= q & q <= 1 } by RCOMP_1:def 1;

      

       A9: [. 0 , 1.] c= (A \/ B)

      proof

        let x be object;

        assume

         A10: x in [. 0 , 1.];

        then

        reconsider y = x as Real;

        ex p be Real st p = y & 0 <= p & p <= 1 by A8, A10;

        then

         A11: [. 0 , 1.] = ( [. 0 , y.] \/ [.y, 1.]) by XXREAL_1: 174;

         [. 0 , 1.] = ( dom F) by A6, FUNCT_2:def 1;

        then

         A12: (F . y) in ( rng F) by A10, FUNCT_1:def 3;

        now

          per cases by A11, A12, XBOOLE_0:def 3;

            suppose

             A13: (F . y) in [. 0 , y.];

            

             A14: A c= (A \/ B) by XBOOLE_1: 7;

            y in A by A10, A13;

            hence y in (A \/ B) by A14;

          end;

            suppose

             A15: (F . y) in [.y, 1.];

            

             A16: B c= (A \/ B) by XBOOLE_1: 7;

            y in B by A10, A15;

            hence y in (A \/ B) by A16;

          end;

        end;

        hence thesis;

      end;

      1 in { w where w be Real : 0 <= w & w <= 1 };

      then

       A17: 1 in [. 0 , 1.] by RCOMP_1:def 1;

      

       A18: B c= [. 0 , 1.]

      proof

        let x be object;

        assume

         A19: x in B;

        then

        reconsider x as Real;

        ex b0 be Real st b0 = x & b0 in [. 0 , 1.] & (F . b0) in [.b0, 1.] by A19;

        hence thesis;

      end;

      assume

       A20: for x be Point of I[01] holds (f . x) <> x;

      

       A21: (A /\ B) = {}

      proof

        set x = the Element of (A /\ B);

        assume

         A22: (A /\ B) <> {} ;

        then x in A by XBOOLE_0:def 4;

        then

         A23: ex z be Real st z = x & z in [. 0 , 1.] & (F . z) in [. 0 , z.];

        reconsider x as Real;

        x in B by A22, XBOOLE_0:def 4;

        then ex b0 be Real st b0 = x & b0 in [. 0 , 1.] & (F . b0) in [.b0, 1.];

        then

         A24: (F . x) in ( [. 0 , x.] /\ [.x, 1.]) by A23, XBOOLE_0:def 4;

        x in { q where q be Real : 0 <= q & q <= 1 } by A23, RCOMP_1:def 1;

        then ex u be Real st u = x & 0 <= u & u <= 1;

        then (F . x) in {x} by A24, XXREAL_1: 418;

        then (F . x) = x by TARSKI:def 1;

        hence contradiction by A20, A23, BORSUK_1: 40;

      end;

      then

       A25: A misses B by XBOOLE_0:def 7;

       [. 0 , 1.] = ( dom F) by A6, FUNCT_2:def 1;

      then (F . 1) in ( rng F) by A17, FUNCT_1:def 3;

      then

       A26: 1 in A by A17;

      ex P,Q be Subset of I[01] st ( [#] I[01] ) = (P \/ Q) & P <> ( {} I[01] ) & Q <> ( {} I[01] ) & P is closed & Q is closed & P misses Q

      proof

        reconsider P = A, Q = B as Subset of I[01] by A2, A18, BORSUK_1: 40;

        take P, Q;

        thus

         A27: ( [#] I[01] ) = (P \/ Q) by A9, BORSUK_1: 40, XBOOLE_0:def 10;

        thus P <> ( {} I[01] ) & Q <> ( {} I[01] ) by A26, A7;

        thus P is closed

        proof

          set z = the Element of (( Cl P) /\ Q);

          assume not P is closed;

          then

           A28: ( Cl P) <> P by PRE_TOPC: 22;

          

           A29: (( Cl P) /\ Q) <> {}

          proof

            assume (( Cl P) /\ Q) = {} ;

            then ( Cl P) misses Q by XBOOLE_0:def 7;

            then

             A30: ( Cl P) c= (Q ` ) by SUBSET_1: 23;

            P c= ( Cl P) & P = (Q ` ) by A25, A27, PRE_TOPC: 5, PRE_TOPC: 18;

            hence contradiction by A28, A30, XBOOLE_0:def 10;

          end;

          then

           A31: z in ( Cl P) by XBOOLE_0:def 4;

          

           A32: z in Q by A29, XBOOLE_0:def 4;

          reconsider z as Point of I[01] by A31;

          reconsider t0 = z as Real;

          

           A33: ex c be Real st c = t0 & c in [. 0 , 1.] & (F . c) in [.c, 1.] by A32;

          then

          reconsider s0 = (F . t0) as Real;

          t0 <= s0 by A33, XXREAL_1: 1;

          then

           A34: 0 <= (s0 - t0) by XREAL_1: 48;

          set r = ((s0 - t0) * (2 " ));

          reconsider m = z, n = (f . z) as Point of ( Closed-Interval-MSpace ( 0 ,1)) by BORSUK_1: 40, TOPMETR: 10;

          reconsider W = ( Ball (n,r)) as Subset of I[01] by BORSUK_1: 40, TOPMETR: 10;

          

           A35: W is open & f is_continuous_at z by A1, TMAP_1: 50, TOPMETR: 14, TOPMETR: 20;

          

           A36: (s0 - t0) <> 0 by A20;

          then

           A37: ( 0 / 2) < ((s0 - t0) / 2) by A34, XREAL_1: 74;

          then (f . z) in W by TBSP_1: 11;

          then

          consider V be Subset of I[01] such that

           A38: V is open & z in V and

           A39: (f .: V) c= W by A35, TMAP_1: 43;

          consider s be Real such that

           A40: s > 0 and

           A41: ( Ball (m,s)) c= V by A1, A38, TOPMETR: 15, TOPMETR: 20;

          reconsider s as Real;

          set r0 = ( min (s,r));

          reconsider W0 = ( Ball (m,r0)) as Subset of I[01] by BORSUK_1: 40, TOPMETR: 10;

          r0 > 0 by A37, A40, XXREAL_0: 15;

          then

           A42: z in W0 by TBSP_1: 11;

          set w = the Element of (P /\ W0);

          W0 is open by A1, TOPMETR: 14, TOPMETR: 20;

          then P meets W0 by A31, A42, PRE_TOPC: 24;

          then

           A43: (P /\ W0) <> ( {} I[01] ) by XBOOLE_0:def 7;

          then

           A44: w in P by XBOOLE_0:def 4;

          

           A45: w in W0 by A43, XBOOLE_0:def 4;

          then

          reconsider w as Point of ( Closed-Interval-MSpace ( 0 ,1));

          reconsider w1 = w as Point of I[01] by A44;

          reconsider d = w1 as Real;

          

           A46: d in A by A43, XBOOLE_0:def 4;

          ( Ball (m,r0)) = { q where q be Element of ( Closed-Interval-MSpace ( 0 ,1)) : ( dist (m,q)) < r0 } by METRIC_1: 17;

          then r0 <= r & ex p be Element of ( Closed-Interval-MSpace ( 0 ,1)) st p = w & ( dist (m,p)) < r0 by A45, XXREAL_0: 17;

          then ( dist (w,m)) < r by XXREAL_0: 2;

          then

           A47: |.(d - t0).| < r by HEINE: 1;

          (d - t0) <= |.(d - t0).| by ABSVALUE: 4;

          then (t0 + r) = (s0 - r) & (d - t0) < r by A47, XXREAL_0: 2;

          then

           A48: d < (s0 - r) by XREAL_1: 19;

          

           A49: r < ((s0 - t0) * 1) by A34, A36, XREAL_1: 68;

          

           A50: ( Ball (n,r)) c= [.t0, 1.]

          proof

            let x be object;

            assume

             A51: x in ( Ball (n,r));

            then

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

            x in [. 0 , 1.] by A4, A51;

            then

            reconsider t = x as Real;

            ( Ball (n,r)) = { q where q be Element of ( Closed-Interval-MSpace ( 0 ,1)) : ( dist (n,q)) < r } by METRIC_1: 17;

            then ex p be Element of ( Closed-Interval-MSpace ( 0 ,1)) st p = u & ( dist (n,p)) < r by A51;

            then |.(s0 - t).| < r by HEINE: 1;

            then

             A52: |.(s0 - t).| < (s0 - t0) by A49, XXREAL_0: 2;

            (s0 - t) <= |.(s0 - t).| by ABSVALUE: 4;

            then (s0 - t) < (s0 - t0) by A52, XXREAL_0: 2;

            then

             A53: t0 <= t by XREAL_1: 10;

            t <= 1 by A4, A51, XXREAL_1: 1;

            then t in { q where q be Real : t0 <= q & q <= 1 } by A53;

            hence thesis by RCOMP_1:def 1;

          end;

          

           A54: ( Ball (n,r)) c= [.d, 1.]

          proof

            let x be object;

            assume

             A55: x in ( Ball (n,r));

            then

            reconsider v = x as Point of ( Closed-Interval-MSpace ( 0 ,1));

            x in [. 0 , 1.] by A4, A55;

            then

            reconsider t = x as Real;

            ( Ball (n,r)) = { q where q be Element of ( Closed-Interval-MSpace ( 0 ,1)) : ( dist (n,q)) < r } by METRIC_1: 17;

            then ex p be Element of ( Closed-Interval-MSpace ( 0 ,1)) st p = v & ( dist (n,p)) < r by A55;

            then

             A56: |.(s0 - t).| < r by HEINE: 1;

             A57:

            now

              per cases ;

                suppose t <= s0;

                then 0 <= (s0 - t) by XREAL_1: 48;

                then (s0 - t) < r by A56, ABSVALUE:def 1;

                then s0 < (r + t) by XREAL_1: 19;

                then (s0 - r) < t by XREAL_1: 19;

                hence d < t by A48, XXREAL_0: 2;

              end;

                suppose

                 A58: s0 < t;

                (s0 - r) < s0 by A37, XREAL_1: 44;

                then d < s0 by A48, XXREAL_0: 2;

                hence d < t by A58, XXREAL_0: 2;

              end;

            end;

            t <= 1 by A50, A55, XXREAL_1: 1;

            then t in { w0 where w0 be Real : d <= w0 & w0 <= 1 } by A57;

            hence thesis by RCOMP_1:def 1;

          end;

          ( Ball (m,r0)) c= ( Ball (m,s)) by PCOMPS_1: 1, XXREAL_0: 17;

          then W0 c= V by A41;

          then (f . w1) in (f .: V) by A45, FUNCT_2: 35;

          then (f . w1) in W by A39;

          then d in B by A54, BORSUK_1: 40;

          hence contradiction by A25, A46, XBOOLE_0: 3;

        end;

        thus Q is closed

        proof

          set z = the Element of (( Cl Q) /\ P);

          assume not Q is closed;

          then

           A59: ( Cl Q) <> Q by PRE_TOPC: 22;

          

           A60: (( Cl Q) /\ P) <> {}

          proof

            assume (( Cl Q) /\ P) = {} ;

            then ( Cl Q) misses P by XBOOLE_0:def 7;

            then

             A61: ( Cl Q) c= (P ` ) by SUBSET_1: 23;

            Q c= ( Cl Q) & Q = (P ` ) by A25, A27, PRE_TOPC: 5, PRE_TOPC: 18;

            hence contradiction by A59, A61, XBOOLE_0:def 10;

          end;

          then

           A62: z in ( Cl Q) by XBOOLE_0:def 4;

          

           A63: z in P by A60, XBOOLE_0:def 4;

          reconsider z as Point of I[01] by A62;

          reconsider t0 = z as Real;

          

           A64: ex c be Real st c = t0 & c in [. 0 , 1.] & (F . c) in [. 0 , c.] by A63;

          then

          reconsider s0 = (F . t0) as Real;

          s0 <= t0 by A64, XXREAL_1: 1;

          then

           A65: 0 <= (t0 - s0) by XREAL_1: 48;

          set r = ((t0 - s0) * (2 " ));

          reconsider m = z, n = (f . z) as Point of ( Closed-Interval-MSpace ( 0 ,1)) by BORSUK_1: 40, TOPMETR: 10;

          reconsider W = ( Ball (n,r)) as Subset of I[01] by BORSUK_1: 40, TOPMETR: 10;

          

           A66: W is open & f is_continuous_at z by A1, TMAP_1: 50, TOPMETR: 14, TOPMETR: 20;

          

           A67: (t0 - s0) <> 0 by A20;

          then

           A68: ( 0 / 2) < ((t0 - s0) / 2) by A65, XREAL_1: 74;

          then (f . z) in W by TBSP_1: 11;

          then

          consider V be Subset of I[01] such that

           A69: V is open & z in V and

           A70: (f .: V) c= W by A66, TMAP_1: 43;

          consider s be Real such that

           A71: s > 0 and

           A72: ( Ball (m,s)) c= V by A1, A69, TOPMETR: 15, TOPMETR: 20;

          reconsider s as Real;

          set r0 = ( min (s,r));

          reconsider W0 = ( Ball (m,r0)) as Subset of I[01] by BORSUK_1: 40, TOPMETR: 10;

          r0 > 0 by A68, A71, XXREAL_0: 15;

          then

           A73: z in W0 by TBSP_1: 11;

          set w = the Element of (Q /\ W0);

          W0 is open by A1, TOPMETR: 14, TOPMETR: 20;

          then Q meets W0 by A62, A73, PRE_TOPC: 24;

          then

           A74: (Q /\ W0) <> ( {} I[01] ) by XBOOLE_0:def 7;

          then

           A75: w in Q by XBOOLE_0:def 4;

          

           A76: w in W0 by A74, XBOOLE_0:def 4;

          then

          reconsider w as Point of ( Closed-Interval-MSpace ( 0 ,1));

          reconsider w1 = w as Point of I[01] by A75;

          reconsider d = w1 as Real;

          

           A77: d in B by A74, XBOOLE_0:def 4;

          ( Ball (m,r0)) = { q where q be Element of ( Closed-Interval-MSpace ( 0 ,1)) : ( dist (m,q)) < r0 } by METRIC_1: 17;

          then r0 <= r & ex p be Element of ( Closed-Interval-MSpace ( 0 ,1)) st p = w & ( dist (m,p)) < r0 by A76, XXREAL_0: 17;

          then ( dist (m,w)) < r by XXREAL_0: 2;

          then

           A78: |.(t0 - d).| < r by HEINE: 1;

          (t0 - d) <= |.(t0 - d).| by ABSVALUE: 4;

          then (t0 + ( - d)) < r by A78, XXREAL_0: 2;

          then t0 < (r - ( - d)) by XREAL_1: 20;

          then (s0 + r) = (t0 - r) & t0 < (r + ( - ( - d)));

          then

           A79: (s0 + r) < d by XREAL_1: 19;

          

           A80: r < ((t0 - s0) * 1) by A65, A67, XREAL_1: 68;

          

           A81: ( Ball (n,r)) c= [. 0 , t0.]

          proof

            let x be object;

            assume

             A82: x in ( Ball (n,r));

            then

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

            x in [. 0 , 1.] by A4, A82;

            then

            reconsider t = x as Real;

            ( Ball (n,r)) = { q where q be Element of ( Closed-Interval-MSpace ( 0 ,1)) : ( dist (n,q)) < r } by METRIC_1: 17;

            then ex p be Element of ( Closed-Interval-MSpace ( 0 ,1)) st p = u & ( dist (n,p)) < r by A82;

            then |.(t - s0).| < r by HEINE: 1;

            then

             A83: |.(t - s0).| < (t0 - s0) by A80, XXREAL_0: 2;

            (t - s0) <= |.(t - s0).| by ABSVALUE: 4;

            then (t - s0) < (t0 - s0) by A83, XXREAL_0: 2;

            then

             A84: t <= t0 by XREAL_1: 9;

             0 <= t by A4, A82, XXREAL_1: 1;

            then t in { q where q be Real : 0 <= q & q <= t0 } by A84;

            hence thesis by RCOMP_1:def 1;

          end;

          

           A85: ( Ball (n,r)) c= [. 0 , d.]

          proof

            let x be object;

            assume

             A86: x in ( Ball (n,r));

            then

            reconsider v = x as Point of ( Closed-Interval-MSpace ( 0 ,1));

            x in [. 0 , 1.] by A4, A86;

            then

            reconsider t = x as Real;

            ( Ball (n,r)) = { q where q be Element of ( Closed-Interval-MSpace ( 0 ,1)) : ( dist (n,q)) < r } by METRIC_1: 17;

            then ex p be Element of ( Closed-Interval-MSpace ( 0 ,1)) st p = v & ( dist (n,p)) < r by A86;

            then

             A87: |.(t - s0).| < r by HEINE: 1;

             A88:

            now

              per cases ;

                suppose s0 <= t;

                then 0 <= (t - s0) by XREAL_1: 48;

                then (t - s0) < r by A87, ABSVALUE:def 1;

                then t < (s0 + r) by XREAL_1: 19;

                hence t < d by A79, XXREAL_0: 2;

              end;

                suppose

                 A89: t < s0;

                s0 < (s0 + r) by A68, XREAL_1: 29;

                then s0 < d by A79, XXREAL_0: 2;

                hence t < d by A89, XXREAL_0: 2;

              end;

            end;

             0 <= t by A81, A86, XXREAL_1: 1;

            then t in { w0 where w0 be Real : 0 <= w0 & w0 <= d } by A88;

            hence thesis by RCOMP_1:def 1;

          end;

          ( Ball (m,r0)) c= ( Ball (m,s)) by PCOMPS_1: 1, XXREAL_0: 17;

          then W0 c= V by A72;

          then (f . w1) in (f .: V) by A76, FUNCT_2: 35;

          then (f . w1) in W by A70;

          then d in A by A85, BORSUK_1: 40;

          hence contradiction by A25, A77, XBOOLE_0: 3;

        end;

        thus thesis by A21, XBOOLE_0:def 7;

      end;

      hence contradiction by Th19, CONNSP_1: 10;

    end;

    theorem :: TREAL_1:22

    

     Th22: a <= b implies for f be continuous Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (a,b)) holds ex x be Point of ( Closed-Interval-TSpace (a,b)) st (f . x) = x

    proof

      assume

       A1: a <= b;

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

      now

        per cases by A1, XXREAL_0: 1;

          suppose

           A2: a < b;

          set L = ( L[01] (( (#) (a,b)),((a,b) (#) ))), P = ( P[01] (a,b,( (#) ( 0 ,1)),(( 0 ,1) (#) )));

          

           A3: P is continuous Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace ( 0 ,1)) by A2, Th12;

          set g = ((P * f) * L);

          

           A4: ( id ( Closed-Interval-TSpace (a,b))) = (L * P) by A2, Th15;

          

          then

           A5: f = ((L * P) * f) by FUNCT_2: 17

          .= (L * (P * f)) by RELAT_1: 36

          .= (L * ((P * f) * (L * P))) by A4, FUNCT_2: 17

          .= (L * (g * P)) by RELAT_1: 36

          .= ((L * g) * P) by RELAT_1: 36;

          L is continuous Function of ( Closed-Interval-TSpace ( 0 ,1)), ( Closed-Interval-TSpace (a,b)) by A1, Th8;

          then

          consider y be Point of ( Closed-Interval-TSpace ( 0 ,1)) such that

           A6: (g . y) = y by A3, Th21, TOPMETR: 20;

          

           A7: ( id ( Closed-Interval-TSpace ( 0 ,1))) = (P * L) by A2, Th15;

          now

            take x = (L . y);

            

            thus (f . x) = ((((L * g) * P) * L) . y) by A5, FUNCT_2: 15

            .= (((L * g) * ( id ( Closed-Interval-TSpace ( 0 ,1)))) . y) by A7, RELAT_1: 36

            .= ((L * g) . y) by FUNCT_2: 17

            .= x by A6, FUNCT_2: 15;

          end;

          hence thesis;

        end;

          suppose

           A8: a = b;

          then [.a, b.] = {a} & a = ( (#) (a,b)) by Def1, XXREAL_1: 17;

          then

           A9: the carrier of ( Closed-Interval-TSpace (a,b)) = {( (#) (a,b))} by A8, TOPMETR: 18;

          now

            take x = ( (#) (a,b));

            thus (f . x) = x by A9, TARSKI:def 1;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: TREAL_1:23

    

     Th23: for X,Y be non empty SubSpace of R^1 , f be continuous Function of X, Y holds (ex a,b be Real st a <= b & [.a, b.] c= the carrier of X & [.a, b.] c= the carrier of Y & (f .: [.a, b.]) c= [.a, b.]) implies ex x be Point of X st (f . x) = x

    proof

      let X,Y be non empty SubSpace of R^1 , f be continuous Function of X, Y;

      given a,b be Real such that

       A1: a <= b and

       A2: [.a, b.] c= the carrier of X and

       A3: [.a, b.] c= the carrier of Y and

       A4: (f .: [.a, b.]) c= [.a, b.];

      reconsider A = [.a, b.] as non empty Subset of X by A1, A2, XXREAL_1: 1;

      

       A5: ( dom (f | A)) = (( dom f) /\ A) by RELAT_1: 61;

      A = (the carrier of X /\ A) & ( dom f) = the carrier of X by FUNCT_2:def 1, XBOOLE_1: 28;

      then

       A6: ( dom (f | A)) = the carrier of ( Closed-Interval-TSpace (a,b)) by A1, A5, TOPMETR: 18;

      

       A7: A = the carrier of ( Closed-Interval-TSpace (a,b)) by A1, TOPMETR: 18;

      then

      reconsider Z = ( Closed-Interval-TSpace (a,b)) as SubSpace of X by TSEP_1: 4;

      ( rng (f | A)) c= the carrier of ( Closed-Interval-TSpace (a,b)) by A4, A7, RELAT_1: 115;

      then

      reconsider g = (f | A) as Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (a,b)) by A6, FUNCT_2:def 1, RELSET_1: 4;

      

       A8: Z is SubSpace of Y by A3, A7, TSEP_1: 4;

      for s be Point of ( Closed-Interval-TSpace (a,b)) holds g is_continuous_at s

      proof

        let s be Point of ( Closed-Interval-TSpace (a,b));

        reconsider w = s as Point of X by A7, TARSKI:def 3;

        for G be Subset of ( Closed-Interval-TSpace (a,b)) st G is open & (g . s) in G holds ex H be Subset of Z st H is open & s in H & (g .: H) c= G

        proof

          let G be Subset of ( Closed-Interval-TSpace (a,b));

          

           A9: f is_continuous_at w by TMAP_1: 44;

          assume G is open;

          then

          consider G0 be Subset of Y such that

           A10: G0 is open and

           A11: (G0 /\ ( [#] ( Closed-Interval-TSpace (a,b)))) = G by A8, TOPS_2: 24;

          assume (g . s) in G;

          then (f . w) in G by A7, FUNCT_1: 49;

          then (f . w) in G0 by A11, XBOOLE_0:def 4;

          then

          consider H0 be Subset of X such that

           A12: H0 is open and

           A13: w in H0 and

           A14: (f .: H0) c= G0 by A10, A9, TMAP_1: 43;

          now

            reconsider H = (H0 /\ ( [#] ( Closed-Interval-TSpace (a,b)))) as Subset of Z;

            take H;

            thus H is open by A12, TOPS_2: 24;

            thus s in H by A13, XBOOLE_0:def 4;

            thus (g .: H) c= G

            proof

              let t be object;

              assume t in (g .: H);

              then

              consider r be object such that r in ( dom g) and

               A15: r in H and

               A16: t = (g . r) by FUNCT_1:def 6;

              

               A17: r in the carrier of Z by A15;

              reconsider r as Point of ( Closed-Interval-TSpace (a,b)) by A15;

              r in ( dom g) by A17, FUNCT_2:def 1;

              then

               A18: t in (g .: the carrier of Z) by A16, FUNCT_1:def 6;

              reconsider p = r as Point of X by A7, TARSKI:def 3;

              p in ( [#] X);

              then

               A19: p in ( dom f) by FUNCT_2:def 1;

              t = (f . p) & p in H0 by A7, A15, A16, FUNCT_1: 49, XBOOLE_0:def 4;

              then t in (f .: H0) by A19, FUNCT_1:def 6;

              hence thesis by A11, A14, A18, XBOOLE_0:def 4;

            end;

          end;

          hence thesis;

        end;

        hence thesis by TMAP_1: 43;

      end;

      then

      reconsider h = g as continuous Function of ( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (a,b)) by TMAP_1: 44;

      now

        consider y be Point of ( Closed-Interval-TSpace (a,b)) such that

         A20: (h . y) = y by A1, Th22;

        reconsider x = y as Point of X by A7, TARSKI:def 3;

        take x;

        thus (f . x) = x by A7, A20, FUNCT_1: 49;

      end;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: TREAL_1:24

    for X,Y be non empty SubSpace of R^1 , f be continuous Function of X, Y holds (ex a,b be Real st a <= b & [.a, b.] c= the carrier of X & (f .: [.a, b.]) c= [.a, b.]) implies ex x be Point of X st (f . x) = x

    proof

      let X,Y be non empty SubSpace of R^1 , f be continuous Function of X, Y;

      given a,b be Real such that

       A1: a <= b and

       A2: [.a, b.] c= the carrier of X and

       A3: (f .: [.a, b.]) c= [.a, b.];

      set g = ((Y incl R^1 ) * f);

      the carrier of Y c= the carrier of R^1 by BORSUK_1: 1;

      then

      reconsider B = (f .: [.a, b.]) as Subset of R^1 by XBOOLE_1: 1;

      (g .: [.a, b.]) = ((Y incl R^1 ) .: (f .: [.a, b.])) by RELAT_1: 126;

      then (g .: [.a, b.]) = ((( id R^1 ) | Y) .: B) by TMAP_1:def 6;

      then (g .: [.a, b.]) = (( id R^1 ) .: B) by TMAP_1: 55;

      then

       A4: (g .: [.a, b.]) c= [.a, b.] by A3, FUNCT_1: 92;

      

       A5: (Y incl R^1 ) is continuous Function of Y, R^1 & R^1 is SubSpace of R^1 by TMAP_1: 87, TSEP_1: 2;

      the carrier of X c= the carrier of R^1 by BORSUK_1: 1;

      then

       A6: [.a, b.] c= the carrier of R^1 by A2;

      now

        consider x be Point of X such that

         A7: (g . x) = x by A1, A2, A5, A6, A4, Th23;

        the carrier of Y c= the carrier of R^1 by BORSUK_1: 1;

        then

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

        take x;

        

        thus (f . x) = ((Y incl R^1 ) . y) by TMAP_1: 84

        .= x by A7, FUNCT_2: 15;

      end;

      hence thesis;

    end;