jordan21.miz



    begin

    reserve C for Simple_closed_curve,

P for Subset of ( TOP-REAL 2),

p for Point of ( TOP-REAL 2),

n for Element of NAT ;

    

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

    

     Lm2: for r be Real, X be Subset of ( TOP-REAL 2) st r in ( proj2 .: X) holds ex x be Point of ( TOP-REAL 2) st x in X & ( proj2 . x) = r

    proof

      let r be Real, X be Subset of ( TOP-REAL 2);

      assume r in ( proj2 .: X);

      then ex x be object st x in the carrier of ( TOP-REAL 2) & x in X & ( proj2 . x) = r by FUNCT_2: 64;

      hence thesis;

    end;

     Lm3:

    now

      let a,A,B,C be set;

      assume a in ((A \/ B) \/ C);

      then a in (A \/ B) or a in C by XBOOLE_0:def 3;

      hence a in A or a in B or a in C by XBOOLE_0:def 3;

    end;

    

     Lm4: for A,B,C,D be set st A misses D & B misses D & C misses D holds ((A \/ B) \/ C) misses D

    proof

      let A,B,C,D be set;

      assume A misses D & B misses D;

      then

       A1: (A \/ B) misses D by XBOOLE_1: 70;

      assume C misses D;

      hence thesis by A1, XBOOLE_1: 70;

    end;

    theorem :: JORDAN21:1

    for p be Point of ( TOP-REAL n) holds {p} is bounded

    proof

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

      reconsider a = p as Point of ( Euclid n) by EUCLID: 67;

       {a} is bounded by TBSP_1: 15;

      hence thesis by JORDAN2C: 11;

    end;

    theorem :: JORDAN21:2

    

     Th2: for s1,t be Real, P be Subset of ( TOP-REAL 2) st P = { |[s, t]| where s be Real : s1 < s } holds P is convex

    proof

      let s1,t be Real, P be Subset of ( TOP-REAL 2);

      assume

       A1: P = { |[s, t]| where s be Real : s1 < s };

      let w1,w2 be Point of ( TOP-REAL 2) such that

       A2: w1 in P and

       A3: w2 in P;

      consider s3 be Real such that

       A4: |[s3, t]| = w1 and

       A5: s1 < s3 by A1, A2;

      consider s4 be Real such that

       A6: |[s4, t]| = w2 and

       A7: s1 < s4 by A1, A3;

      

       A8: (w2 `1 ) = s4 by A6, EUCLID: 52;

      let x be object;

      assume x in ( LSeg (w1,w2));

      then

      consider l be Real such that

       A9: x = (((1 - l) * w1) + (l * w2)) and

       A10: 0 <= l & l <= 1;

      set w = (((1 - l) * w1) + (l * w2));

      

       A11: w = |[((((1 - l) * w1) `1 ) + ((l * w2) `1 )), ((((1 - l) * w1) `2 ) + ((l * w2) `2 ))]| by EUCLID: 55;

      

       A12: (l * w2) = |[(l * (w2 `1 )), (l * (w2 `2 ))]| by EUCLID: 57;

      then

       A13: ((l * w2) `1 ) = (l * (w2 `1 )) by EUCLID: 52;

      

       A14: ((1 - l) * w1) = |[((1 - l) * (w1 `1 )), ((1 - l) * (w1 `2 ))]| by EUCLID: 57;

      then (((1 - l) * w1) `1 ) = ((1 - l) * (w1 `1 )) by EUCLID: 52;

      then

       A15: (w `1 ) = (((1 - l) * (w1 `1 )) + (l * (w2 `1 ))) by A11, A13, EUCLID: 52;

      

       A16: ((l * w2) `2 ) = (l * (w2 `2 )) by A12, EUCLID: 52;

      (((1 - l) * w1) `2 ) = ((1 - l) * (w1 `2 )) by A14, EUCLID: 52;

      then

       A17: (w `2 ) = (((1 - l) * (w1 `2 )) + (l * (w2 `2 ))) by A11, A16, EUCLID: 52;

      (w2 `2 ) = t by A6, EUCLID: 52;

      

      then

       A18: (w `2 ) = (((1 - l) * t) + (l * t)) by A4, A17, EUCLID: 52

      .= (t - 0 );

      

       A19: w = |[(w `1 ), (w `2 )]| by EUCLID: 53;

      (w1 `1 ) = s3 by A4, EUCLID: 52;

      then s1 < (w `1 ) by A5, A7, A8, A10, A15, XREAL_1: 175;

      hence thesis by A1, A9, A19, A18;

    end;

    theorem :: JORDAN21:3

    

     Th3: for s2,t be Real, P be Subset of ( TOP-REAL 2) st P = { |[s, t]| where s be Real : s < s2 } holds P is convex

    proof

      let s2,t be Real, P be Subset of ( TOP-REAL 2);

      assume

       A1: P = { |[s, t]| where s be Real : s < s2 };

      let w1,w2 be Point of ( TOP-REAL 2) such that

       A2: w1 in P and

       A3: w2 in P;

      consider s3 be Real such that

       A4: |[s3, t]| = w1 and

       A5: s3 < s2 by A1, A2;

      consider s4 be Real such that

       A6: |[s4, t]| = w2 and

       A7: s4 < s2 by A1, A3;

      

       A8: (w2 `1 ) = s4 by A6, EUCLID: 52;

      let x be object;

      assume x in ( LSeg (w1,w2));

      then

      consider l be Real such that

       A9: x = (((1 - l) * w1) + (l * w2)) and

       A10: 0 <= l & l <= 1;

      set w = (((1 - l) * w1) + (l * w2));

      

       A11: w = |[((((1 - l) * w1) `1 ) + ((l * w2) `1 )), ((((1 - l) * w1) `2 ) + ((l * w2) `2 ))]| by EUCLID: 55;

      

       A12: (l * w2) = |[(l * (w2 `1 )), (l * (w2 `2 ))]| by EUCLID: 57;

      then

       A13: ((l * w2) `1 ) = (l * (w2 `1 )) by EUCLID: 52;

      

       A14: ((1 - l) * w1) = |[((1 - l) * (w1 `1 )), ((1 - l) * (w1 `2 ))]| by EUCLID: 57;

      then (((1 - l) * w1) `1 ) = ((1 - l) * (w1 `1 )) by EUCLID: 52;

      then

       A15: (w `1 ) = (((1 - l) * (w1 `1 )) + (l * (w2 `1 ))) by A11, A13, EUCLID: 52;

      

       A16: ((l * w2) `2 ) = (l * (w2 `2 )) by A12, EUCLID: 52;

      (((1 - l) * w1) `2 ) = ((1 - l) * (w1 `2 )) by A14, EUCLID: 52;

      then

       A17: (w `2 ) = (((1 - l) * (w1 `2 )) + (l * (w2 `2 ))) by A11, A16, EUCLID: 52;

      (w2 `2 ) = t by A6, EUCLID: 52;

      

      then

       A18: (w `2 ) = (((1 - l) * t) + (l * t)) by A4, A17, EUCLID: 52

      .= (t - 0 );

      

       A19: w = |[(w `1 ), (w `2 )]| by EUCLID: 53;

      (w1 `1 ) = s3 by A4, EUCLID: 52;

      then s2 > (w `1 ) by A5, A7, A8, A10, A15, XREAL_1: 176;

      hence thesis by A1, A9, A19, A18;

    end;

    theorem :: JORDAN21:4

    

     Th4: for s,t1 be Real, P be Subset of ( TOP-REAL 2) st P = { |[s, t]| where t be Real : t1 < t } holds P is convex

    proof

      let s,t1 be Real, P be Subset of ( TOP-REAL 2);

      assume

       A1: P = { |[s, t]| where t be Real : t1 < t };

      let w1,w2 be Point of ( TOP-REAL 2) such that

       A2: w1 in P and

       A3: w2 in P;

      consider t3 be Real such that

       A4: |[s, t3]| = w1 and

       A5: t1 < t3 by A1, A2;

      

       A6: (w1 `1 ) = s by A4, EUCLID: 52;

      let x be object;

      assume x in ( LSeg (w1,w2));

      then

      consider l be Real such that

       A7: x = (((1 - l) * w1) + (l * w2)) and

       A8: 0 <= l & l <= 1;

      set w = (((1 - l) * w1) + (l * w2));

      

       A9: w = |[((((1 - l) * w1) `1 ) + ((l * w2) `1 )), ((((1 - l) * w1) `2 ) + ((l * w2) `2 ))]| by EUCLID: 55;

      consider t4 be Real such that

       A10: |[s, t4]| = w2 and

       A11: t1 < t4 by A1, A3;

      

       A12: (w2 `1 ) = s by A10, EUCLID: 52;

      

       A13: (l * w2) = |[(l * (w2 `1 )), (l * (w2 `2 ))]| by EUCLID: 57;

      then

       A14: ((l * w2) `1 ) = (l * (w2 `1 )) by EUCLID: 52;

      

       A15: ((l * w2) `2 ) = (l * (w2 `2 )) by A13, EUCLID: 52;

      

       A16: ((1 - l) * w1) = |[((1 - l) * (w1 `1 )), ((1 - l) * (w1 `2 ))]| by EUCLID: 57;

      then (((1 - l) * w1) `2 ) = ((1 - l) * (w1 `2 )) by EUCLID: 52;

      then

       A17: (w `2 ) = (((1 - l) * (w1 `2 )) + (l * (w2 `2 ))) by A9, A15, EUCLID: 52;

      

       A18: (w2 `2 ) = t4 by A10, EUCLID: 52;

      (((1 - l) * w1) `1 ) = ((1 - l) * (w1 `1 )) by A16, EUCLID: 52;

      then

       A19: w = |[(w `1 ), (w `2 )]| & (w `1 ) = (s - 0 ) by A6, A12, A9, A14, EUCLID: 52, EUCLID: 53;

      (w1 `2 ) = t3 by A4, EUCLID: 52;

      then t1 < (w `2 ) by A5, A11, A18, A8, A17, XREAL_1: 175;

      hence thesis by A1, A7, A19;

    end;

    theorem :: JORDAN21:5

    

     Th5: for s,t2 be Real, P be Subset of ( TOP-REAL 2) st P = { |[s, t]| where t be Real : t < t2 } holds P is convex

    proof

      let s,t2 be Real, P be Subset of ( TOP-REAL 2);

      assume

       A1: P = { |[s, t]| where t be Real : t < t2 };

      let w1,w2 be Point of ( TOP-REAL 2) such that

       A2: w1 in P and

       A3: w2 in P;

      consider t3 be Real such that

       A4: |[s, t3]| = w1 and

       A5: t3 < t2 by A1, A2;

      consider t4 be Real such that

       A6: |[s, t4]| = w2 and

       A7: t4 < t2 by A1, A3;

      

       A8: (w2 `2 ) = t4 by A6, EUCLID: 52;

      let x be object;

      assume x in ( LSeg (w1,w2));

      then

      consider l be Real such that

       A9: x = (((1 - l) * w1) + (l * w2)) and

       A10: 0 <= l & l <= 1;

      set w = (((1 - l) * w1) + (l * w2));

      

       A11: w = |[((((1 - l) * w1) `1 ) + ((l * w2) `1 )), ((((1 - l) * w1) `2 ) + ((l * w2) `2 ))]| by EUCLID: 55;

      

       A12: (l * w2) = |[(l * (w2 `1 )), (l * (w2 `2 ))]| by EUCLID: 57;

      then

       A13: ((l * w2) `1 ) = (l * (w2 `1 )) by EUCLID: 52;

      

       A14: ((1 - l) * w1) = |[((1 - l) * (w1 `1 )), ((1 - l) * (w1 `2 ))]| by EUCLID: 57;

      then (((1 - l) * w1) `1 ) = ((1 - l) * (w1 `1 )) by EUCLID: 52;

      then

       A15: (w `1 ) = (((1 - l) * (w1 `1 )) + (l * (w2 `1 ))) by A11, A13, EUCLID: 52;

      (w2 `1 ) = s by A6, EUCLID: 52;

      

      then

       A16: (w `1 ) = (((1 - l) * s) + (l * s)) by A4, A15, EUCLID: 52

      .= (s - 0 );

      

       A17: w = |[(w `1 ), (w `2 )]| by EUCLID: 53;

      

       A18: ((l * w2) `2 ) = (l * (w2 `2 )) by A12, EUCLID: 52;

      (((1 - l) * w1) `2 ) = ((1 - l) * (w1 `2 )) by A14, EUCLID: 52;

      then

       A19: (w `2 ) = (((1 - l) * (w1 `2 )) + (l * (w2 `2 ))) by A11, A18, EUCLID: 52;

      (w1 `2 ) = t3 by A4, EUCLID: 52;

      then t2 > (w `2 ) by A5, A7, A8, A10, A19, XREAL_1: 176;

      hence thesis by A1, A9, A17, A16;

    end;

    theorem :: JORDAN21:6

    (( north_halfline p) \ {p}) is convex

    proof

      set P = (( north_halfline p) \ {p});

      P = { |[(p `1 ), r]| where r be Real : r > (p `2 ) }

      proof

        hereby

          let x be object;

          assume

           A1: x in P;

          then

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

          

           A2: x in ( north_halfline p) by A1, XBOOLE_0:def 5;

          then

           A3: (y `1 ) = (p `1 ) by TOPREAL1:def 10;

          then

           A4: x = |[(p `1 ), (y `2 )]| by EUCLID: 53;

          

           A5: not x in {p} by A1, XBOOLE_0:def 5;

           A6:

          now

            assume (y `2 ) = (p `2 );

            then x = p by A3, TOPREAL3: 6;

            hence contradiction by A5, TARSKI:def 1;

          end;

          (y `2 ) >= (p `2 ) by A2, TOPREAL1:def 10;

          then (y `2 ) > (p `2 ) by A6, XXREAL_0: 1;

          hence x in { |[(p `1 ), r]| where r be Real : r > (p `2 ) } by A4;

        end;

        let x be object;

        assume x in { |[(p `1 ), r]| where r be Real : r > (p `2 ) };

        then

        consider r be Real such that

         A7: x = |[(p `1 ), r]| and

         A8: r > (p `2 );

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

        

         A9: (y `2 ) = r by A7, EUCLID: 52;

        then

         A10: not x in {p} by A8, TARSKI:def 1;

        (y `1 ) = (p `1 ) by A7, EUCLID: 52;

        then x in ( north_halfline p) by A8, A9, TOPREAL1:def 10;

        hence thesis by A10, XBOOLE_0:def 5;

      end;

      hence thesis by Th4;

    end;

    theorem :: JORDAN21:7

    (( south_halfline p) \ {p}) is convex

    proof

      set P = (( south_halfline p) \ {p});

      P = { |[(p `1 ), r]| where r be Real : r < (p `2 ) }

      proof

        hereby

          let x be object;

          assume

           A1: x in P;

          then

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

          

           A2: x in ( south_halfline p) by A1, XBOOLE_0:def 5;

          then

           A3: (y `1 ) = (p `1 ) by TOPREAL1:def 12;

          then

           A4: x = |[(p `1 ), (y `2 )]| by EUCLID: 53;

          

           A5: not x in {p} by A1, XBOOLE_0:def 5;

           A6:

          now

            assume (y `2 ) = (p `2 );

            then x = p by A3, TOPREAL3: 6;

            hence contradiction by A5, TARSKI:def 1;

          end;

          (y `2 ) <= (p `2 ) by A2, TOPREAL1:def 12;

          then (y `2 ) < (p `2 ) by A6, XXREAL_0: 1;

          hence x in { |[(p `1 ), r]| where r be Real : r < (p `2 ) } by A4;

        end;

        let x be object;

        assume x in { |[(p `1 ), r]| where r be Real : r < (p `2 ) };

        then

        consider r be Real such that

         A7: x = |[(p `1 ), r]| and

         A8: r < (p `2 );

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

        

         A9: (y `2 ) = r by A7, EUCLID: 52;

        then

         A10: not x in {p} by A8, TARSKI:def 1;

        (y `1 ) = (p `1 ) by A7, EUCLID: 52;

        then x in ( south_halfline p) by A8, A9, TOPREAL1:def 12;

        hence thesis by A10, XBOOLE_0:def 5;

      end;

      hence thesis by Th5;

    end;

    theorem :: JORDAN21:8

    (( west_halfline p) \ {p}) is convex

    proof

      set P = (( west_halfline p) \ {p});

      P = { |[r, (p `2 )]| where r be Real : r < (p `1 ) }

      proof

        hereby

          let x be object;

          assume

           A1: x in P;

          then

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

          

           A2: x in ( west_halfline p) by A1, XBOOLE_0:def 5;

          then

           A3: (y `2 ) = (p `2 ) by TOPREAL1:def 13;

          then

           A4: x = |[(y `1 ), (p `2 )]| by EUCLID: 53;

          

           A5: not x in {p} by A1, XBOOLE_0:def 5;

           A6:

          now

            assume (y `1 ) = (p `1 );

            then x = p by A3, TOPREAL3: 6;

            hence contradiction by A5, TARSKI:def 1;

          end;

          (y `1 ) <= (p `1 ) by A2, TOPREAL1:def 13;

          then (y `1 ) < (p `1 ) by A6, XXREAL_0: 1;

          hence x in { |[r, (p `2 )]| where r be Real : r < (p `1 ) } by A4;

        end;

        let x be object;

        assume x in { |[r, (p `2 )]| where r be Real : r < (p `1 ) };

        then

        consider r be Real such that

         A7: x = |[r, (p `2 )]| and

         A8: r < (p `1 );

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

        

         A9: (y `1 ) = r by A7, EUCLID: 52;

        then

         A10: not x in {p} by A8, TARSKI:def 1;

        (y `2 ) = (p `2 ) by A7, EUCLID: 52;

        then x in ( west_halfline p) by A8, A9, TOPREAL1:def 13;

        hence thesis by A10, XBOOLE_0:def 5;

      end;

      hence thesis by Th3;

    end;

    theorem :: JORDAN21:9

    (( east_halfline p) \ {p}) is convex

    proof

      set P = (( east_halfline p) \ {p});

      P = { |[r, (p `2 )]| where r be Real : r > (p `1 ) }

      proof

        hereby

          let x be object;

          assume

           A1: x in P;

          then

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

          

           A2: x in ( east_halfline p) by A1, XBOOLE_0:def 5;

          then

           A3: (y `2 ) = (p `2 ) by TOPREAL1:def 11;

          then

           A4: x = |[(y `1 ), (p `2 )]| by EUCLID: 53;

          

           A5: not x in {p} by A1, XBOOLE_0:def 5;

           A6:

          now

            assume (y `1 ) = (p `1 );

            then x = p by A3, TOPREAL3: 6;

            hence contradiction by A5, TARSKI:def 1;

          end;

          (y `1 ) >= (p `1 ) by A2, TOPREAL1:def 11;

          then (y `1 ) > (p `1 ) by A6, XXREAL_0: 1;

          hence x in { |[r, (p `2 )]| where r be Real : r > (p `1 ) } by A4;

        end;

        let x be object;

        assume x in { |[r, (p `2 )]| where r be Real : r > (p `1 ) };

        then

        consider r be Real such that

         A7: x = |[r, (p `2 )]| and

         A8: r > (p `1 );

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

        

         A9: (y `1 ) = r by A7, EUCLID: 52;

        then

         A10: not x in {p} by A8, TARSKI:def 1;

        (y `2 ) = (p `2 ) by A7, EUCLID: 52;

        then x in ( east_halfline p) by A8, A9, TOPREAL1:def 11;

        hence thesis by A10, XBOOLE_0:def 5;

      end;

      hence thesis by Th2;

    end;

    theorem :: JORDAN21:10

    for A be Subset of the carrier of ( TOP-REAL 2) holds ( UBD A) misses A

    proof

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

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

      hence thesis by XBOOLE_1: 63, XBOOLE_1: 79;

    end;

    theorem :: JORDAN21:11

    

     Th11: for P be Subset of the carrier of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2) st P is_an_arc_of (p1,p2) & p1 <> q1 & p2 <> q2 holds not p1 in ( Segment (P,p1,p2,q1,q2)) & not p2 in ( Segment (P,p1,p2,q1,q2))

    proof

      let P be Subset of the carrier of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2);

      assume P is_an_arc_of (p1,p2) & p1 <> q1 & p2 <> q2;

      then

       A1: ( not p2 in ( L_Segment (P,p1,p2,q2))) & not p1 in ( R_Segment (P,p1,p2,q1)) by JORDAN6: 59, JORDAN6: 60;

      ( Segment (P,p1,p2,q1,q2)) = (( R_Segment (P,p1,p2,q1)) /\ ( L_Segment (P,p1,p2,q2))) by JORDAN6:def 5;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    definition

      let D be Subset of ( TOP-REAL 2);

      :: JORDAN21:def1

      attr D is with_the_max_arc means

      : Def1: D meets ( Vertical_Line ((( W-bound D) + ( E-bound D)) / 2));

    end

    registration

      cluster with_the_max_arc -> non empty for Subset of ( TOP-REAL 2);

      coherence

      proof

        let D be Subset of ( TOP-REAL 2);

        assume D meets ( Vertical_Line ((( W-bound D) + ( E-bound D)) / 2));

        hence thesis;

      end;

    end

    registration

      cluster -> with_the_max_arc for Simple_closed_curve;

      coherence

      proof

        let C be Simple_closed_curve;

        (( Upper_Middle_Point C) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by JORDAN6: 65;

        then ( Upper_Middle_Point C) in C & ( Upper_Middle_Point C) in ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2)) by JORDAN6: 31, JORDAN6: 68;

        hence C meets ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2)) by XBOOLE_0: 3;

      end;

    end

    registration

      cluster non empty for Simple_closed_curve;

      existence

      proof

        set A = the Simple_closed_curve;

        take A;

        thus thesis;

      end;

    end

    reserve D for compact with_the_max_arc Subset of ( TOP-REAL 2);

    theorem :: JORDAN21:12

    

     Th12: for D be with_the_max_arc Subset of ( TOP-REAL 2) holds not ( proj2 .: (D /\ ( Vertical_Line ((( W-bound D) + ( E-bound D)) / 2)))) is empty

    proof

      let D be with_the_max_arc Subset of ( TOP-REAL 2);

      set w = ((( W-bound D) + ( E-bound D)) / 2);

      D meets ( Vertical_Line w) by Def1;

      then (D /\ ( Vertical_Line w)) is non empty;

      hence thesis by Lm1, RELAT_1: 119;

    end;

    theorem :: JORDAN21:13

    

     Th13: for C be compact Subset of ( TOP-REAL 2) holds ( proj2 .: (C /\ ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2)))) is closed bounded_below bounded_above

    proof

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

      set w = ((( W-bound C) + ( E-bound C)) / 2);

      set X = (C /\ ( Vertical_Line w));

      ( Vertical_Line w) is closed by JORDAN6: 30;

      then

       A1: X is closed by TOPS_1: 8;

      X is bounded by RLTOPSP1: 42, XBOOLE_1: 17;

      hence ( proj2 .: X) is closed by A1, JCT_MISC: 13;

      X c= C by XBOOLE_1: 17;

      then ( proj2 .: X) is real-bounded by JCT_MISC: 14, RLTOPSP1: 42;

      hence thesis by XXREAL_2:def 11;

    end;

    begin

    theorem :: JORDAN21:14

    

     Th14: ( Lower_Middle_Point C) in C

    proof

      ( Lower_Middle_Point C) in ( Lower_Arc C) & ( Lower_Arc C) c= C by JORDAN6: 61, JORDAN6: 66;

      hence thesis;

    end;

    theorem :: JORDAN21:15

    

     Th15: (( Lower_Middle_Point C) `2 ) <> (( Upper_Middle_Point C) `2 )

    proof

      set l = ( Lower_Middle_Point C), u = ( Upper_Middle_Point C), w = ((( W-bound C) + ( E-bound C)) / 2);

      

       A1: (l `1 ) = w by JORDAN6: 64;

      

       A2: (u `1 ) = w by JORDAN6: 65;

      assume (l `2 ) = (u `2 );

      then l = u by A1, A2, TOPREAL3: 6;

      then l in ( Lower_Arc C) & l in ( Upper_Arc C) by JORDAN6: 66, JORDAN6: 67;

      then l in (( Lower_Arc C) /\ ( Upper_Arc C)) by XBOOLE_0:def 4;

      then l in {( W-min C), ( E-max C)} by JORDAN6:def 9;

      then l = ( W-min C) or l = ( E-max C) by TARSKI:def 2;

      then ( W-bound C) = w or ( E-bound C) = w by A1, EUCLID: 52;

      hence thesis by SPRECT_1: 31;

    end;

    theorem :: JORDAN21:16

    ( Lower_Middle_Point C) <> ( Upper_Middle_Point C)

    proof

      (( Lower_Middle_Point C) `2 ) <> (( Upper_Middle_Point C) `2 ) by Th15;

      hence thesis;

    end;

    begin

    theorem :: JORDAN21:17

    

     Th17: ( W-bound C) = ( W-bound ( Upper_Arc C))

    proof

      

       A1: ( W-bound ( Upper_Arc C)) <= ( W-bound C)

      proof

        

         A2: (( W-min C) `1 ) = ( W-bound C) by EUCLID: 52;

        assume

         A3: ( W-bound ( Upper_Arc C)) > ( W-bound C);

        

         A4: ( west_halfline ( W-min C)) misses ( Upper_Arc C)

        proof

          assume ( west_halfline ( W-min C)) meets ( Upper_Arc C);

          then

          consider p be object such that

           A5: p in ( west_halfline ( W-min C)) and

           A6: p in ( Upper_Arc C) by XBOOLE_0: 3;

          reconsider p as Point of ( TOP-REAL 2) by A5;

          (p `1 ) >= ( W-bound ( Upper_Arc C)) by A6, PSCOMP_1: 24;

          then ( W-bound C) < (p `1 ) by A3, XXREAL_0: 2;

          hence contradiction by A2, A5, TOPREAL1:def 13;

        end;

        ( W-min C) in ( west_halfline ( W-min C)) & ( W-min C) in ( Upper_Arc C) by JORDAN7: 1, TOPREAL1: 38;

        hence contradiction by A4, XBOOLE_0: 3;

      end;

      ( W-bound C) <= ( W-bound ( Upper_Arc C)) by JORDAN6: 61, PSCOMP_1: 69;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: JORDAN21:18

    

     Th18: ( E-bound C) = ( E-bound ( Upper_Arc C))

    proof

      

       A1: ( E-bound ( Upper_Arc C)) >= ( E-bound C)

      proof

        

         A2: (( E-max C) `1 ) = ( E-bound C) by EUCLID: 52;

        assume

         A3: ( E-bound ( Upper_Arc C)) < ( E-bound C);

        

         A4: ( east_halfline ( E-max C)) misses ( Upper_Arc C)

        proof

          assume ( east_halfline ( E-max C)) meets ( Upper_Arc C);

          then

          consider p be object such that

           A5: p in ( east_halfline ( E-max C)) and

           A6: p in ( Upper_Arc C) by XBOOLE_0: 3;

          reconsider p as Point of ( TOP-REAL 2) by A5;

          (p `1 ) <= ( E-bound ( Upper_Arc C)) by A6, PSCOMP_1: 24;

          then ( E-bound C) > (p `1 ) by A3, XXREAL_0: 2;

          hence contradiction by A2, A5, TOPREAL1:def 11;

        end;

        ( E-max C) in ( east_halfline ( E-max C)) & ( E-max C) in ( Upper_Arc C) by JORDAN7: 1, TOPREAL1: 38;

        hence contradiction by A4, XBOOLE_0: 3;

      end;

      ( E-bound C) >= ( E-bound ( Upper_Arc C)) by JORDAN6: 61, PSCOMP_1: 67;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: JORDAN21:19

    

     Th19: ( W-bound C) = ( W-bound ( Lower_Arc C))

    proof

      

       A1: ( W-bound ( Lower_Arc C)) <= ( W-bound C)

      proof

        

         A2: (( W-min C) `1 ) = ( W-bound C) by EUCLID: 52;

        assume

         A3: ( W-bound ( Lower_Arc C)) > ( W-bound C);

        

         A4: ( west_halfline ( W-min C)) misses ( Lower_Arc C)

        proof

          assume ( west_halfline ( W-min C)) meets ( Lower_Arc C);

          then

          consider p be object such that

           A5: p in ( west_halfline ( W-min C)) and

           A6: p in ( Lower_Arc C) by XBOOLE_0: 3;

          reconsider p as Point of ( TOP-REAL 2) by A5;

          (p `1 ) >= ( W-bound ( Lower_Arc C)) by A6, PSCOMP_1: 24;

          then ( W-bound C) < (p `1 ) by A3, XXREAL_0: 2;

          hence contradiction by A2, A5, TOPREAL1:def 13;

        end;

        ( W-min C) in ( west_halfline ( W-min C)) & ( W-min C) in ( Lower_Arc C) by JORDAN7: 1, TOPREAL1: 38;

        hence contradiction by A4, XBOOLE_0: 3;

      end;

      ( W-bound C) <= ( W-bound ( Lower_Arc C)) by JORDAN6: 61, PSCOMP_1: 69;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: JORDAN21:20

    

     Th20: ( E-bound C) = ( E-bound ( Lower_Arc C))

    proof

      

       A1: ( E-bound ( Lower_Arc C)) >= ( E-bound C)

      proof

        

         A2: (( E-max C) `1 ) = ( E-bound C) by EUCLID: 52;

        assume

         A3: ( E-bound ( Lower_Arc C)) < ( E-bound C);

        

         A4: ( east_halfline ( E-max C)) misses ( Lower_Arc C)

        proof

          assume ( east_halfline ( E-max C)) meets ( Lower_Arc C);

          then

          consider p be object such that

           A5: p in ( east_halfline ( E-max C)) and

           A6: p in ( Lower_Arc C) by XBOOLE_0: 3;

          reconsider p as Point of ( TOP-REAL 2) by A5;

          (p `1 ) <= ( E-bound ( Lower_Arc C)) by A6, PSCOMP_1: 24;

          then ( E-bound C) > (p `1 ) by A3, XXREAL_0: 2;

          hence contradiction by A2, A5, TOPREAL1:def 11;

        end;

        ( E-max C) in ( east_halfline ( E-max C)) & ( E-max C) in ( Lower_Arc C) by JORDAN7: 1, TOPREAL1: 38;

        hence contradiction by A4, XBOOLE_0: 3;

      end;

      ( E-bound C) >= ( E-bound ( Lower_Arc C)) by JORDAN6: 61, PSCOMP_1: 67;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: JORDAN21:21

    

     Th21: not (( Upper_Arc C) /\ ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2))) is empty & not ( proj2 .: (( Upper_Arc C) /\ ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2)))) is empty

    proof

      set w = ((( W-bound C) + ( E-bound C)) / 2);

      

       A1: ( W-bound C) < ( E-bound C) by SPRECT_1: 31;

      (( E-max C) `1 ) = ( E-bound C) by EUCLID: 52;

      then

       A2: w <= (( E-max C) `1 ) by A1, XREAL_1: 226;

      (( W-min C) `1 ) = ( W-bound C) by EUCLID: 52;

      then ( Upper_Arc C) is_an_arc_of (( W-min C),( E-max C)) & (( W-min C) `1 ) <= w by A1, JORDAN6:def 8, XREAL_1: 226;

      then ( Upper_Arc C) meets ( Vertical_Line w) by A2, JORDAN6: 49;

      then (( Upper_Arc C) /\ ( Vertical_Line w)) is non empty;

      hence thesis by Lm1, RELAT_1: 119;

    end;

    theorem :: JORDAN21:22

    

     Th22: not (( Lower_Arc C) /\ ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2))) is empty & not ( proj2 .: (( Lower_Arc C) /\ ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2)))) is empty

    proof

      set w = ((( W-bound C) + ( E-bound C)) / 2);

      

       A1: ( W-bound C) < ( E-bound C) by SPRECT_1: 31;

      (( E-max C) `1 ) = ( E-bound C) by EUCLID: 52;

      then

       A2: w <= (( E-max C) `1 ) by A1, XREAL_1: 226;

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

      then

       A3: ( Lower_Arc C) is_an_arc_of (( W-min C),( E-max C)) by JORDAN5B: 14;

      (( W-min C) `1 ) = ( W-bound C) by EUCLID: 52;

      then (( W-min C) `1 ) <= w by A1, XREAL_1: 226;

      then ( Lower_Arc C) meets ( Vertical_Line w) by A3, A2, JORDAN6: 49;

      then (( Lower_Arc C) /\ ( Vertical_Line w)) is non empty;

      hence thesis by Lm1, RELAT_1: 119;

    end;

    theorem :: JORDAN21:23

    for P be compact connected Subset of ( TOP-REAL 2) st P c= C & ( W-min C) in P & ( E-max C) in P holds ( Upper_Arc C) c= P or ( Lower_Arc C) c= P

    proof

      let P be compact connected Subset of ( TOP-REAL 2) such that

       A1: P c= C and

       A2: ( W-min C) in P and

       A3: ( E-max C) in P;

       A4:

      now

        given p be Point of ( TOP-REAL 2) such that

         A5: P = {p};

        ( W-min C) = p & ( E-max C) = p by A2, A3, A5, TARSKI:def 1;

        hence contradiction by TOPREAL5: 19;

      end;

      per cases by A1, A2, A4, BORSUK_4: 56;

        suppose ex p1,p2 be Point of ( TOP-REAL 2) st P is_an_arc_of (p1,p2);

        hence thesis by A1, A2, A3, JORDAN16: 22;

      end;

        suppose P = C;

        hence thesis by JORDAN6: 61;

      end;

    end;

    registration

      let C;

      cluster ( Lower_Arc C) -> with_the_max_arc;

      coherence

      proof

        ( W-bound C) = ( W-bound ( Lower_Arc C)) & ( E-bound C) = ( E-bound ( Lower_Arc C)) by Th19, Th20;

        hence ( Lower_Arc C) meets ( Vertical_Line ((( W-bound ( Lower_Arc C)) + ( E-bound ( Lower_Arc C))) / 2)) by JORDAN6: 62;

      end;

      cluster ( Upper_Arc C) -> with_the_max_arc;

      coherence

      proof

        ( W-bound C) = ( W-bound ( Upper_Arc C)) & ( E-bound C) = ( E-bound ( Upper_Arc C)) by Th17, Th18;

        hence ( Upper_Arc C) meets ( Vertical_Line ((( W-bound ( Upper_Arc C)) + ( E-bound ( Upper_Arc C))) / 2)) by JORDAN6: 63;

      end;

    end

    begin

    definition

      let P be Subset of the carrier of ( TOP-REAL 2);

      :: JORDAN21:def2

      func UMP P -> Point of ( TOP-REAL 2) equals |[((( E-bound P) + ( W-bound P)) / 2), ( upper_bound ( proj2 .: (P /\ ( Vertical_Line ((( E-bound P) + ( W-bound P)) / 2)))))]|;

      correctness ;

      :: JORDAN21:def3

      func LMP P -> Point of ( TOP-REAL 2) equals |[((( E-bound P) + ( W-bound P)) / 2), ( lower_bound ( proj2 .: (P /\ ( Vertical_Line ((( E-bound P) + ( W-bound P)) / 2)))))]|;

      correctness ;

    end

    theorem :: JORDAN21:24

    

     Th24: for C be non vertical compact Subset of ( TOP-REAL 2) holds ( UMP C) <> ( W-min C)

    proof

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

      

       A1: (( W-min C) `1 ) = ( W-bound C) & (( UMP C) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by EUCLID: 52;

      assume ( UMP C) = ( W-min C);

      hence thesis by A1, SPRECT_1: 31;

    end;

    theorem :: JORDAN21:25

    

     Th25: for C be non vertical compact Subset of ( TOP-REAL 2) holds ( UMP C) <> ( E-max C)

    proof

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

      

       A1: (( E-max C) `1 ) = ( E-bound C) & (( UMP C) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by EUCLID: 52;

      assume ( UMP C) = ( E-max C);

      hence thesis by A1, SPRECT_1: 31;

    end;

    theorem :: JORDAN21:26

    

     Th26: for C be non vertical compact Subset of ( TOP-REAL 2) holds ( LMP C) <> ( W-min C)

    proof

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

      

       A1: (( W-min C) `1 ) = ( W-bound C) & (( LMP C) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by EUCLID: 52;

      assume ( LMP C) = ( W-min C);

      hence thesis by A1, SPRECT_1: 31;

    end;

    theorem :: JORDAN21:27

    

     Th27: for C be non vertical compact Subset of ( TOP-REAL 2) holds ( LMP C) <> ( E-max C)

    proof

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

      

       A1: (( E-max C) `1 ) = ( E-bound C) & (( LMP C) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by EUCLID: 52;

      assume ( LMP C) = ( E-max C);

      hence thesis by A1, SPRECT_1: 31;

    end;

    theorem :: JORDAN21:28

    for C be compact Subset of ( TOP-REAL 2) st p in (C /\ ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2))) holds (p `2 ) <= (( UMP C) `2 )

    proof

      let C be compact Subset of ( TOP-REAL 2) such that

       A1: p in (C /\ ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2)));

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

      then

       A2: (p `2 ) in ( proj2 .: (C /\ ( Vertical_Line ((( E-bound C) + ( W-bound C)) / 2)))) by A1, FUNCT_2: 35;

      (( UMP C) `2 ) = ( upper_bound ( proj2 .: (C /\ ( Vertical_Line ((( E-bound C) + ( W-bound C)) / 2))))) & ( proj2 .: (C /\ ( Vertical_Line ((( E-bound C) + ( W-bound C)) / 2)))) is non empty bounded_above by A1, Lm1, Th13, EUCLID: 52, RELAT_1: 119;

      hence thesis by A2, SEQ_4:def 1;

    end;

    theorem :: JORDAN21:29

    for C be compact Subset of ( TOP-REAL 2) st p in (C /\ ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2))) holds (( LMP C) `2 ) <= (p `2 )

    proof

      let C be compact Subset of ( TOP-REAL 2) such that

       A1: p in (C /\ ( Vertical_Line ((( W-bound C) + ( E-bound C)) / 2)));

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

      then

       A2: (p `2 ) in ( proj2 .: (C /\ ( Vertical_Line ((( E-bound C) + ( W-bound C)) / 2)))) by A1, FUNCT_2: 35;

      (( LMP C) `2 ) = ( lower_bound ( proj2 .: (C /\ ( Vertical_Line ((( E-bound C) + ( W-bound C)) / 2))))) & ( proj2 .: (C /\ ( Vertical_Line ((( E-bound C) + ( W-bound C)) / 2)))) is non empty bounded_below by A1, Lm1, Th13, EUCLID: 52, RELAT_1: 119;

      hence thesis by A2, SEQ_4:def 2;

    end;

    theorem :: JORDAN21:30

    

     Th30: ( UMP D) in D

    proof

      set w = ((( W-bound D) + ( E-bound D)) / 2);

      set X = (D /\ ( Vertical_Line w));

      D meets ( Vertical_Line w) by Def1;

      then

       A1: X is non empty;

      ( proj2 .: X) is closed & ( proj2 .: X) is bounded_above by Th13;

      then ( upper_bound ( proj2 .: X)) in ( proj2 .: X) by A1, Lm1, RCOMP_1: 12, RELAT_1: 119;

      then

      consider x be Point of ( TOP-REAL 2) such that

       A2: x in X and

       A3: ( upper_bound ( proj2 .: X)) = ( proj2 . x) by Lm2;

      x in ( Vertical_Line w) by A2, XBOOLE_0:def 4;

      

      then

       A4: (x `1 ) = w by JORDAN6: 31

      .= (( UMP D) `1 ) by EUCLID: 52;

      (x `2 ) = ( upper_bound ( proj2 .: X)) by A3, PSCOMP_1:def 6

      .= (( UMP D) `2 ) by EUCLID: 52;

      then x = ( UMP D) by A4, TOPREAL3: 6;

      hence thesis by A2, XBOOLE_0:def 4;

    end;

    theorem :: JORDAN21:31

    

     Th31: ( LMP D) in D

    proof

      set w = ((( W-bound D) + ( E-bound D)) / 2);

      set X = (D /\ ( Vertical_Line w));

      

       A1: ( proj2 .: X) is bounded_below by Th13;

      ( proj2 .: X) is non empty & ( proj2 .: X) is closed by Th12, Th13;

      then

      consider x be Point of ( TOP-REAL 2) such that

       A2: x in X and

       A3: ( lower_bound ( proj2 .: X)) = ( proj2 . x) by A1, Lm2, RCOMP_1: 13;

      x in ( Vertical_Line w) by A2, XBOOLE_0:def 4;

      

      then

       A4: (x `1 ) = w by JORDAN6: 31

      .= (( LMP D) `1 ) by EUCLID: 52;

      (x `2 ) = ( lower_bound ( proj2 .: X)) by A3, PSCOMP_1:def 6

      .= (( LMP D) `2 ) by EUCLID: 52;

      then x = ( LMP D) by A4, TOPREAL3: 6;

      hence thesis by A2, XBOOLE_0:def 4;

    end;

    theorem :: JORDAN21:32

    

     Th32: ( LSeg (( UMP P), |[((( W-bound P) + ( E-bound P)) / 2), ( N-bound P)]|)) is vertical

    proof

      set w = ((( W-bound P) + ( E-bound P)) / 2);

      ( |[w, ( N-bound P)]| `1 ) = w & (( UMP P) `1 ) = w by EUCLID: 52;

      hence thesis by SPPOL_1: 16;

    end;

    theorem :: JORDAN21:33

    

     Th33: ( LSeg (( LMP P), |[((( W-bound P) + ( E-bound P)) / 2), ( S-bound P)]|)) is vertical

    proof

      set w = ((( W-bound P) + ( E-bound P)) / 2);

      ( |[w, ( S-bound P)]| `1 ) = w & (( LMP P) `1 ) = w by EUCLID: 52;

      hence thesis by SPPOL_1: 16;

    end;

    theorem :: JORDAN21:34

    

     Th34: (( LSeg (( UMP D), |[((( W-bound D) + ( E-bound D)) / 2), ( N-bound D)]|)) /\ D) = {( UMP D)}

    proof

      set C = D;

      set w = ((( W-bound C) + ( E-bound C)) / 2);

      set L = ( LSeg (( UMP C), |[w, ( N-bound C)]|));

      set X = (C /\ ( Vertical_Line w));

      

       A1: ( UMP C) in C by Th30;

      

       A2: ( UMP C) in L by RLTOPSP1: 68;

      hereby

        let x be object;

        

         A3: (( UMP C) `1 ) = w by EUCLID: 52;

        assume

         A4: x in (L /\ C);

        then

         A5: x in L by XBOOLE_0:def 4;

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

        ( UMP C) in C by Th30;

        then ( |[w, ( N-bound C)]| `2 ) = ( N-bound C) & (( UMP C) `2 ) <= ( N-bound C) by EUCLID: 52, PSCOMP_1: 24;

        then

         A6: (( UMP C) `2 ) <= (y `2 ) by A5, TOPREAL1: 4;

        

         A7: ( proj2 .: X) is bounded_above by Th13;

        

         A8: (( UMP C) `2 ) = ( upper_bound ( proj2 .: X)) by EUCLID: 52;

        

         A9: x in C by A4, XBOOLE_0:def 4;

        L is vertical by Th32;

        then

         A10: (y `1 ) = w by A2, A5, A3, SPPOL_1:def 3;

        then y in ( Vertical_Line w) by JORDAN6: 31;

        then (y `2 ) = ( proj2 . y) & y in X by A9, PSCOMP_1:def 6, XBOOLE_0:def 4;

        then (y `2 ) in ( proj2 .: X) by FUNCT_2: 35;

        then (y `2 ) <= ( upper_bound ( proj2 .: X)) by A7, SEQ_4:def 1;

        then (y `2 ) = ( upper_bound ( proj2 .: X)) by A8, A6, XXREAL_0: 1;

        then y = ( UMP C) by A3, A8, A10, TOPREAL3: 6;

        hence x in {( UMP C)} by TARSKI:def 1;

      end;

      let x be object;

      assume x in {( UMP C)};

      then x = ( UMP C) by TARSKI:def 1;

      hence thesis by A2, A1, XBOOLE_0:def 4;

    end;

    theorem :: JORDAN21:35

    

     Th35: (( LSeg (( LMP D), |[((( W-bound D) + ( E-bound D)) / 2), ( S-bound D)]|)) /\ D) = {( LMP D)}

    proof

      set C = D;

      set w = ((( W-bound C) + ( E-bound C)) / 2);

      set L = ( LSeg (( LMP C), |[w, ( S-bound C)]|));

      set X = (C /\ ( Vertical_Line w));

      

       A1: ( LMP C) in C by Th31;

      

       A2: ( LMP C) in L by RLTOPSP1: 68;

      hereby

        let x be object;

        

         A3: (( LMP C) `1 ) = w by EUCLID: 52;

        assume

         A4: x in (L /\ C);

        then

         A5: x in L by XBOOLE_0:def 4;

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

        ( LMP C) in C by Th31;

        then ( |[w, ( S-bound C)]| `2 ) = ( S-bound C) & (( LMP C) `2 ) >= ( S-bound C) by EUCLID: 52, PSCOMP_1: 24;

        then

         A6: (( LMP C) `2 ) >= (y `2 ) by A5, TOPREAL1: 4;

        

         A7: ( proj2 .: X) is bounded_below by Th13;

        

         A8: (( LMP C) `2 ) = ( lower_bound ( proj2 .: X)) by EUCLID: 52;

        

         A9: x in C by A4, XBOOLE_0:def 4;

        L is vertical by Th33;

        then

         A10: (y `1 ) = w by A2, A5, A3, SPPOL_1:def 3;

        then y in ( Vertical_Line w) by JORDAN6: 31;

        then (y `2 ) = ( proj2 . y) & y in X by A9, PSCOMP_1:def 6, XBOOLE_0:def 4;

        then (y `2 ) in ( proj2 .: X) by FUNCT_2: 35;

        then (y `2 ) >= ( lower_bound ( proj2 .: X)) by A7, SEQ_4:def 2;

        then (y `2 ) = ( lower_bound ( proj2 .: X)) by A8, A6, XXREAL_0: 1;

        then y = ( LMP C) by A3, A8, A10, TOPREAL3: 6;

        hence x in {( LMP C)} by TARSKI:def 1;

      end;

      let x be object;

      assume x in {( LMP C)};

      then x = ( LMP C) by TARSKI:def 1;

      hence thesis by A2, A1, XBOOLE_0:def 4;

    end;

    theorem :: JORDAN21:36

    

     Th36: (( LMP C) `2 ) < (( UMP C) `2 )

    proof

      set w = ((( E-bound C) + ( W-bound C)) / 2);

      set X = (C /\ ( Vertical_Line w));

      

       A1: (( UMP C) `2 ) = ( upper_bound ( proj2 .: X)) & (( LMP C) `2 ) = ( lower_bound ( proj2 .: X)) by EUCLID: 52;

      set u = ( Upper_Middle_Point C), l = ( Lower_Middle_Point C);

      

       A2: (l `2 ) = ( proj2 . l) by PSCOMP_1:def 6;

      (l `1 ) = w by JORDAN6: 64;

      then

       A3: l in ( Vertical_Line w) by JORDAN6: 31;

      l in C by Th14;

      then l in X by A3, XBOOLE_0:def 4;

      then

       A4: (l `2 ) in ( proj2 .: X) by A2, FUNCT_2: 35;

      X is bounded by TOPREAL6: 89;

      then

       A5: ( proj2 .: X) is real-bounded by JCT_MISC: 14;

      (u `1 ) = w by JORDAN6: 65;

      then u in C & u in ( Vertical_Line w) by JORDAN6: 31, JORDAN6: 68;

      then

       A6: u in X by XBOOLE_0:def 4;

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

      then

       A7: (u `2 ) in ( proj2 .: X) by A6, FUNCT_2: 35;

      (u `2 ) <> (l `2 ) by Th15;

      hence thesis by A1, A5, A7, A4, SEQ_4: 12;

    end;

    theorem :: JORDAN21:37

    

     Th37: ( UMP C) <> ( LMP C)

    proof

      assume

       A1: ( UMP C) = ( LMP C);

      (( LMP C) `2 ) < (( UMP C) `2 ) by Th36;

      hence contradiction by A1;

    end;

    theorem :: JORDAN21:38

    

     Th38: ( S-bound C) < (( UMP C) `2 )

    proof

      set u = ( UMP C), l = ( LMP C);

       A1:

      now

        assume

         A2: ( S-bound C) = (u `2 );

        (l `2 ) < (u `2 ) & l in C by Th31, Th36;

        hence contradiction by A2, PSCOMP_1: 24;

      end;

      u in C by Th30;

      then ( S-bound C) <= (u `2 ) by PSCOMP_1: 24;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: JORDAN21:39

    

     Th39: (( UMP C) `2 ) <= ( N-bound C)

    proof

      ( UMP C) in C by Th30;

      hence thesis by PSCOMP_1: 24;

    end;

    theorem :: JORDAN21:40

    

     Th40: ( S-bound C) <= (( LMP C) `2 )

    proof

      ( LMP C) in C by Th31;

      hence thesis by PSCOMP_1: 24;

    end;

    theorem :: JORDAN21:41

    

     Th41: (( LMP C) `2 ) < ( N-bound C)

    proof

      set u = ( UMP C), l = ( LMP C);

       A1:

      now

        assume

         A2: ( N-bound C) = (l `2 );

        (l `2 ) < (u `2 ) & u in C by Th30, Th36;

        hence contradiction by A2, PSCOMP_1: 24;

      end;

      l in C by Th31;

      then (l `2 ) <= ( N-bound C) by PSCOMP_1: 24;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: JORDAN21:42

    

     Th42: ( LSeg (( UMP C), |[((( W-bound C) + ( E-bound C)) / 2), ( N-bound C)]|)) misses ( LSeg (( LMP C), |[((( W-bound C) + ( E-bound C)) / 2), ( S-bound C)]|))

    proof

      set w = ((( W-bound C) + ( E-bound C)) / 2);

      assume ( LSeg (( UMP C), |[w, ( N-bound C)]|)) meets ( LSeg (( LMP C), |[w, ( S-bound C)]|));

      then

      consider x be object such that

       A1: x in ( LSeg (( UMP C), |[w, ( N-bound C)]|)) and

       A2: x in ( LSeg (( LMP C), |[w, ( S-bound C)]|)) by XBOOLE_0: 3;

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

      ( |[w, ( N-bound C)]| `2 ) = ( N-bound C) by EUCLID: 52;

      then (( UMP C) `2 ) <= ( |[w, ( N-bound C)]| `2 ) by Th39;

      then

       A3: (x `2 ) >= (( UMP C) `2 ) by A1, TOPREAL1: 4;

      ( |[w, ( S-bound C)]| `2 ) = ( S-bound C) by EUCLID: 52;

      then ( |[w, ( S-bound C)]| `2 ) <= (( LMP C) `2 ) by Th40;

      then (x `2 ) <= (( LMP C) `2 ) by A2, TOPREAL1: 4;

      hence contradiction by A3, Th36, XXREAL_0: 2;

    end;

    theorem :: JORDAN21:43

    for A,B be Subset of ( TOP-REAL 2) st A c= B & (( W-bound A) + ( E-bound A)) = (( W-bound B) + ( E-bound B)) & (A /\ ( Vertical_Line ((( W-bound A) + ( E-bound A)) / 2))) is non empty & ( proj2 .: (B /\ ( Vertical_Line ((( W-bound A) + ( E-bound A)) / 2)))) is bounded_above holds (( UMP A) `2 ) <= (( UMP B) `2 )

    proof

      let A,B be Subset of ( TOP-REAL 2);

      assume that

       A1: A c= B and

       A2: (( W-bound A) + ( E-bound A)) = (( W-bound B) + ( E-bound B)) and

       A3: (A /\ ( Vertical_Line ((( W-bound A) + ( E-bound A)) / 2))) is non empty and

       A4: ( proj2 .: (B /\ ( Vertical_Line ((( W-bound A) + ( E-bound A)) / 2)))) is bounded_above;

      set w = ((( W-bound A) + ( E-bound A)) / 2);

      ( proj2 .: (A /\ ( Vertical_Line w))) is non empty & (A /\ ( Vertical_Line w)) c= (B /\ ( Vertical_Line w)) by A1, A3, Lm1, RELAT_1: 119, XBOOLE_1: 26;

      then ( upper_bound ( proj2 .: (A /\ ( Vertical_Line w)))) <= ( upper_bound ( proj2 .: (B /\ ( Vertical_Line w)))) by A4, RELAT_1: 123, SEQ_4: 48;

      then (( UMP A) `2 ) <= ( upper_bound ( proj2 .: (B /\ ( Vertical_Line w)))) by EUCLID: 52;

      hence thesis by A2, EUCLID: 52;

    end;

    theorem :: JORDAN21:44

    for A,B be Subset of ( TOP-REAL 2) st A c= B & (( W-bound A) + ( E-bound A)) = (( W-bound B) + ( E-bound B)) & (A /\ ( Vertical_Line ((( W-bound A) + ( E-bound A)) / 2))) is non empty & ( proj2 .: (B /\ ( Vertical_Line ((( W-bound A) + ( E-bound A)) / 2)))) is bounded_below holds (( LMP B) `2 ) <= (( LMP A) `2 )

    proof

      let A,B be Subset of ( TOP-REAL 2);

      assume that

       A1: A c= B and

       A2: (( W-bound A) + ( E-bound A)) = (( W-bound B) + ( E-bound B)) and

       A3: (A /\ ( Vertical_Line ((( W-bound A) + ( E-bound A)) / 2))) is non empty and

       A4: ( proj2 .: (B /\ ( Vertical_Line ((( W-bound A) + ( E-bound A)) / 2)))) is bounded_below;

      set w = ((( W-bound A) + ( E-bound A)) / 2);

      ( proj2 .: (A /\ ( Vertical_Line w))) is non empty & (A /\ ( Vertical_Line w)) c= (B /\ ( Vertical_Line w)) by A1, A3, Lm1, RELAT_1: 119, XBOOLE_1: 26;

      then ( lower_bound ( proj2 .: (A /\ ( Vertical_Line w)))) >= ( lower_bound ( proj2 .: (B /\ ( Vertical_Line w)))) by A4, RELAT_1: 123, SEQ_4: 47;

      then (( LMP A) `2 ) >= ( lower_bound ( proj2 .: (B /\ ( Vertical_Line w)))) by EUCLID: 52;

      hence thesis by A2, EUCLID: 52;

    end;

    theorem :: JORDAN21:45

    for A,B be Subset of ( TOP-REAL 2) st A c= B & ( UMP B) in A & (A /\ ( Vertical_Line ((( W-bound A) + ( E-bound A)) / 2))) is non empty & ( proj2 .: (B /\ ( Vertical_Line ((( W-bound B) + ( E-bound B)) / 2)))) is bounded_above & (( W-bound A) + ( E-bound A)) = (( W-bound B) + ( E-bound B)) holds ( UMP A) = ( UMP B)

    proof

      let A,B be Subset of ( TOP-REAL 2) such that

       A1: A c= B and

       A2: ( UMP B) in A and

       A3: (A /\ ( Vertical_Line ((( W-bound A) + ( E-bound A)) / 2))) is non empty and

       A4: ( proj2 .: (B /\ ( Vertical_Line ((( W-bound B) + ( E-bound B)) / 2)))) is bounded_above and

       A5: (( W-bound A) + ( E-bound A)) = (( W-bound B) + ( E-bound B));

      set w = ((( W-bound A) + ( E-bound A)) / 2);

      

       A6: (( UMP A) `2 ) = ( upper_bound ( proj2 .: (A /\ ( Vertical_Line w)))) & ( proj2 .: (A /\ ( Vertical_Line w))) is non empty by A3, Lm1, EUCLID: 52, RELAT_1: 119;

      

       A7: (( UMP B) `1 ) = w by A5, EUCLID: 52;

      

       A8: for s be Real st 0 < s holds ex r be Real st r in ( proj2 .: (A /\ ( Vertical_Line w))) & ((( UMP B) `2 ) - s) < r

      proof

        let s be Real;

        assume

         A9: 0 < s;

        take (( UMP B) `2 );

        ( UMP B) in ( Vertical_Line w) by A7, JORDAN6: 31;

        then ( proj2 . ( UMP B)) = (( UMP B) `2 ) & ( UMP B) in (A /\ ( Vertical_Line w)) by A2, PSCOMP_1:def 6, XBOOLE_0:def 4;

        hence (( UMP B) `2 ) in ( proj2 .: (A /\ ( Vertical_Line w))) by FUNCT_2: 35;

        ((( UMP B) `2 ) - s) < ((( UMP B) `2 ) - 0 ) by A9, XREAL_1: 15;

        hence thesis;

      end;

      

       A10: (A /\ ( Vertical_Line w)) c= (B /\ ( Vertical_Line w)) by A1, XBOOLE_1: 26;

      then

       A11: ( proj2 .: (A /\ ( Vertical_Line w))) c= ( proj2 .: (B /\ ( Vertical_Line w))) by RELAT_1: 123;

      (( UMP B) `2 ) = ( upper_bound ( proj2 .: (B /\ ( Vertical_Line w)))) by A5, EUCLID: 52;

      then

       A12: for r be Real st r in ( proj2 .: (A /\ ( Vertical_Line w))) holds (( UMP B) `2 ) >= r by A4, A5, A11, SEQ_4:def 1;

      ( proj2 .: (A /\ ( Vertical_Line w))) is bounded_above by A4, A5, A10, RELAT_1: 123, XXREAL_2: 43;

      then (( UMP A) `1 ) = w & (( UMP A) `2 ) = (( UMP B) `2 ) by A6, A12, A8, EUCLID: 52, SEQ_4:def 1;

      hence thesis by A7, TOPREAL3: 6;

    end;

    theorem :: JORDAN21:46

    for A,B be Subset of ( TOP-REAL 2) st A c= B & ( LMP B) in A & (A /\ ( Vertical_Line ((( W-bound A) + ( E-bound A)) / 2))) is non empty & ( proj2 .: (B /\ ( Vertical_Line ((( W-bound B) + ( E-bound B)) / 2)))) is bounded_below & (( W-bound A) + ( E-bound A)) = (( W-bound B) + ( E-bound B)) holds ( LMP A) = ( LMP B)

    proof

      let A,B be Subset of ( TOP-REAL 2) such that

       A1: A c= B and

       A2: ( LMP B) in A and

       A3: (A /\ ( Vertical_Line ((( W-bound A) + ( E-bound A)) / 2))) is non empty and

       A4: ( proj2 .: (B /\ ( Vertical_Line ((( W-bound B) + ( E-bound B)) / 2)))) is bounded_below and

       A5: (( W-bound A) + ( E-bound A)) = (( W-bound B) + ( E-bound B));

      set w = ((( W-bound A) + ( E-bound A)) / 2);

      

       A6: (( LMP A) `2 ) = ( lower_bound ( proj2 .: (A /\ ( Vertical_Line w)))) & ( proj2 .: (A /\ ( Vertical_Line w))) is non empty by A3, Lm1, EUCLID: 52, RELAT_1: 119;

      

       A7: (( LMP B) `1 ) = w by A5, EUCLID: 52;

      

       A8: for s be Real st 0 < s holds ex r be Real st r in ( proj2 .: (A /\ ( Vertical_Line w))) & r < ((( LMP B) `2 ) + s)

      proof

        let s be Real;

        assume

         A9: 0 < s;

        take (( LMP B) `2 );

        ( LMP B) in ( Vertical_Line w) by A7, JORDAN6: 31;

        then ( proj2 . ( LMP B)) = (( LMP B) `2 ) & ( LMP B) in (A /\ ( Vertical_Line w)) by A2, PSCOMP_1:def 6, XBOOLE_0:def 4;

        hence (( LMP B) `2 ) in ( proj2 .: (A /\ ( Vertical_Line w))) by FUNCT_2: 35;

        ((( LMP B) `2 ) + 0 ) < ((( LMP B) `2 ) + s) by A9, XREAL_1: 6;

        hence thesis;

      end;

      

       A10: (A /\ ( Vertical_Line w)) c= (B /\ ( Vertical_Line w)) by A1, XBOOLE_1: 26;

      then

       A11: ( proj2 .: (A /\ ( Vertical_Line w))) c= ( proj2 .: (B /\ ( Vertical_Line w))) by RELAT_1: 123;

      (( LMP B) `2 ) = ( lower_bound ( proj2 .: (B /\ ( Vertical_Line w)))) by A5, EUCLID: 52;

      then

       A12: for r be Real st r in ( proj2 .: (A /\ ( Vertical_Line w))) holds (( LMP B) `2 ) <= r by A4, A5, A11, SEQ_4:def 2;

      ( proj2 .: (A /\ ( Vertical_Line w))) is bounded_below by A4, A5, A10, RELAT_1: 123, XXREAL_2: 44;

      then (( LMP A) `1 ) = w & (( LMP A) `2 ) = (( LMP B) `2 ) by A6, A12, A8, EUCLID: 52, SEQ_4:def 2;

      hence thesis by A7, TOPREAL3: 6;

    end;

    theorem :: JORDAN21:47

    (( UMP ( Upper_Arc C)) `2 ) <= ( N-bound C)

    proof

      set w = ((( E-bound C) + ( W-bound C)) / 2);

      

       A1: (( Upper_Arc C) /\ ( Vertical_Line w)) c= (C /\ ( Vertical_Line w)) by JORDAN6: 61, XBOOLE_1: 26;

      ( proj2 .: (( Upper_Arc C) /\ ( Vertical_Line w))) is non empty & ( proj2 .: (C /\ ( Vertical_Line w))) is bounded_above by Th13, Th21;

      then

       A2: ( upper_bound ( proj2 .: (( Upper_Arc C) /\ ( Vertical_Line w)))) <= ( upper_bound ( proj2 .: (C /\ ( Vertical_Line w)))) by A1, RELAT_1: 123, SEQ_4: 48;

      ( W-bound C) = ( W-bound ( Upper_Arc C)) & ( E-bound C) = ( E-bound ( Upper_Arc C)) by Th17, Th18;

      then

       A3: (( UMP ( Upper_Arc C)) `2 ) = ( upper_bound ( proj2 .: (( Upper_Arc C) /\ ( Vertical_Line w)))) by EUCLID: 52;

      (( UMP C) `2 ) = ( upper_bound ( proj2 .: (C /\ ( Vertical_Line w)))) & (( UMP C) `2 ) <= ( N-bound C) by Th39, EUCLID: 52;

      hence thesis by A2, A3, XXREAL_0: 2;

    end;

    theorem :: JORDAN21:48

    ( S-bound C) <= (( LMP ( Lower_Arc C)) `2 )

    proof

      set w = ((( E-bound C) + ( W-bound C)) / 2);

      

       A1: (( Lower_Arc C) /\ ( Vertical_Line w)) c= (C /\ ( Vertical_Line w)) by JORDAN6: 61, XBOOLE_1: 26;

      ( proj2 .: (( Lower_Arc C) /\ ( Vertical_Line w))) is non empty & ( proj2 .: (C /\ ( Vertical_Line w))) is bounded_below by Th13, Th22;

      then

       A2: ( lower_bound ( proj2 .: (( Lower_Arc C) /\ ( Vertical_Line w)))) >= ( lower_bound ( proj2 .: (C /\ ( Vertical_Line w)))) by A1, RELAT_1: 123, SEQ_4: 47;

      ( W-bound C) = ( W-bound ( Lower_Arc C)) & ( E-bound C) = ( E-bound ( Lower_Arc C)) by Th19, Th20;

      then

       A3: (( LMP ( Lower_Arc C)) `2 ) = ( lower_bound ( proj2 .: (( Lower_Arc C) /\ ( Vertical_Line w)))) by EUCLID: 52;

      (( LMP C) `2 ) = ( lower_bound ( proj2 .: (C /\ ( Vertical_Line w)))) & ( S-bound C) <= (( LMP C) `2 ) by Th40, EUCLID: 52;

      hence thesis by A2, A3, XXREAL_0: 2;

    end;

    theorem :: JORDAN21:49

     not (( LMP C) in ( Lower_Arc C) & ( UMP C) in ( Lower_Arc C))

    proof

      assume that

       A1: ( LMP C) in ( Lower_Arc C) and

       A2: ( UMP C) in ( Lower_Arc C);

      

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

      set n = |[((( W-bound C) + ( E-bound C)) / 2), ( N-bound C)]|;

      set S1 = ( LSeg (n,( UMP C)));

      

       A4: ( Lower_Arc C) c= C by JORDAN6: 61;

      

       A5: (n `2 ) = ( N-bound C) by EUCLID: 52;

      set s = |[((( W-bound C) + ( E-bound C)) / 2), ( S-bound C)]|;

      set S2 = ( LSeg (( LMP C),s));

      

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

      

       A7: (( W-min C) `1 ) = ( W-bound C) & (( E-max C) `1 ) = ( E-bound C) by EUCLID: 52;

      

       A8: ( Upper_Arc C) c= C by JORDAN6: 61;

      then

       A9: for p be Point of ( TOP-REAL 2) st p in ( Upper_Arc C) holds (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A7, PSCOMP_1: 24;

      

       A10: ( UMP C) <> ( E-max C) by Th25;

      

       A11: ( UMP C) <> ( W-min C) by Th24;

       A12:

      now

        assume ( UMP C) in ( Upper_Arc C);

        then ( UMP C) in (( Upper_Arc C) /\ ( Lower_Arc C)) by A2, XBOOLE_0:def 4;

        hence contradiction by A11, A10, A3, TARSKI:def 2;

      end;

      

       A13: ( W-bound C) < ( E-bound C) by SPRECT_1: 31;

      

       A14: ( Upper_Arc C) misses S1

      proof

        

         A15: (S1 /\ C) = {( UMP C)} by Th34;

        assume ( Upper_Arc C) meets S1;

        then

        consider x be object such that

         A16: x in ( Upper_Arc C) and

         A17: x in S1 by XBOOLE_0: 3;

        x in (S1 /\ C) by A8, A16, A17, XBOOLE_0:def 4;

        then

         A18: x = ( UMP C) by A15, TARSKI:def 1;

        then x in (( Lower_Arc C) /\ ( Upper_Arc C)) by A2, A16, XBOOLE_0:def 4;

        hence contradiction by A11, A10, A3, A18, TARSKI:def 2;

      end;

      

       A19: ( UMP C) in C & ( LMP C) in C by Th30, Th31;

      

       A20: (( UMP C) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by EUCLID: 52;

      (n `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by EUCLID: 52;

      then

       A21: S1 is vertical by A20, SPPOL_1: 16;

      

       A22: ( UMP C) in S1 by RLTOPSP1: 68;

      

       A23: ( LMP C) <> ( E-max C) by Th27;

      

       A24: ( LMP C) <> ( W-min C) by Th26;

       A25:

      now

        assume ( LMP C) in ( Upper_Arc C);

        then ( LMP C) in (( Upper_Arc C) /\ ( Lower_Arc C)) by A1, XBOOLE_0:def 4;

        hence contradiction by A24, A23, A3, TARSKI:def 2;

      end;

      

       A26: ( LMP C) <> ( UMP C) by Th37;

      

       A27: (( LMP C) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by EUCLID: 52;

      

       A28: ( Upper_Arc C) misses S2

      proof

        

         A29: (S2 /\ C) = {( LMP C)} by Th35;

        assume ( Upper_Arc C) meets S2;

        then

        consider x be object such that

         A30: x in ( Upper_Arc C) and

         A31: x in S2 by XBOOLE_0: 3;

        x in (S2 /\ C) by A8, A30, A31, XBOOLE_0:def 4;

        then

         A32: x = ( LMP C) by A29, TARSKI:def 1;

        then x in (( Lower_Arc C) /\ ( Upper_Arc C)) by A1, A30, XBOOLE_0:def 4;

        hence contradiction by A24, A23, A3, A32, TARSKI:def 2;

      end;

      (s `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by EUCLID: 52;

      then

       A33: S2 is vertical by A27, SPPOL_1: 16;

      

       A34: ( LMP C) in S2 by RLTOPSP1: 68;

      

       A35: S1 misses S2 by Th42;

      

       A36: (s `2 ) = ( S-bound C) by EUCLID: 52;

      then

       A37: ( Upper_Arc C) is_an_arc_of (( W-min C),( E-max C)) & for p be Point of ( TOP-REAL 2) st p in ( Upper_Arc C) holds (s `2 ) <= (p `2 ) & (p `2 ) <= (n `2 ) by A8, A5, JORDAN6:def 8, PSCOMP_1: 24;

      per cases by A19, JORDAN16: 7;

        suppose

         A38: LE (( LMP C),( UMP C),C);

        set S = ( Segment (( Lower_Arc C),( E-max C),( W-min C),( LMP C),( UMP C)));

        

         A39: S c= ( Lower_Arc C) by JORDAN16: 2;

        then

         A40: S c= C by A4;

         A41:

        now

          let p be Point of ( TOP-REAL 2);

          assume

           A42: p in ((S1 \/ S) \/ S2);

          per cases by A42, Lm3;

            suppose p in S1;

            then (p `1 ) = (( UMP C) `1 ) by A21, A22, SPPOL_1:def 3;

            hence (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A20, A7, A13, XREAL_1: 226;

          end;

            suppose p in S;

            hence (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A7, A40, PSCOMP_1: 24;

          end;

            suppose p in S2;

            then (p `1 ) = (( LMP C) `1 ) by A33, A34, SPPOL_1:def 3;

            hence (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A27, A7, A13, XREAL_1: 226;

          end;

        end;

         A43:

        now

          let p be Point of ( TOP-REAL 2);

          assume

           A44: p in ((S1 \/ S) \/ S2);

          per cases by A44, Lm3;

            suppose

             A45: p in S1;

            

             A46: (s `2 ) <= (( UMP C) `2 ) by A36, Th38;

            

             A47: (( UMP C) `2 ) <= (n `2 ) by A5, Th39;

            then (( UMP C) `2 ) <= (p `2 ) by A45, TOPREAL1: 4;

            hence (s `2 ) <= (p `2 ) & (p `2 ) <= (n `2 ) by A45, A47, A46, TOPREAL1: 4, XXREAL_0: 2;

          end;

            suppose p in S;

            hence (s `2 ) <= (p `2 ) & (p `2 ) <= (n `2 ) by A36, A5, A40, PSCOMP_1: 24;

          end;

            suppose

             A48: p in S2;

            

             A49: (s `2 ) <= (( LMP C) `2 ) by A36, Th40;

            hence (s `2 ) <= (p `2 ) by A48, TOPREAL1: 4;

            (p `2 ) <= (( LMP C) `2 ) by A48, A49, TOPREAL1: 4;

            hence (p `2 ) <= (n `2 ) by A5, Th41, XXREAL_0: 2;

          end;

        end;

        

         A50: S c= (( Lower_Arc C) \ {( W-min C), ( E-max C)})

        proof

          let s be object;

          assume

           A51: s in S;

          now

            assume s in {( W-min C), ( E-max C)};

            then s = ( W-min C) or s = ( E-max C) by TARSKI:def 2;

            hence contradiction by A11, A23, A6, A51, Th11;

          end;

          hence thesis by A39, A51, XBOOLE_0:def 5;

        end;

        ( Upper_Arc C) misses S

        proof

          assume ( Upper_Arc C) meets S;

          then

          consider x be object such that

           A52: x in ( Upper_Arc C) and

           A53: x in S by XBOOLE_0: 3;

          x in ( Lower_Arc C) by A50, A53, XBOOLE_0:def 5;

          then x in (( Lower_Arc C) /\ ( Upper_Arc C)) by A52, XBOOLE_0:def 4;

          hence contradiction by A3, A50, A53, XBOOLE_0:def 5;

        end;

        then

         A54: ( Upper_Arc C) misses ((S1 \/ S) \/ S2) by A14, A28, Lm4;

        

         A55: LE (( LMP C),( UMP C),( Lower_Arc C),( E-max C),( W-min C)) by A25, A38, JORDAN6:def 10;

        then

         A56: ( UMP C) in S by JORDAN16: 5;

        

         A57: (S1 /\ S) = {( UMP C)}

        proof

          (S1 /\ C) = {( UMP C)} by Th34;

          hence (S1 /\ S) c= {( UMP C)} by A40, XBOOLE_1: 26;

          let x be object;

          assume x in {( UMP C)};

          then

           A58: x = ( UMP C) by TARSKI:def 1;

          ( UMP C) in S1 by RLTOPSP1: 68;

          hence thesis by A56, A58, XBOOLE_0:def 4;

        end;

        

         A59: ( LMP C) in S by A55, JORDAN16: 5;

        

         A60: (S2 /\ S) = {( LMP C)}

        proof

          (S2 /\ C) = {( LMP C)} by Th35;

          hence (S2 /\ S) c= {( LMP C)} by A40, XBOOLE_1: 26;

          let x be object;

          assume x in {( LMP C)};

          then x = ( LMP C) by TARSKI:def 1;

          hence thesis by A34, A59, XBOOLE_0:def 4;

        end;

        S is_an_arc_of (( LMP C),( UMP C)) by A26, A6, A55, JORDAN16: 21;

        then S is_an_arc_of (( UMP C),( LMP C)) by JORDAN5B: 14;

        then

         A61: (S1 \/ S) is_an_arc_of (n,( LMP C)) by A57, TOPREAL1: 11;

        ((S1 \/ S) /\ S2) = ((S1 /\ S2) \/ (S /\ S2)) by XBOOLE_1: 23

        .= ( {} \/ (S /\ S2)) by A35;

        then ((S1 \/ S) \/ S2) is_an_arc_of (n,s) by A60, A61, TOPREAL1: 10;

        then ((S1 \/ S) \/ S2) is_an_arc_of (s,n) by JORDAN5B: 14;

        hence thesis by A37, A9, A54, A43, A41, JGRAPH_1: 44;

      end;

        suppose

         A62: LE (( UMP C),( LMP C),C);

        set S = ( Segment (( Lower_Arc C),( E-max C),( W-min C),( UMP C),( LMP C)));

        

         A63: S c= ( Lower_Arc C) by JORDAN16: 2;

        then

         A64: S c= C by A4;

         A65:

        now

          let p be Point of ( TOP-REAL 2);

          assume

           A66: p in ((S1 \/ S) \/ S2);

          per cases by A66, Lm3;

            suppose p in S1;

            then (p `1 ) = (( UMP C) `1 ) by A21, A22, SPPOL_1:def 3;

            hence (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A20, A7, A13, XREAL_1: 226;

          end;

            suppose p in S;

            hence (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A7, A64, PSCOMP_1: 24;

          end;

            suppose p in S2;

            then (p `1 ) = (( LMP C) `1 ) by A33, A34, SPPOL_1:def 3;

            hence (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A27, A7, A13, XREAL_1: 226;

          end;

        end;

         A67:

        now

          let p be Point of ( TOP-REAL 2);

          assume

           A68: p in ((S1 \/ S) \/ S2);

          per cases by A68, Lm3;

            suppose

             A69: p in S1;

            

             A70: (s `2 ) <= (( UMP C) `2 ) by A36, Th38;

            

             A71: (( UMP C) `2 ) <= (n `2 ) by A5, Th39;

            then (( UMP C) `2 ) <= (p `2 ) by A69, TOPREAL1: 4;

            hence (s `2 ) <= (p `2 ) & (p `2 ) <= (n `2 ) by A69, A71, A70, TOPREAL1: 4, XXREAL_0: 2;

          end;

            suppose p in S;

            hence (s `2 ) <= (p `2 ) & (p `2 ) <= (n `2 ) by A36, A5, A64, PSCOMP_1: 24;

          end;

            suppose

             A72: p in S2;

            

             A73: (s `2 ) <= (( LMP C) `2 ) by A36, Th40;

            hence (s `2 ) <= (p `2 ) by A72, TOPREAL1: 4;

            (p `2 ) <= (( LMP C) `2 ) by A72, A73, TOPREAL1: 4;

            hence (p `2 ) <= (n `2 ) by A5, Th41, XXREAL_0: 2;

          end;

        end;

        

         A74: S c= (( Lower_Arc C) \ {( W-min C), ( E-max C)})

        proof

          let s be object;

          assume

           A75: s in S;

          now

            assume s in {( W-min C), ( E-max C)};

            then s = ( W-min C) or s = ( E-max C) by TARSKI:def 2;

            hence contradiction by A10, A24, A6, A75, Th11;

          end;

          hence thesis by A63, A75, XBOOLE_0:def 5;

        end;

        ( Upper_Arc C) misses S

        proof

          assume ( Upper_Arc C) meets S;

          then

          consider x be object such that

           A76: x in ( Upper_Arc C) and

           A77: x in S by XBOOLE_0: 3;

          x in ( Lower_Arc C) by A74, A77, XBOOLE_0:def 5;

          then x in (( Lower_Arc C) /\ ( Upper_Arc C)) by A76, XBOOLE_0:def 4;

          hence contradiction by A3, A74, A77, XBOOLE_0:def 5;

        end;

        then

         A78: ( Upper_Arc C) misses ((S1 \/ S) \/ S2) by A14, A28, Lm4;

        

         A79: LE (( UMP C),( LMP C),( Lower_Arc C),( E-max C),( W-min C)) by A12, A62, JORDAN6:def 10;

        then

         A80: ( UMP C) in S by JORDAN16: 5;

        

         A81: (S1 /\ S) = {( UMP C)}

        proof

          (S1 /\ C) = {( UMP C)} by Th34;

          hence (S1 /\ S) c= {( UMP C)} by A64, XBOOLE_1: 26;

          let x be object;

          assume x in {( UMP C)};

          then

           A82: x = ( UMP C) by TARSKI:def 1;

          ( UMP C) in S1 by RLTOPSP1: 68;

          hence thesis by A80, A82, XBOOLE_0:def 4;

        end;

        

         A83: ( LMP C) in S by A79, JORDAN16: 5;

        

         A84: (S2 /\ S) = {( LMP C)}

        proof

          (S2 /\ C) = {( LMP C)} by Th35;

          hence (S2 /\ S) c= {( LMP C)} by A64, XBOOLE_1: 26;

          let x be object;

          assume x in {( LMP C)};

          then x = ( LMP C) by TARSKI:def 1;

          hence thesis by A34, A83, XBOOLE_0:def 4;

        end;

        S is_an_arc_of (( UMP C),( LMP C)) by A6, A79, Th37, JORDAN16: 21;

        then

         A85: (S1 \/ S) is_an_arc_of (n,( LMP C)) by A81, TOPREAL1: 11;

        ((S1 \/ S) /\ S2) = ((S1 /\ S2) \/ (S /\ S2)) by XBOOLE_1: 23

        .= ( {} \/ (S /\ S2)) by A35;

        then ((S1 \/ S) \/ S2) is_an_arc_of (n,s) by A84, A85, TOPREAL1: 10;

        then ((S1 \/ S) \/ S2) is_an_arc_of (s,n) by JORDAN5B: 14;

        hence thesis by A37, A9, A78, A67, A65, JGRAPH_1: 44;

      end;

    end;

    theorem :: JORDAN21:50

     not (( LMP C) in ( Upper_Arc C) & ( UMP C) in ( Upper_Arc C))

    proof

      assume that

       A1: ( LMP C) in ( Upper_Arc C) and

       A2: ( UMP C) in ( Upper_Arc C);

      

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

      set s = |[((( W-bound C) + ( E-bound C)) / 2), ( S-bound C)]|;

      set S2 = ( LSeg (( LMP C),s));

      

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

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

      then

       A5: ( Lower_Arc C) is_an_arc_of (( W-min C),( E-max C)) by JORDAN5B: 14;

      

       A6: ( UMP C) in C & ( LMP C) in C by Th30, Th31;

      

       A7: (( UMP C) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by EUCLID: 52;

      set n = |[((( W-bound C) + ( E-bound C)) / 2), ( N-bound C)]|;

      set S1 = ( LSeg (n,( UMP C)));

      

       A8: ( Upper_Arc C) c= C by JORDAN6: 61;

      

       A9: (n `2 ) = ( N-bound C) by EUCLID: 52;

      (n `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by EUCLID: 52;

      then

       A10: S1 is vertical by A7, SPPOL_1: 16;

      

       A11: S1 misses S2 by Th42;

      

       A12: ( UMP C) in S1 by RLTOPSP1: 68;

      

       A13: (( W-min C) `1 ) = ( W-bound C) & (( E-max C) `1 ) = ( E-bound C) by EUCLID: 52;

      

       A14: ( Lower_Arc C) c= C by JORDAN6: 61;

      then

       A15: for p be Point of ( TOP-REAL 2) st p in ( Lower_Arc C) holds (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A13, PSCOMP_1: 24;

      

       A16: ( UMP C) <> ( E-max C) by Th25;

      

       A17: ( UMP C) <> ( W-min C) by Th24;

       A18:

      now

        assume ( UMP C) in ( Lower_Arc C);

        then ( UMP C) in (( Upper_Arc C) /\ ( Lower_Arc C)) by A2, XBOOLE_0:def 4;

        hence contradiction by A17, A16, A3, TARSKI:def 2;

      end;

      

       A19: ( W-bound C) < ( E-bound C) by SPRECT_1: 31;

      

       A20: ( Lower_Arc C) misses S1

      proof

        

         A21: (S1 /\ C) = {( UMP C)} by Th34;

        assume ( Lower_Arc C) meets S1;

        then

        consider x be object such that

         A22: x in ( Lower_Arc C) and

         A23: x in S1 by XBOOLE_0: 3;

        x in (S1 /\ C) by A14, A22, A23, XBOOLE_0:def 4;

        then

         A24: x = ( UMP C) by A21, TARSKI:def 1;

        then x in (( Lower_Arc C) /\ ( Upper_Arc C)) by A2, A22, XBOOLE_0:def 4;

        hence contradiction by A17, A16, A3, A24, TARSKI:def 2;

      end;

      

       A25: ( LMP C) <> ( E-max C) by Th27;

      

       A26: ( LMP C) <> ( W-min C) by Th26;

       A27:

      now

        assume ( LMP C) in ( Lower_Arc C);

        then ( LMP C) in (( Upper_Arc C) /\ ( Lower_Arc C)) by A1, XBOOLE_0:def 4;

        hence contradiction by A26, A25, A3, TARSKI:def 2;

      end;

      

       A28: ( LMP C) <> ( UMP C) by Th37;

      

       A29: (( LMP C) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by EUCLID: 52;

      

       A30: ( Lower_Arc C) misses S2

      proof

        

         A31: (S2 /\ C) = {( LMP C)} by Th35;

        assume ( Lower_Arc C) meets S2;

        then

        consider x be object such that

         A32: x in ( Lower_Arc C) and

         A33: x in S2 by XBOOLE_0: 3;

        x in (S2 /\ C) by A14, A32, A33, XBOOLE_0:def 4;

        then

         A34: x = ( LMP C) by A31, TARSKI:def 1;

        then x in (( Lower_Arc C) /\ ( Upper_Arc C)) by A1, A32, XBOOLE_0:def 4;

        hence contradiction by A26, A25, A3, A34, TARSKI:def 2;

      end;

      (s `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by EUCLID: 52;

      then

       A35: S2 is vertical by A29, SPPOL_1: 16;

      

       A36: ( LMP C) in S2 by RLTOPSP1: 68;

      

       A37: (s `2 ) = ( S-bound C) by EUCLID: 52;

      then

       A38: for p be Point of ( TOP-REAL 2) st p in ( Lower_Arc C) holds (s `2 ) <= (p `2 ) & (p `2 ) <= (n `2 ) by A14, A9, PSCOMP_1: 24;

      per cases by A6, JORDAN16: 7;

        suppose

         A39: LE (( LMP C),( UMP C),C);

        set S = ( Segment (( Upper_Arc C),( W-min C),( E-max C),( LMP C),( UMP C)));

        

         A40: S c= ( Upper_Arc C) by JORDAN16: 2;

        then

         A41: S c= C by A8;

         A42:

        now

          let p be Point of ( TOP-REAL 2);

          assume

           A43: p in ((S1 \/ S) \/ S2);

          per cases by A43, Lm3;

            suppose p in S1;

            then (p `1 ) = (( UMP C) `1 ) by A10, A12, SPPOL_1:def 3;

            hence (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A7, A13, A19, XREAL_1: 226;

          end;

            suppose p in S;

            hence (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A13, A41, PSCOMP_1: 24;

          end;

            suppose p in S2;

            then (p `1 ) = (( LMP C) `1 ) by A35, A36, SPPOL_1:def 3;

            hence (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A29, A13, A19, XREAL_1: 226;

          end;

        end;

         A44:

        now

          let p be Point of ( TOP-REAL 2);

          assume

           A45: p in ((S1 \/ S) \/ S2);

          per cases by A45, Lm3;

            suppose

             A46: p in S1;

            

             A47: (s `2 ) <= (( UMP C) `2 ) by A37, Th38;

            

             A48: (( UMP C) `2 ) <= (n `2 ) by A9, Th39;

            then (( UMP C) `2 ) <= (p `2 ) by A46, TOPREAL1: 4;

            hence (s `2 ) <= (p `2 ) & (p `2 ) <= (n `2 ) by A46, A48, A47, TOPREAL1: 4, XXREAL_0: 2;

          end;

            suppose p in S;

            hence (s `2 ) <= (p `2 ) & (p `2 ) <= (n `2 ) by A37, A9, A41, PSCOMP_1: 24;

          end;

            suppose

             A49: p in S2;

            

             A50: (s `2 ) <= (( LMP C) `2 ) by A37, Th40;

            hence (s `2 ) <= (p `2 ) by A49, TOPREAL1: 4;

            (p `2 ) <= (( LMP C) `2 ) by A49, A50, TOPREAL1: 4;

            hence (p `2 ) <= (n `2 ) by A9, Th41, XXREAL_0: 2;

          end;

        end;

        

         A51: S c= (( Upper_Arc C) \ {( W-min C), ( E-max C)})

        proof

          let s be object;

          assume

           A52: s in S;

          now

            assume s in {( W-min C), ( E-max C)};

            then s = ( W-min C) or s = ( E-max C) by TARSKI:def 2;

            hence contradiction by A16, A26, A4, A52, Th11;

          end;

          hence thesis by A40, A52, XBOOLE_0:def 5;

        end;

        ( Lower_Arc C) misses S

        proof

          assume ( Lower_Arc C) meets S;

          then

          consider x be object such that

           A53: x in ( Lower_Arc C) and

           A54: x in S by XBOOLE_0: 3;

          x in ( Upper_Arc C) by A51, A54, XBOOLE_0:def 5;

          then x in (( Lower_Arc C) /\ ( Upper_Arc C)) by A53, XBOOLE_0:def 4;

          hence contradiction by A3, A51, A54, XBOOLE_0:def 5;

        end;

        then

         A55: ( Lower_Arc C) misses ((S1 \/ S) \/ S2) by A20, A30, Lm4;

        

         A56: LE (( LMP C),( UMP C),( Upper_Arc C),( W-min C),( E-max C)) by A18, A39, JORDAN6:def 10;

        then

         A57: ( UMP C) in S by JORDAN16: 5;

        

         A58: (S1 /\ S) = {( UMP C)}

        proof

          (S1 /\ C) = {( UMP C)} by Th34;

          hence (S1 /\ S) c= {( UMP C)} by A41, XBOOLE_1: 26;

          let x be object;

          assume x in {( UMP C)};

          then

           A59: x = ( UMP C) by TARSKI:def 1;

          ( UMP C) in S1 by RLTOPSP1: 68;

          hence thesis by A57, A59, XBOOLE_0:def 4;

        end;

        

         A60: ( LMP C) in S by A56, JORDAN16: 5;

        

         A61: (S2 /\ S) = {( LMP C)}

        proof

          (S2 /\ C) = {( LMP C)} by Th35;

          hence (S2 /\ S) c= {( LMP C)} by A41, XBOOLE_1: 26;

          let x be object;

          assume x in {( LMP C)};

          then x = ( LMP C) by TARSKI:def 1;

          hence thesis by A36, A60, XBOOLE_0:def 4;

        end;

        S is_an_arc_of (( LMP C),( UMP C)) by A28, A4, A56, JORDAN16: 21;

        then S is_an_arc_of (( UMP C),( LMP C)) by JORDAN5B: 14;

        then

         A62: (S1 \/ S) is_an_arc_of (n,( LMP C)) by A58, TOPREAL1: 11;

        ((S1 \/ S) /\ S2) = ((S1 /\ S2) \/ (S /\ S2)) by XBOOLE_1: 23

        .= ( {} \/ (S /\ S2)) by A11;

        then ((S1 \/ S) \/ S2) is_an_arc_of (n,s) by A61, A62, TOPREAL1: 10;

        then ((S1 \/ S) \/ S2) is_an_arc_of (s,n) by JORDAN5B: 14;

        hence thesis by A5, A38, A15, A55, A44, A42, JGRAPH_1: 44;

      end;

        suppose

         A63: LE (( UMP C),( LMP C),C);

        set S = ( Segment (( Upper_Arc C),( W-min C),( E-max C),( UMP C),( LMP C)));

        

         A64: S c= ( Upper_Arc C) by JORDAN16: 2;

        then

         A65: S c= C by A8;

         A66:

        now

          let p be Point of ( TOP-REAL 2);

          assume

           A67: p in ((S1 \/ S) \/ S2);

          per cases by A67, Lm3;

            suppose p in S1;

            then (p `1 ) = (( UMP C) `1 ) by A10, A12, SPPOL_1:def 3;

            hence (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A7, A13, A19, XREAL_1: 226;

          end;

            suppose p in S;

            hence (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A13, A65, PSCOMP_1: 24;

          end;

            suppose p in S2;

            then (p `1 ) = (( LMP C) `1 ) by A35, A36, SPPOL_1:def 3;

            hence (( W-min C) `1 ) <= (p `1 ) & (p `1 ) <= (( E-max C) `1 ) by A29, A13, A19, XREAL_1: 226;

          end;

        end;

         A68:

        now

          let p be Point of ( TOP-REAL 2);

          assume

           A69: p in ((S1 \/ S) \/ S2);

          per cases by A69, Lm3;

            suppose

             A70: p in S1;

            

             A71: (s `2 ) <= (( UMP C) `2 ) by A37, Th38;

            

             A72: (( UMP C) `2 ) <= (n `2 ) by A9, Th39;

            then (( UMP C) `2 ) <= (p `2 ) by A70, TOPREAL1: 4;

            hence (s `2 ) <= (p `2 ) & (p `2 ) <= (n `2 ) by A70, A72, A71, TOPREAL1: 4, XXREAL_0: 2;

          end;

            suppose p in S;

            hence (s `2 ) <= (p `2 ) & (p `2 ) <= (n `2 ) by A37, A9, A65, PSCOMP_1: 24;

          end;

            suppose

             A73: p in S2;

            

             A74: (s `2 ) <= (( LMP C) `2 ) by A37, Th40;

            hence (s `2 ) <= (p `2 ) by A73, TOPREAL1: 4;

            (p `2 ) <= (( LMP C) `2 ) by A73, A74, TOPREAL1: 4;

            hence (p `2 ) <= (n `2 ) by A9, Th41, XXREAL_0: 2;

          end;

        end;

        

         A75: S c= (( Upper_Arc C) \ {( W-min C), ( E-max C)})

        proof

          let s be object;

          assume

           A76: s in S;

          now

            assume s in {( W-min C), ( E-max C)};

            then s = ( W-min C) or s = ( E-max C) by TARSKI:def 2;

            hence contradiction by A17, A25, A4, A76, Th11;

          end;

          hence thesis by A64, A76, XBOOLE_0:def 5;

        end;

        ( Lower_Arc C) misses S

        proof

          assume ( Lower_Arc C) meets S;

          then

          consider x be object such that

           A77: x in ( Lower_Arc C) and

           A78: x in S by XBOOLE_0: 3;

          x in ( Upper_Arc C) by A75, A78, XBOOLE_0:def 5;

          then x in (( Lower_Arc C) /\ ( Upper_Arc C)) by A77, XBOOLE_0:def 4;

          hence contradiction by A3, A75, A78, XBOOLE_0:def 5;

        end;

        then

         A79: ( Lower_Arc C) misses ((S1 \/ S) \/ S2) by A20, A30, Lm4;

        

         A80: LE (( UMP C),( LMP C),( Upper_Arc C),( W-min C),( E-max C)) by A27, A63, JORDAN6:def 10;

        then

         A81: ( UMP C) in S by JORDAN16: 5;

        

         A82: (S1 /\ S) = {( UMP C)}

        proof

          (S1 /\ C) = {( UMP C)} by Th34;

          hence (S1 /\ S) c= {( UMP C)} by A65, XBOOLE_1: 26;

          let x be object;

          assume x in {( UMP C)};

          then

           A83: x = ( UMP C) by TARSKI:def 1;

          ( UMP C) in S1 by RLTOPSP1: 68;

          hence thesis by A81, A83, XBOOLE_0:def 4;

        end;

        

         A84: ( LMP C) in S by A80, JORDAN16: 5;

        

         A85: (S2 /\ S) = {( LMP C)}

        proof

          (S2 /\ C) = {( LMP C)} by Th35;

          hence (S2 /\ S) c= {( LMP C)} by A65, XBOOLE_1: 26;

          let x be object;

          assume x in {( LMP C)};

          then x = ( LMP C) by TARSKI:def 1;

          hence thesis by A36, A84, XBOOLE_0:def 4;

        end;

        S is_an_arc_of (( UMP C),( LMP C)) by A4, A80, Th37, JORDAN16: 21;

        then

         A86: (S1 \/ S) is_an_arc_of (n,( LMP C)) by A82, TOPREAL1: 11;

        ((S1 \/ S) /\ S2) = ((S1 /\ S2) \/ (S /\ S2)) by XBOOLE_1: 23

        .= ( {} \/ (S /\ S2)) by A11;

        then ((S1 \/ S) \/ S2) is_an_arc_of (n,s) by A85, A86, TOPREAL1: 10;

        then ((S1 \/ S) \/ S2) is_an_arc_of (s,n) by JORDAN5B: 14;

        hence thesis by A5, A38, A15, A79, A68, A66, JGRAPH_1: 44;

      end;

    end;