topreal5.miz



    begin

    reserve x for set;

    reserve a,b,d,ra,rb,r0,s1,s2 for Real;

    reserve r,s,r1,r2,r3,rc for Real;

    reserve p,q,q1,q2 for Point of ( TOP-REAL 2);

    reserve X,Y,Z for non empty TopSpace;

    

     Lm1: for f be continuous Function of X, Y, g be continuous Function of Y, Z holds (g * f) is continuous Function of X, Z;

    theorem :: TOPREAL5:1

    

     Th1: for A,B1,B2 be Subset of X st B1 is open & B2 is open & B1 meets A & B2 meets A & A c= (B1 \/ B2) & B1 misses B2 holds not A is connected

    proof

      let A,B1,B2 be Subset of X;

      assume that

       A1: B1 is open & B2 is open & B1 meets A and

       A2: B2 meets A and

       A3: A c= (B1 \/ B2) and

       A4: B1 misses B2;

      reconsider C1 = (B1 /\ A), C2 = (B2 /\ A) as Subset of X;

      

       A5: A = ((B1 \/ B2) /\ A) by A3, XBOOLE_1: 28

      .= (C1 \/ C2) by XBOOLE_1: 23;

      

       A6: C2 <> {} by A2, XBOOLE_0:def 7;

      

       A7: A is connected iff for P,Q be Subset of X st A = (P \/ Q) & (P,Q) are_separated holds P = ( {} X) or Q = ( {} X) by CONNSP_1: 15;

      

       A8: C1 c= B1 & C2 c= B2 by XBOOLE_1: 17;

      (B1,B2) are_separated & C1 <> {} by A1, A4, TSEP_1: 37, XBOOLE_0:def 7;

      hence thesis by A7, A5, A8, A6, CONNSP_1: 7;

    end;

    theorem :: TOPREAL5:2

    

     Th2: for ra, rb st ra <= rb holds ( [#] ( Closed-Interval-TSpace (ra,rb))) is connected

    proof

      let ra, rb;

      assume ra <= rb;

      then ( Closed-Interval-TSpace (ra,rb)) is connected by TREAL_1: 20;

      hence thesis by CONNSP_1: 27;

    end;

    theorem :: TOPREAL5:3

    

     Th3: for A be Subset of R^1 , a st not a in A & ex b, d st b in A & d in A & b < a & a < d holds not A is connected

    proof

      let A be Subset of R^1 , a;

      assume that

       A1: not a in A and

       A2: ex b, d st b in A & d in A & b < a & a < d;

      consider b, d such that

       A3: b in A and

       A4: d in A and

       A5: b < a and

       A6: a < d by A2;

      set B2 = { s : s > a };

      set B1 = { r : r < a };

      

       A7: A c= (B1 \/ B2)

      proof

        let x be object;

        assume

         A8: x in A;

        then

        reconsider r = x as Real;

        r < a or a < r by A1, A8, XXREAL_0: 1;

        then r in B1 or r in B2;

        hence thesis by XBOOLE_0:def 3;

      end;

      B2 c= REAL

      proof

        let x be object;

        assume x in B2;

        then

        consider r such that

         A9: r = x and r > a;

        r in REAL by XREAL_0:def 1;

        hence thesis by A9;

      end;

      then

      reconsider C2 = B2 as Subset of R^1 by METRIC_1:def 13, TOPMETR: 12, TOPMETR:def 6;

      B1 c= REAL

      proof

        let x be object;

        assume x in B1;

        then

        consider r such that

         A10: r = x and r < a;

        r in REAL by XREAL_0:def 1;

        hence thesis by A10;

      end;

      then

      reconsider C1 = B1 as Subset of R^1 by METRIC_1:def 13, TOPMETR: 12, TOPMETR:def 6;

       A11:

      now

        assume B1 meets B2;

        then

        consider x be object such that

         A12: x in (B1 /\ B2) by XBOOLE_0: 4;

        x in B2 by A12, XBOOLE_0:def 4;

        then

         A13: ex r2 st r2 = x & r2 > a;

        x in B1 by A12, XBOOLE_0:def 4;

        then ex r1 st r1 = x & r1 < a;

        hence contradiction by A13;

      end;

      reconsider r1 = d as Element of REAL by XREAL_0:def 1;

      r1 in B2 by A6;

      then d in (B2 /\ A) by A4, XBOOLE_0:def 4;

      then

       A14: B2 meets A by XBOOLE_0: 4;

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

      r in B1 by A5;

      then b in (B1 /\ A) by A3, XBOOLE_0:def 4;

      then

       A15: B1 meets A by XBOOLE_0: 4;

      C1 is open & C2 is open by JORDAN2B: 24, JORDAN2B: 25;

      hence thesis by A11, A15, A14, A7, Th1;

    end;

    ::$Notion-Name

    theorem :: TOPREAL5:4

    for X be non empty TopSpace, xa,xb be Point of X, a,b,d be Real, f be continuous Function of X, R^1 st X is connected & (f . xa) = a & (f . xb) = b & a <= d & d <= b holds ex xc be Point of X st (f . xc) = d

    proof

      let X be non empty TopSpace, xa,xb be Point of X, a,b,d be Real, f be continuous Function of X, R^1 ;

      assume that

       A1: X is connected and

       A2: (f . xa) = a & (f . xb) = b and

       A3: a <= d & d <= b;

      now

        assume ( not a = d) & not d = b;

        then

         A4: a < d & d < b by A3, XXREAL_0: 1;

        now

          assume

           A5: not ex rc be Point of X st (f . rc) = d;

           A6:

          now

            assume d in (f .: ( [#] X));

            then ex x be object st x in the carrier of X & x in ( [#] X) & d = (f . x) by FUNCT_2: 64;

            hence contradiction by A5;

          end;

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

          then

           A7: a in (f .: ( [#] X)) & b in (f .: ( [#] X)) by A2, FUNCT_1:def 6;

          ( [#] X) is connected by A1, CONNSP_1: 27;

          hence contradiction by A4, A6, A7, Th3, TOPS_2: 61;

        end;

        hence thesis;

      end;

      hence thesis by A2;

    end;

    theorem :: TOPREAL5:5

    for X be non empty TopSpace, xa,xb be Point of X, B be Subset of X, a,b,d be Real, f be continuous Function of X, R^1 st B is connected & (f . xa) = a & (f . xb) = b & a <= d & d <= b & xa in B & xb in B holds ex xc be Point of X st xc in B & (f . xc) = d

    proof

      let X be non empty TopSpace, xa,xb be Point of X, B be Subset of X, a,b,d be Real, f be continuous Function of X, R^1 ;

      assume that

       A1: B is connected and

       A2: (f . xa) = a & (f . xb) = b and

       A3: a <= d & d <= b and

       A4: xa in B & xb in B;

      now

        assume ( not a = d) & not d = b;

        then

         A5: a < d & d < b by A3, XXREAL_0: 1;

        now

          assume

           A6: not ex rc be Point of X st rc in B & (f . rc) = d;

           A7:

          now

            assume d in (f .: B);

            then ex x be object st x in the carrier of X & x in B & d = (f . x) by FUNCT_2: 64;

            hence contradiction by A6;

          end;

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

          then a in (f .: B) & b in (f .: B) by A2, A4, FUNCT_1:def 6;

          hence contradiction by A1, A5, A7, Th3, TOPS_2: 61;

        end;

        hence thesis;

      end;

      hence thesis by A2, A4;

    end;

    theorem :: TOPREAL5:6

    

     Th6: for ra, rb, a, b st ra < rb holds for f be continuous Function of ( Closed-Interval-TSpace (ra,rb)), R^1 , d st (f . ra) = a & (f . rb) = b & a < d & d < b holds ex rc st (f . rc) = d & ra < rc & rc < rb

    proof

      let ra, rb, a, b;

      assume

       A1: ra < rb;

      let f be continuous Function of ( Closed-Interval-TSpace (ra,rb)), R^1 , d;

      assume that

       A2: (f . ra) = a and

       A3: (f . rb) = b and

       A4: a < d and

       A5: d < b;

      now

        reconsider C = (f .: ( [#] ( Closed-Interval-TSpace (ra,rb)))) as Subset of R^1 ;

        

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

        

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

        then rb in ( [#] ( Closed-Interval-TSpace (ra,rb))) by A1, XXREAL_1: 1;

        then

         A8: b in (f .: ( [#] ( Closed-Interval-TSpace (ra,rb)))) by A3, A6, FUNCT_1:def 6;

        assume

         A9: not ex rc st (f . rc) = d & ra < rc & rc < rb;

         A10:

        now

          assume d in (f .: ( [#] ( Closed-Interval-TSpace (ra,rb))));

          then

          consider x be object such that

           A11: x in the carrier of ( Closed-Interval-TSpace (ra,rb)) and x in ( [#] ( Closed-Interval-TSpace (ra,rb))) and

           A12: d = (f . x) by FUNCT_2: 64;

          reconsider r = x as Real by A11;

          r <= rb by A7, A11, XXREAL_1: 1;

          then

           A13: r < rb by A3, A5, A12, XXREAL_0: 1;

          ra <= r by A7, A11, XXREAL_1: 1;

          then ra < r by A2, A4, A12, XXREAL_0: 1;

          hence contradiction by A9, A12, A13;

        end;

        ra in ( [#] ( Closed-Interval-TSpace (ra,rb))) by A1, A7, XXREAL_1: 1;

        then a in (f .: ( [#] ( Closed-Interval-TSpace (ra,rb)))) by A2, A6, FUNCT_1:def 6;

        then not C is connected by A4, A5, A10, A8, Th3;

        hence contradiction by A1, Th2, TOPS_2: 61;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL5:7

    

     Th7: for ra, rb, a, b st ra < rb holds for f be continuous Function of ( Closed-Interval-TSpace (ra,rb)), R^1 , d st (f . ra) = a & (f . rb) = b & a > d & d > b holds ex rc st (f . rc) = d & ra < rc & rc < rb

    proof

      let ra, rb, a, b;

      assume

       A1: ra < rb;

      then

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

      let f be continuous Function of ( Closed-Interval-TSpace (ra,rb)), R^1 , d;

      assume that

       A3: (f . ra) = a and

       A4: (f . rb) = b and

       A5: a > d and

       A6: d > b;

      

       A7: ( dom f) = the carrier of ( Closed-Interval-TSpace (ra,rb)) by FUNCT_2:def 1;

      

       A8: ( [#] ( Closed-Interval-TSpace (ra,rb))) is connected by A1, Th2;

      now

        assume

         A9: for rc st ra < rc & rc < rb holds (f . rc) <> d;

         A10:

        now

          assume d in (f .: ( [#] ( Closed-Interval-TSpace (ra,rb))));

          then

          consider x be object such that

           A11: x in ( dom f) and x in ( [#] ( Closed-Interval-TSpace (ra,rb))) and

           A12: d = (f . x) by FUNCT_1:def 6;

          x in [.ra, rb.] by A2, A11;

          then

          reconsider r = x as Real;

          r <= rb by A2, A11, XXREAL_1: 1;

          then

           A13: rb > r by A4, A6, A12, XXREAL_0: 1;

          ra <= r by A2, A11, XXREAL_1: 1;

          then ra < r by A3, A5, A12, XXREAL_0: 1;

          hence contradiction by A9, A12, A13;

        end;

        rb in [.ra, rb.] by A1, XXREAL_1: 1;

        then

         A14: b in (f .: ( [#] ( Closed-Interval-TSpace (ra,rb)))) by A4, A2, A7, FUNCT_1:def 6;

        ra in [.ra, rb.] by A1, XXREAL_1: 1;

        then a in (f .: ( [#] ( Closed-Interval-TSpace (ra,rb)))) by A3, A2, A7, FUNCT_1:def 6;

        hence contradiction by A5, A6, A8, A10, A14, Th3, TOPS_2: 61;

      end;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: TOPREAL5:8

    for ra, rb holds for g be continuous Function of ( Closed-Interval-TSpace (ra,rb)), R^1 , s1, s2 st ra < rb & (s1 * s2) < 0 & s1 = (g . ra) & s2 = (g . rb) holds ex r1 st (g . r1) = 0 & ra < r1 & r1 < rb

    proof

      let ra, rb;

      let g be continuous Function of ( Closed-Interval-TSpace (ra,rb)), R^1 , s1, s2;

      assume that

       A1: ra < rb and

       A2: (s1 * s2) < 0 ;

      s1 > 0 & s2 < 0 or s1 < 0 & s2 > 0 by A2, XREAL_1: 133;

      hence thesis by A1, Th6, Th7;

    end;

    theorem :: TOPREAL5:9

    

     Th9: for g be Function of I[01] , R^1 , s1, s2 st g is continuous & (g . 0 ) <> (g . 1) & s1 = (g . 0 ) & s2 = (g . 1) holds ex r1 st 0 < r1 & r1 < 1 & (g . r1) = ((s1 + s2) / 2)

    proof

      let g be Function of I[01] , R^1 , s1, s2;

      assume that

       A1: g is continuous and

       A2: (g . 0 ) <> (g . 1) and

       A3: s1 = (g . 0 ) & s2 = (g . 1);

      now

        per cases by A2, A3, XXREAL_0: 1;

          case s1 < s2;

          then s1 < ((s1 + s2) / 2) & ((s1 + s2) / 2) < s2 by XREAL_1: 226;

          hence ex rc st (g . rc) = ((s1 + s2) / 2) & 0 < rc & rc < 1 by A1, A3, Th6, TOPMETR: 20;

        end;

          case s2 < s1;

          then s2 < ((s1 + s2) / 2) & ((s1 + s2) / 2) < s1 by XREAL_1: 226;

          hence ex rc st (g . rc) = ((s1 + s2) / 2) & 0 < rc & rc < 1 by A1, A3, Th7, TOPMETR: 20;

        end;

      end;

      hence thesis;

    end;

    begin

    theorem :: TOPREAL5:10

    

     Th10: for f be Function of ( TOP-REAL 2), R^1 st f = proj1 holds f is continuous

    proof

      let f be Function of ( TOP-REAL 2), R^1 ;

      assume f = proj1 ;

      then 1 in ( Seg 2) & for p be Element of ( TOP-REAL 2) holds (f . p) = (p /. 1) by FINSEQ_1: 1, JORDAN2B: 30;

      hence thesis by JORDAN2B: 18;

    end;

    theorem :: TOPREAL5:11

    

     Th11: for f be Function of ( TOP-REAL 2), R^1 st f = proj2 holds f is continuous

    proof

      let f be Function of ( TOP-REAL 2), R^1 ;

      assume f = proj2 ;

      then 2 in ( Seg 2) & for p be Element of ( TOP-REAL 2) holds (f . p) = (p /. 2) by FINSEQ_1: 1, JORDAN2B: 30;

      hence thesis by JORDAN2B: 18;

    end;

    theorem :: TOPREAL5:12

    

     Th12: for P be non empty Subset of ( TOP-REAL 2), f be Function of I[01] , (( TOP-REAL 2) | P) st f is continuous holds ex g be Function of I[01] , R^1 st g is continuous & for r, q st r in the carrier of I[01] & q = (f . r) holds (q `1 ) = (g . r)

    proof

      reconsider rj = proj1 as Function of ( TOP-REAL 2), R^1 by TOPMETR: 17;

      let P be non empty Subset of ( TOP-REAL 2), f be Function of I[01] , (( TOP-REAL 2) | P);

      assume

       A1: f is continuous;

      reconsider f1 = f as Function;

      set h = (( proj1 | P) * f);

      

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

      then

       A3: ( rng f1) c= P by RELAT_1:def 19;

      rj is continuous Function of ( TOP-REAL 2), R^1 by Th10;

      then (rj | (( TOP-REAL 2) | P)) is continuous Function of (( TOP-REAL 2) | P), R^1 ;

      then (rj | P) is continuous Function of (( TOP-REAL 2) | P), R^1 by A2, TMAP_1:def 3;

      then

      reconsider h2 = h as continuous Function of I[01] , R^1 by A1, Lm1;

      take h2;

      thus h2 is continuous;

      let r be Real, q be Point of ( TOP-REAL 2);

      assume that

       A4: r in the carrier of I[01] and

       A5: q = (f . r);

      

       A6: ( dom proj1 ) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

      

       A7: r in ( dom f1) by A4, FUNCT_2:def 1;

      then (f1 . r) in ( rng f1) by FUNCT_1:def 3;

      then

       A8: q in (( dom proj1 ) /\ P) by A5, A3, A6, XBOOLE_0:def 4;

      

      thus (h2 . r) = (( proj1 | P) . q) by A5, A7, FUNCT_1: 13

      .= ( proj1 . q) by A8, FUNCT_1: 48

      .= (q `1 ) by PSCOMP_1:def 5;

    end;

    theorem :: TOPREAL5:13

    

     Th13: for P be non empty Subset of ( TOP-REAL 2), f be Function of I[01] , (( TOP-REAL 2) | P) st f is continuous holds ex g be Function of I[01] , R^1 st g is continuous & for r, q st r in the carrier of I[01] & q = (f . r) holds (q `2 ) = (g . r)

    proof

      reconsider rj = proj2 as Function of ( TOP-REAL 2), R^1 by TOPMETR: 17;

      let P be non empty Subset of ( TOP-REAL 2), f be Function of I[01] , (( TOP-REAL 2) | P);

      assume

       A1: f is continuous;

      reconsider f1 = f as Function;

      set h = (( proj2 | P) * f);

      

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

      then

       A3: ( rng f1) c= P by RELAT_1:def 19;

      rj is continuous by Th11;

      then (rj | (( TOP-REAL 2) | P)) is continuous Function of (( TOP-REAL 2) | P), R^1 ;

      then (rj | P) is continuous Function of (( TOP-REAL 2) | P), R^1 by A2, TMAP_1:def 3;

      then

      reconsider h2 = h as continuous Function of I[01] , R^1 by A1, Lm1;

      take h2;

      thus h2 is continuous;

      let r be Real, q be Point of ( TOP-REAL 2);

      assume that

       A4: r in the carrier of I[01] and

       A5: q = (f . r);

      

       A6: ( dom proj2 ) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

      

       A7: r in ( dom f1) by A4, FUNCT_2:def 1;

      then (f1 . r) in ( rng f1) by FUNCT_1:def 3;

      then

       A8: q in (( dom proj2 ) /\ P) by A5, A3, A6, XBOOLE_0:def 4;

      

      thus (h2 . r) = (( proj2 | P) . q) by A5, A7, FUNCT_1: 13

      .= ( proj2 . q) by A8, FUNCT_1: 48

      .= (q `2 ) by PSCOMP_1:def 6;

    end;

    theorem :: TOPREAL5:14

    

     Th14: for P be non empty Subset of ( TOP-REAL 2) st P is being_simple_closed_curve holds not (ex r st for p st p in P holds (p `2 ) = r)

    proof

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

      assume

       A1: P is being_simple_closed_curve;

      now

        

         A2: [. 0 , 1.] = ( ]. 0 , 1.[ \/ { 0 , 1}) by XXREAL_1: 128;

        given r0 such that

         A3: for p st p in P holds (p `2 ) = r0;

        consider p1,p2 be Point of ( TOP-REAL 2), P1,P2 be non empty Subset of ( TOP-REAL 2) such that

         A4: p1 <> p2 and

         A5: p1 in P and

         A6: p2 in P and

         A7: P1 is_an_arc_of (p1,p2) and

         A8: P2 is_an_arc_of (p1,p2) and

         A9: P = (P1 \/ P2) and

         A10: (P1 /\ P2) = {p1, p2} by A1, TOPREAL2: 6;

        

         A11: (p1 `2 ) = r0 by A3, A5;

        

         A12: (p2 `2 ) = r0 by A3, A6;

        then

         A13: (p1 `2 ) = (p2 `2 ) by A3, A5;

         A14:

        now

          assume (p1 `1 ) = (p2 `1 );

          then p1 = |[(p2 `1 ), (p2 `2 )]| by A13, EUCLID: 53;

          hence contradiction by A4, EUCLID: 53;

        end;

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

         A15: f2 is being_homeomorphism and

         A16: (f2 . 0 ) = p1 and

         A17: (f2 . 1) = p2 by A8, TOPREAL1:def 1;

        f2 is continuous by A15, TOPS_2:def 5;

        then

        consider g2 be Function of I[01] , R^1 such that

         A18: g2 is continuous and

         A19: for r, q2 st r in the carrier of I[01] & q2 = (f2 . r) holds (q2 `1 ) = (g2 . r) by Th12;

        

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

        1 in { 0 , 1} by TARSKI:def 2;

        then

         A21: 1 in the carrier of I[01] by A2, BORSUK_1: 40, XBOOLE_0:def 3;

        then

         A22: (p2 `1 ) = (g2 . 1) by A17, A19;

         0 in { 0 , 1} by TARSKI:def 2;

        then

         A23: 0 in the carrier of I[01] by A2, BORSUK_1: 40, XBOOLE_0:def 3;

        then (p1 `1 ) = (g2 . 0 ) by A16, A19;

        then

        consider r2 such that

         A24: 0 < r2 & r2 < 1 and

         A25: (g2 . r2) = (((p1 `1 ) + (p2 `1 )) / 2) by A18, A22, A14, Th9;

        

         A26: [. 0 , 1.] = { r3 : 0 <= r3 & r3 <= 1 } by RCOMP_1:def 1;

        then

         A27: r2 in the carrier of I[01] by A24, BORSUK_1: 40;

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

        then

         A28: (f2 . r2) in ( rng f2) by A27, FUNCT_1:def 3;

        then

         A29: (f2 . r2) in P by A9, A20, XBOOLE_0:def 3;

        (f2 . r2) in P2 by A28, A20;

        then

        reconsider p4 = (f2 . r2) as Point of ( TOP-REAL 2);

        

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

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

         A31: f1 is being_homeomorphism and

         A32: (f1 . 0 ) = p1 and

         A33: (f1 . 1) = p2 by A7, TOPREAL1:def 1;

        f1 is continuous by A31, TOPS_2:def 5;

        then

        consider g1 be Function of I[01] , R^1 such that

         A34: g1 is continuous and

         A35: for r, q1 st r in the carrier of I[01] & q1 = (f1 . r) holds (q1 `1 ) = (g1 . r) by Th12;

        

         A36: (p2 `1 ) = (g1 . 1) by A33, A35, A21;

        (p1 `1 ) = (g1 . 0 ) by A32, A35, A23;

        then

        consider r1 such that

         A37: 0 < r1 & r1 < 1 and

         A38: (g1 . r1) = (((p1 `1 ) + (p2 `1 )) / 2) by A34, A36, A14, Th9;

        

         A39: r1 in the carrier of I[01] by A37, A26, BORSUK_1: 40;

        then r1 in ( dom f1) by FUNCT_2:def 1;

        then

         A40: (f1 . r1) in ( rng f1) by FUNCT_1:def 3;

        then (f1 . r1) in P1 by A30;

        then

        reconsider p3 = (f1 . r1) as Point of ( TOP-REAL 2);

        (f1 . r1) in P by A9, A40, A30, XBOOLE_0:def 3;

        

        then

         A41: (p3 `2 ) = r0 by A3

        .= (p4 `2 ) by A3, A29;

        (p3 `1 ) = (((p1 `1 ) + (p2 `1 )) / 2) by A35, A38, A39

        .= (p4 `1 ) by A19, A25, A27;

        then (f1 . r1) = (f2 . r2) by A41, TOPREAL3: 6;

        then

         A42: (f1 . r1) in (P1 /\ P2) by A40, A30, A28, A20, XBOOLE_0:def 4;

        now

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

            case

             A43: (f1 . r1) = p1;

            

             A44: ((((1 / 2) * p1) + ((1 / 2) * p2)) `2 ) = ((((1 / 2) * p1) `2 ) + (((1 / 2) * p2) `2 )) by TOPREAL3: 2

            .= (((1 / 2) * (p1 `2 )) + (((1 / 2) * p2) `2 )) by TOPREAL3: 4

            .= (((1 / 2) * r0) + ((1 / 2) * r0)) by A11, A12, TOPREAL3: 4

            .= r0;

            (p1 `1 ) = (((2 " ) * (p1 `1 )) + ((p2 `1 ) / 2)) by A35, A38, A39, A43

            .= ((((2 " ) * p1) `1 ) + ((2 " ) * (p2 `1 ))) by TOPREAL3: 4

            .= ((((2 " ) * p1) `1 ) + (((2 " ) * p2) `1 )) by TOPREAL3: 4

            .= ((((1 / 2) * p1) + ((1 / 2) * p2)) `1 ) by TOPREAL3: 2;

            then p1 = (((1 / 2) * p1) + ((1 / 2) * p2)) by A11, A44, TOPREAL3: 6;

            then ((1 * p1) - ((1 / 2) * p1)) = ((((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p1)) by RLVECT_1:def 8;

            then ((1 * p1) - ((1 / 2) * p1)) = (((1 / 2) * p2) + (((1 / 2) * p1) - ((1 / 2) * p1))) by RLVECT_1:def 3;

            then ((1 * p1) - ((1 / 2) * p1)) = (((1 / 2) * p2) + ( 0. ( TOP-REAL 2))) by RLVECT_1: 5;

            then ((1 * p1) - ((1 / 2) * p1)) = ((1 / 2) * p2) by RLVECT_1: 4;

            then ((1 - (1 / 2)) * p1) = ((1 / 2) * p2) by RLVECT_1: 35;

            hence contradiction by A4, RLVECT_1: 36;

          end;

            case

             A45: (f1 . r1) = p2;

            

             A46: ((((1 / 2) * p1) + ((1 / 2) * p2)) `2 ) = ((((1 / 2) * p1) `2 ) + (((1 / 2) * p2) `2 )) by TOPREAL3: 2

            .= (((1 / 2) * (p1 `2 )) + (((1 / 2) * p2) `2 )) by TOPREAL3: 4

            .= (((1 / 2) * r0) + ((1 / 2) * r0)) by A11, A12, TOPREAL3: 4

            .= r0;

            (p2 `1 ) = (((2 " ) * (p1 `1 )) + ((p2 `1 ) / 2)) by A35, A38, A39, A45

            .= ((((2 " ) * p1) `1 ) + ((2 " ) * (p2 `1 ))) by TOPREAL3: 4

            .= ((((2 " ) * p1) `1 ) + (((2 " ) * p2) `1 )) by TOPREAL3: 4

            .= ((((1 / 2) * p1) + ((1 / 2) * p2)) `1 ) by TOPREAL3: 2;

            then p2 = (((1 / 2) * p1) + ((1 / 2) * p2)) by A12, A46, TOPREAL3: 6;

            then ((1 * p2) - ((1 / 2) * p2)) = ((((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p2)) by RLVECT_1:def 8;

            then ((1 * p2) - ((1 / 2) * p2)) = (((1 / 2) * p1) + (((1 / 2) * p2) - ((1 / 2) * p2))) by RLVECT_1:def 3;

            then ((1 * p2) - ((1 / 2) * p2)) = (((1 / 2) * p1) + ( 0. ( TOP-REAL 2))) by RLVECT_1: 5;

            then ((1 * p2) - ((1 / 2) * p2)) = ((1 / 2) * p1) by RLVECT_1: 4;

            then ((1 - (1 / 2)) * p2) = ((1 / 2) * p1) by RLVECT_1: 35;

            hence contradiction by A4, RLVECT_1: 36;

          end;

        end;

        hence contradiction;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL5:15

    

     Th15: for P be non empty Subset of ( TOP-REAL 2) st P is being_simple_closed_curve holds not (ex r st for p st p in P holds (p `1 ) = r)

    proof

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

      assume

       A1: P is being_simple_closed_curve;

      now

        

         A2: [. 0 , 1.] = ( ]. 0 , 1.[ \/ { 0 , 1}) by XXREAL_1: 128;

        given r0 such that

         A3: for p st p in P holds (p `1 ) = r0;

        consider p1,p2 be Point of ( TOP-REAL 2), P1,P2 be non empty Subset of ( TOP-REAL 2) such that

         A4: p1 <> p2 and

         A5: p1 in P and

         A6: p2 in P and

         A7: P1 is_an_arc_of (p1,p2) and

         A8: P2 is_an_arc_of (p1,p2) and

         A9: P = (P1 \/ P2) and

         A10: (P1 /\ P2) = {p1, p2} by A1, TOPREAL2: 6;

        

         A11: (p1 `1 ) = r0 by A3, A5;

        

         A12: (p2 `1 ) = r0 by A3, A6;

        then

         A13: (p1 `1 ) = (p2 `1 ) by A3, A5;

         A14:

        now

          assume (p1 `2 ) = (p2 `2 );

          then p1 = |[(p2 `1 ), (p2 `2 )]| by A13, EUCLID: 53;

          hence contradiction by A4, EUCLID: 53;

        end;

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

         A15: f2 is being_homeomorphism and

         A16: (f2 . 0 ) = p1 and

         A17: (f2 . 1) = p2 by A8, TOPREAL1:def 1;

        f2 is continuous by A15, TOPS_2:def 5;

        then

        consider g2 be Function of I[01] , R^1 such that

         A18: g2 is continuous and

         A19: for r, q2 st r in the carrier of I[01] & q2 = (f2 . r) holds (q2 `2 ) = (g2 . r) by Th13;

        

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

        1 in { 0 , 1} by TARSKI:def 2;

        then

         A21: 1 in the carrier of I[01] by A2, BORSUK_1: 40, XBOOLE_0:def 3;

        then

         A22: (p2 `2 ) = (g2 . 1) by A17, A19;

         0 in { 0 , 1} by TARSKI:def 2;

        then

         A23: 0 in the carrier of I[01] by A2, BORSUK_1: 40, XBOOLE_0:def 3;

        then (p1 `2 ) = (g2 . 0 ) by A16, A19;

        then

        consider r2 such that

         A24: 0 < r2 & r2 < 1 and

         A25: (g2 . r2) = (((p1 `2 ) + (p2 `2 )) / 2) by A18, A22, A14, Th9;

        

         A26: [. 0 , 1.] = { r3 : 0 <= r3 & r3 <= 1 } by RCOMP_1:def 1;

        then

         A27: r2 in the carrier of I[01] by A24, BORSUK_1: 40;

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

        then

         A28: (f2 . r2) in ( rng f2) by A27, FUNCT_1:def 3;

        then

         A29: (f2 . r2) in P by A9, A20, XBOOLE_0:def 3;

        (f2 . r2) in P2 by A28, A20;

        then

        reconsider p4 = (f2 . r2) as Point of ( TOP-REAL 2);

        

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

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

         A31: f1 is being_homeomorphism and

         A32: (f1 . 0 ) = p1 and

         A33: (f1 . 1) = p2 by A7, TOPREAL1:def 1;

        f1 is continuous by A31, TOPS_2:def 5;

        then

        consider g1 be Function of I[01] , R^1 such that

         A34: g1 is continuous and

         A35: for r, q1 st r in the carrier of I[01] & q1 = (f1 . r) holds (q1 `2 ) = (g1 . r) by Th13;

        

         A36: (p2 `2 ) = (g1 . 1) by A33, A35, A21;

        (p1 `2 ) = (g1 . 0 ) by A32, A35, A23;

        then

        consider r1 such that

         A37: 0 < r1 & r1 < 1 and

         A38: (g1 . r1) = (((p1 `2 ) + (p2 `2 )) / 2) by A34, A36, A14, Th9;

        

         A39: r1 in the carrier of I[01] by A37, A26, BORSUK_1: 40;

        then r1 in ( dom f1) by FUNCT_2:def 1;

        then

         A40: (f1 . r1) in ( rng f1) by FUNCT_1:def 3;

        then (f1 . r1) in P1 by A30;

        then

        reconsider p3 = (f1 . r1) as Point of ( TOP-REAL 2);

        (f1 . r1) in P by A9, A40, A30, XBOOLE_0:def 3;

        

        then

         A41: (p3 `1 ) = r0 by A3

        .= (p4 `1 ) by A3, A29;

        (p3 `2 ) = (((p1 `2 ) + (p2 `2 )) / 2) by A35, A38, A39

        .= (p4 `2 ) by A19, A25, A27;

        then (f1 . r1) = (f2 . r2) by A41, TOPREAL3: 6;

        then

         A42: (f1 . r1) in (P1 /\ P2) by A40, A30, A28, A20, XBOOLE_0:def 4;

        now

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

            case

             A43: (f1 . r1) = p1;

            

             A44: ((((1 / 2) * p1) + ((1 / 2) * p2)) `1 ) = ((((1 / 2) * p1) `1 ) + (((1 / 2) * p2) `1 )) by TOPREAL3: 2

            .= (((1 / 2) * (p1 `1 )) + (((1 / 2) * p2) `1 )) by TOPREAL3: 4

            .= (((1 / 2) * r0) + ((1 / 2) * r0)) by A11, A12, TOPREAL3: 4

            .= r0;

            (p1 `2 ) = (((2 " ) * (p1 `2 )) + ((p2 `2 ) / 2)) by A35, A38, A39, A43

            .= ((((2 " ) * p1) `2 ) + ((2 " ) * (p2 `2 ))) by TOPREAL3: 4

            .= ((((2 " ) * p1) `2 ) + (((2 " ) * p2) `2 )) by TOPREAL3: 4

            .= ((((1 / 2) * p1) + ((1 / 2) * p2)) `2 ) by TOPREAL3: 2;

            then p1 = (((1 / 2) * p1) + ((1 / 2) * p2)) by A11, A44, TOPREAL3: 6;

            then ((1 * p1) - ((1 / 2) * p1)) = ((((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p1)) by RLVECT_1:def 8;

            then ((1 * p1) - ((1 / 2) * p1)) = (((1 / 2) * p2) + (((1 / 2) * p1) - ((1 / 2) * p1))) by RLVECT_1:def 3;

            then ((1 * p1) - ((1 / 2) * p1)) = (((1 / 2) * p2) + ( 0. ( TOP-REAL 2))) by RLVECT_1: 5;

            then ((1 * p1) - ((1 / 2) * p1)) = ((1 / 2) * p2) by RLVECT_1: 4;

            then ((1 - (1 / 2)) * p1) = ((1 / 2) * p2) by RLVECT_1: 35;

            hence contradiction by A4, RLVECT_1: 36;

          end;

            case

             A45: (f1 . r1) = p2;

            

             A46: ((((1 / 2) * p1) + ((1 / 2) * p2)) `1 ) = ((((1 / 2) * p1) `1 ) + (((1 / 2) * p2) `1 )) by TOPREAL3: 2

            .= (((1 / 2) * (p1 `1 )) + (((1 / 2) * p2) `1 )) by TOPREAL3: 4

            .= (((1 / 2) * r0) + ((1 / 2) * r0)) by A11, A12, TOPREAL3: 4

            .= r0;

            (p2 `2 ) = (((2 " ) * (p1 `2 )) + ((p2 `2 ) / 2)) by A35, A38, A39, A45

            .= ((((2 " ) * p1) `2 ) + ((2 " ) * (p2 `2 ))) by TOPREAL3: 4

            .= ((((2 " ) * p1) `2 ) + (((2 " ) * p2) `2 )) by TOPREAL3: 4

            .= ((((1 / 2) * p1) + ((1 / 2) * p2)) `2 ) by TOPREAL3: 2;

            then p2 = (((1 / 2) * p1) + ((1 / 2) * p2)) by A12, A46, TOPREAL3: 6;

            then ((1 * p2) - ((1 / 2) * p2)) = ((((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p2)) by RLVECT_1:def 8;

            then ((1 * p2) - ((1 / 2) * p2)) = (((1 / 2) * p1) + (((1 / 2) * p2) - ((1 / 2) * p2))) by RLVECT_1:def 3;

            then ((1 * p2) - ((1 / 2) * p2)) = (((1 / 2) * p1) + ( 0. ( TOP-REAL 2))) by RLVECT_1: 5;

            then ((1 * p2) - ((1 / 2) * p2)) = ((1 / 2) * p1) by RLVECT_1: 4;

            then ((1 - (1 / 2)) * p2) = ((1 / 2) * p1) by RLVECT_1: 35;

            hence contradiction by A4, RLVECT_1: 36;

          end;

        end;

        hence contradiction;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL5:16

    

     Th16: for C be compact non empty Subset of ( TOP-REAL 2) st C is being_simple_closed_curve holds ( N-bound C) > ( S-bound C)

    proof

      let C be compact non empty Subset of ( TOP-REAL 2);

      assume

       A1: C is being_simple_closed_curve;

      now

        assume

         A2: ( N-bound C) <= ( S-bound C);

        for p st p in C holds (p `2 ) = ( S-bound C)

        proof

          let p;

          assume p in C;

          then

           A3: ( S-bound C) <= (p `2 ) & (p `2 ) <= ( N-bound C) by PSCOMP_1: 24;

          then ( S-bound C) <= ( N-bound C) by XXREAL_0: 2;

          then ( S-bound C) = ( N-bound C) by A2, XXREAL_0: 1;

          hence thesis by A3, XXREAL_0: 1;

        end;

        hence contradiction by A1, Th14;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL5:17

    

     Th17: for C be compact non empty Subset of ( TOP-REAL 2) st C is being_simple_closed_curve holds ( E-bound C) > ( W-bound C)

    proof

      let C be compact non empty Subset of ( TOP-REAL 2);

      assume

       A1: C is being_simple_closed_curve;

      now

        assume

         A2: ( E-bound C) <= ( W-bound C);

        for p st p in C holds (p `1 ) = ( W-bound C)

        proof

          let p;

          assume p in C;

          then

           A3: ( W-bound C) <= (p `1 ) & (p `1 ) <= ( E-bound C) by PSCOMP_1: 24;

          then ( W-bound C) <= ( E-bound C) by XXREAL_0: 2;

          then ( W-bound C) = ( E-bound C) by A2, XXREAL_0: 1;

          hence thesis by A3, XXREAL_0: 1;

        end;

        hence contradiction by A1, Th15;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL5:18

    for P be compact non empty Subset of ( TOP-REAL 2) st P is being_simple_closed_curve holds ( S-min P) <> ( N-max P)

    proof

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

      assume

       A1: P is being_simple_closed_curve;

      now

        

         A2: |[( lower_bound ( proj1 | ( S-most P))), ( S-bound P)]| = ( S-min P) & |[( upper_bound ( proj1 | ( N-most P))), ( N-bound P)]| = ( N-max P) by PSCOMP_1:def 22, PSCOMP_1:def 26;

        assume ( S-min P) = ( N-max P);

        then ( S-bound P) = ( N-bound P) by A2, SPPOL_2: 1;

        hence contradiction by A1, Th16;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL5:19

    for P be compact non empty Subset of ( TOP-REAL 2) st P is being_simple_closed_curve holds ( W-min P) <> ( E-max P)

    proof

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

      assume

       A1: P is being_simple_closed_curve;

      now

        

         A2: |[( W-bound P), ( lower_bound ( proj2 | ( W-most P)))]| = ( W-min P) & |[( E-bound P), ( upper_bound ( proj2 | ( E-most P)))]| = ( E-max P) by PSCOMP_1:def 19, PSCOMP_1:def 23;

        assume ( W-min P) = ( E-max P);

        then ( W-bound P) = ( E-bound P) by A2, SPPOL_2: 1;

        hence contradiction by A1, Th17;

      end;

      hence thesis;

    end;

    registration

      cluster -> non vertical non horizontal for Simple_closed_curve;

      coherence

      proof

        let S be Simple_closed_curve;

        consider p1 be object such that

         A1: p1 in S by XBOOLE_0:def 1;

        reconsider p1 as Point of ( TOP-REAL 2) by A1;

        ex p2 be Point of ( TOP-REAL 2) st p2 in S & (p2 `1 ) <> (p1 `1 ) by Th15;

        hence S is non vertical by A1, SPPOL_1:def 3;

        ex p2 be Point of ( TOP-REAL 2) st p2 in S & (p2 `2 ) <> (p1 `2 ) by Th14;

        hence thesis by A1, SPPOL_1:def 2;

      end;

    end