jordan_a.miz



    begin

    reserve C for Simple_closed_curve,

p,q,p1 for Point of ( TOP-REAL 2),

i,j,k,n for Nat,

r,s for Real;

    theorem :: JORDAN_A:1

    

     Th1: for T be non empty TopSpace, f be continuous RealMap of T, A be compact Subset of T holds (f .: A) is compact

    proof

      let T be non empty TopSpace, f be continuous RealMap of T, A be compact Subset of T;

      reconsider g = f as continuous Function of T, R^1 by JORDAN5A: 27, TOPMETR: 17;

      ( [#] (g .: A)) is compact by WEIERSTR: 9, WEIERSTR: 13;

      hence thesis by WEIERSTR:def 1;

    end;

    theorem :: JORDAN_A:2

    

     Th2: for A be compact Subset of REAL , B be non empty Subset of REAL st B c= A holds ( lower_bound B) in A

    proof

      let A be compact Subset of REAL , B be non empty Subset of REAL such that

       A1: B c= A;

      

       A2: A is real-bounded by RCOMP_1: 10;

      then

       A3: B is bounded_below by A1, XXREAL_2: 44;

      

       A4: ( Cl B) c= A by A1, MEASURE6: 57;

      ( Cl B) is bounded_below by A1, A2, MEASURE6: 57, XXREAL_2: 44;

      then ( lower_bound ( Cl B)) in ( Cl B) by RCOMP_1: 13;

      then ( lower_bound ( Cl B)) in A by A4;

      hence thesis by A3, TOPREAL6: 68;

    end;

    theorem :: JORDAN_A:3

    for A,B be compact non empty Subset of ( TOP-REAL n), f be continuous RealMap of [:( TOP-REAL n), ( TOP-REAL n):], g be RealMap of ( TOP-REAL n) st for p be Point of ( TOP-REAL n) holds ex G be Subset of REAL st G = { (f . (p,q)) where q be Point of ( TOP-REAL n) : q in B } & (g . p) = ( lower_bound G) holds ( lower_bound (f .: [:A, B:])) = ( lower_bound (g .: A))

    proof

      let A,B be compact non empty Subset of ( TOP-REAL n);

      let f be continuous RealMap of [:( TOP-REAL n), ( TOP-REAL n):];

      let g be RealMap of ( TOP-REAL n) such that

       A1: for p be Point of ( TOP-REAL n) holds ex G be Subset of REAL st G = { (f . (p,q)) where q be Point of ( TOP-REAL n) : q in B } & (g . p) = ( lower_bound G);

      

       A2: [:A, B:] is compact by BORSUK_3: 23;

      then

       A3: (f .: [:A, B:]) is compact by Th1;

      

       A4: (f .: [:A, B:]) is real-bounded by A2, Th1, RCOMP_1: 10;

      

       A5: (g .: A) c= (f .: [:A, B:])

      proof

        let u be object;

        assume u in (g .: A);

        then

        consider p be Point of ( TOP-REAL n) such that

         A6: p in A and

         A7: u = (g . p) by FUNCT_2: 65;

        consider q be Point of ( TOP-REAL n) such that

         A8: q in B by SUBSET_1: 4;

        consider G be Subset of REAL such that

         A9: G = { (f . (p,q1)) where q1 be Point of ( TOP-REAL n) : q1 in B } and

         A10: u = ( lower_bound G) by A1, A7;

        

         A11: (f . (p,q)) in G by A8, A9;

        G c= (f .: [:A, B:])

        proof

          let u be object;

          assume u in G;

          then

          consider q1 be Point of ( TOP-REAL n) such that

           A12: u = (f . (p,q1)) and

           A13: q1 in B by A9;

           [p, q1] in [:A, B:] by A6, A13, ZFMISC_1: 87;

          hence thesis by A12, FUNCT_2: 35;

        end;

        hence thesis by A3, A10, A11, Th2;

      end;

      then

       A14: (g .: A) is bounded_below by A4, XXREAL_2: 44;

      

       A15: for r st r in (f .: [:A, B:]) holds ( lower_bound (g .: A)) <= r

      proof

        let r;

        assume r in (f .: [:A, B:]);

        then

        consider pq be Point of [:( TOP-REAL n), ( TOP-REAL n):] such that

         A16: pq in [:A, B:] and

         A17: r = (f . pq) by FUNCT_2: 65;

        pq in the carrier of [:( TOP-REAL n), ( TOP-REAL n):];

        then pq in [:the carrier of ( TOP-REAL n), the carrier of ( TOP-REAL n):] by BORSUK_1:def 2;

        then

        consider p,q be object such that

         A18: p in the carrier of ( TOP-REAL n) and

         A19: q in the carrier of ( TOP-REAL n) and

         A20: pq = [p, q] by ZFMISC_1: 84;

        

         A21: q in B by A16, A20, ZFMISC_1: 87;

        reconsider p, q as Point of ( TOP-REAL n) by A18, A19;

        consider G be Subset of REAL such that

         A22: G = { (f . (p,q1)) where q1 be Point of ( TOP-REAL n) : q1 in B } and

         A23: (g . p) = ( lower_bound G) by A1;

        

         A24: p in A by A16, A20, ZFMISC_1: 87;

        G c= (f .: [:A, B:])

        proof

          let u be object;

          assume u in G;

          then

          consider q1 be Point of ( TOP-REAL n) such that

           A25: u = (f . (p,q1)) and

           A26: q1 in B by A22;

           [p, q1] in [:A, B:] by A24, A26, ZFMISC_1: 87;

          hence thesis by A25, FUNCT_2: 35;

        end;

        then

         A27: G is bounded_below by A4, XXREAL_2: 44;

        r = (f . (p,q)) by A17, A20;

        then r in G by A21, A22;

        then

         A28: (g . p) <= r by A23, A27, SEQ_4:def 2;

        (g . p) in (g .: A) by A24, FUNCT_2: 35;

        then ( lower_bound (g .: A)) <= (g . p) by A14, SEQ_4:def 2;

        hence thesis by A28, XXREAL_0: 2;

      end;

      for s st 0 < s holds ex r st r in (f .: [:A, B:]) & r < (( lower_bound (g .: A)) + s)

      proof

        let s;

        assume 0 < s;

        then

        consider r such that

         A29: r in (g .: A) and

         A30: r < (( lower_bound (g .: A)) + s) by A14, SEQ_4:def 2;

        take r;

        thus r in (f .: [:A, B:]) by A5, A29;

        thus thesis by A30;

      end;

      hence thesis by A4, A15, SEQ_4:def 2;

    end;

    theorem :: JORDAN_A:4

    for A,B be compact non empty Subset of ( TOP-REAL n), f be continuous RealMap of [:( TOP-REAL n), ( TOP-REAL n):], g be RealMap of ( TOP-REAL n) st for q be Point of ( TOP-REAL n) holds ex G be Subset of REAL st G = { (f . (p,q)) where p be Point of ( TOP-REAL n) : p in A } & (g . q) = ( lower_bound G) holds ( lower_bound (f .: [:A, B:])) = ( lower_bound (g .: B))

    proof

      let A,B be compact non empty Subset of ( TOP-REAL n);

      let f be continuous RealMap of [:( TOP-REAL n), ( TOP-REAL n):];

      let g be RealMap of ( TOP-REAL n) such that

       A1: for q be Point of ( TOP-REAL n) holds ex G be Subset of REAL st G = { (f . (p,q)) where p be Point of ( TOP-REAL n) : p in A } & (g . q) = ( lower_bound G);

      

       A2: [:A, B:] is compact by BORSUK_3: 23;

      then

       A3: (f .: [:A, B:]) is compact by Th1;

      

       A4: (f .: [:A, B:]) is real-bounded by A2, Th1, RCOMP_1: 10;

      

       A5: (g .: B) c= (f .: [:A, B:])

      proof

        let u be object;

        assume u in (g .: B);

        then

        consider q be Point of ( TOP-REAL n) such that

         A6: q in B and

         A7: u = (g . q) by FUNCT_2: 65;

        consider p be Point of ( TOP-REAL n) such that

         A8: p in A by SUBSET_1: 4;

        consider G be Subset of REAL such that

         A9: G = { (f . (p1,q)) where p1 be Point of ( TOP-REAL n) : p1 in A } and

         A10: u = ( lower_bound G) by A1, A7;

        

         A11: (f . (p,q)) in G by A8, A9;

        G c= (f .: [:A, B:])

        proof

          let u be object;

          assume u in G;

          then

          consider p1 be Point of ( TOP-REAL n) such that

           A12: u = (f . (p1,q)) and

           A13: p1 in A by A9;

           [p1, q] in [:A, B:] by A6, A13, ZFMISC_1: 87;

          hence thesis by A12, FUNCT_2: 35;

        end;

        hence thesis by A3, A10, A11, Th2;

      end;

      then

       A14: (g .: B) is bounded_below by A4, XXREAL_2: 44;

      

       A15: for r st r in (f .: [:A, B:]) holds ( lower_bound (g .: B)) <= r

      proof

        let r;

        assume r in (f .: [:A, B:]);

        then

        consider pq be Point of [:( TOP-REAL n), ( TOP-REAL n):] such that

         A16: pq in [:A, B:] and

         A17: r = (f . pq) by FUNCT_2: 65;

        pq in the carrier of [:( TOP-REAL n), ( TOP-REAL n):];

        then pq in [:the carrier of ( TOP-REAL n), the carrier of ( TOP-REAL n):] by BORSUK_1:def 2;

        then

        consider p,q be object such that

         A18: p in the carrier of ( TOP-REAL n) and

         A19: q in the carrier of ( TOP-REAL n) and

         A20: pq = [p, q] by ZFMISC_1: 84;

        

         A21: p in A by A16, A20, ZFMISC_1: 87;

        reconsider p, q as Point of ( TOP-REAL n) by A18, A19;

        consider G be Subset of REAL such that

         A22: G = { (f . (p1,q)) where p1 be Point of ( TOP-REAL n) : p1 in A } and

         A23: (g . q) = ( lower_bound G) by A1;

        

         A24: q in B by A16, A20, ZFMISC_1: 87;

        G c= (f .: [:A, B:])

        proof

          let u be object;

          assume u in G;

          then

          consider p1 be Point of ( TOP-REAL n) such that

           A25: u = (f . (p1,q)) and

           A26: p1 in A by A22;

           [p1, q] in [:A, B:] by A24, A26, ZFMISC_1: 87;

          hence thesis by A25, FUNCT_2: 35;

        end;

        then

         A27: G is bounded_below by A4, XXREAL_2: 44;

        r = (f . (p,q)) by A17, A20;

        then r in G by A21, A22;

        then

         A28: (g . q) <= r by A23, A27, SEQ_4:def 2;

        (g . q) in (g .: B) by A24, FUNCT_2: 35;

        then ( lower_bound (g .: B)) <= (g . q) by A14, SEQ_4:def 2;

        hence thesis by A28, XXREAL_0: 2;

      end;

      for s st 0 < s holds ex r st r in (f .: [:A, B:]) & r < (( lower_bound (g .: B)) + s)

      proof

        let s;

        assume 0 < s;

        then

        consider r such that

         A29: r in (g .: B) and

         A30: r < (( lower_bound (g .: B)) + s) by A14, SEQ_4:def 2;

        take r;

        thus r in (f .: [:A, B:]) by A5, A29;

        thus thesis by A30;

      end;

      hence thesis by A4, A15, SEQ_4:def 2;

    end;

    theorem :: JORDAN_A:5

    

     Th5: q in ( Lower_Arc C) & q <> ( W-min C) implies LE (( E-max C),q,C)

    proof

      ( E-max C) in ( Upper_Arc C) by JORDAN7: 1;

      hence thesis by JORDAN6:def 10;

    end;

    theorem :: JORDAN_A:6

    

     Th6: q in ( Upper_Arc C) implies LE (q,( E-max C),C)

    proof

      

       A1: ( E-max C) in ( Lower_Arc C) by JORDAN7: 1;

      ( E-max C) <> ( W-min C) by TOPREAL5: 19;

      hence thesis by A1, JORDAN6:def 10;

    end;

    begin

    definition

      let n;

      

       A1: [:the carrier of ( TOP-REAL n), the carrier of ( TOP-REAL n):] = the carrier of [:( TOP-REAL n), ( TOP-REAL n):] by BORSUK_1:def 2;

      :: JORDAN_A:def1

      func Eucl_dist n -> RealMap of [:( TOP-REAL n), ( TOP-REAL n):] means

      : Def1: for p,q be Point of ( TOP-REAL n) holds (it . (p,q)) = |.(p - q).|;

      existence

      proof

        deffunc F( Point of ( TOP-REAL n), Point of ( TOP-REAL n)) = |.($1 - $2).|;

        

         A2: for p,q be Point of ( TOP-REAL n) holds F(p,q) in REAL by XREAL_0:def 1;

        consider f be Function of [:the carrier of ( TOP-REAL n), the carrier of ( TOP-REAL n):], REAL such that

         A3: for p,q be Point of ( TOP-REAL n) holds (f . (p,q)) = F(p,q) from FUNCT_7:sch 1( A2);

        reconsider f as RealMap of [:( TOP-REAL n), ( TOP-REAL n):] by A1;

        take f;

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

        thus thesis by A3;

      end;

      uniqueness

      proof

        let IT1,IT2 be RealMap of [:( TOP-REAL n), ( TOP-REAL n):] such that

         A4: for p,q be Point of ( TOP-REAL n) holds (IT1 . (p,q)) = |.(p - q).| and

         A5: for p,q be Point of ( TOP-REAL n) holds (IT2 . (p,q)) = |.(p - q).|;

        now

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

          

          thus (IT1 . (p,q)) = |.(p - q).| by A4

          .= (IT2 . (p,q)) by A5;

        end;

        hence thesis by A1, BINOP_1: 2;

      end;

    end

    definition

      let T be non empty TopSpace, f be RealMap of T;

      :: original: continuous

      redefine

      :: JORDAN_A:def2

      attr f is continuous means for p be Point of T, N be Neighbourhood of (f . p) holds ex V be a_neighborhood of p st (f .: V) c= N;

      compatibility

      proof

        thus f is continuous implies for p be Point of T, N be Neighbourhood of (f . p) holds ex V be a_neighborhood of p st (f .: V) c= N

        proof

          assume

           A1: f is continuous;

          let p be Point of T, N be Neighbourhood of (f . p);

          

           A2: (f " (N ` )) = ((f " N) ` ) by FUNCT_2: 100;

          (N ` ) is closed by RCOMP_1:def 5;

          then (f " (N ` )) is closed by A1;

          then

           A3: (f " N) is open by A2, TOPS_1: 4;

          (f . p) in N by RCOMP_1: 16;

          then p in (f " N) by FUNCT_2: 38;

          then

          reconsider V = (f " N) as a_neighborhood of p by A3, CONNSP_2: 3;

          take V;

          thus thesis by FUNCT_1: 75;

        end;

        assume

         A4: for p be Point of T, N be Neighbourhood of (f . p) holds ex V be a_neighborhood of p st (f .: V) c= N;

        let Y be Subset of REAL ;

        assume Y is closed;

        then ((Y ` ) ` ) is closed;

        then

         A5: (Y ` ) is open by RCOMP_1:def 5;

        for p be Point of T st p in ((f " Y) ` ) holds ex A be Subset of T st A is a_neighborhood of p & A c= ((f " Y) ` )

        proof

          let p be Point of T;

          assume p in ((f " Y) ` );

          then p in (f " (Y ` )) by FUNCT_2: 100;

          then (f . p) in (Y ` ) by FUNCT_2: 38;

          then

          consider N be Neighbourhood of (f . p) such that

           A6: N c= (Y ` ) by A5, RCOMP_1: 18;

          consider V be a_neighborhood of p such that

           A7: (f .: V) c= N by A4;

          take V;

          thus V is a_neighborhood of p;

          (f .: V) c= (Y ` ) by A6, A7;

          then

           A8: (f " (f .: V)) c= (f " (Y ` )) by RELAT_1: 143;

          V c= (f " (f .: V)) by FUNCT_2: 42;

          then V c= (f " (Y ` )) by A8;

          hence thesis by FUNCT_2: 100;

        end;

        then ((f " Y) ` ) is open by CONNSP_2: 7;

        then (((f " Y) ` ) ` ) is closed by TOPS_1: 4;

        hence thesis;

      end;

    end

    

     Lm1: for X,Y be TopSpace holds the TopStruct of [:X, Y:] = [: the TopStruct of X, the TopStruct of Y:]

    proof

      let X,Y be TopSpace;

      set T = [: the TopStruct of X, the TopStruct of Y:];

      

       A1: the carrier of T = [:the carrier of the TopStruct of X, the carrier of the TopStruct of Y:] by BORSUK_1:def 2

      .= the carrier of [:X, Y:] by BORSUK_1:def 2;

      set tau1 = { ( union A) where A be Subset-Family of T : A c= { [:X1, Y1:] where X1 be Subset of the TopStruct of X, Y1 be Subset of the TopStruct of Y : X1 in the topology of the TopStruct of X & Y1 in the topology of the TopStruct of Y } };

      set tau2 = { ( union A) where A be Subset-Family of T : A c= { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y } };

      the topology of T = tau1 by BORSUK_1:def 2

      .= tau2

      .= the topology of [:X, Y:] by A1, BORSUK_1:def 2;

      hence thesis by A1;

    end;

    registration

      let n;

      cluster ( Eucl_dist n) -> continuous;

      coherence

      proof

        set f = ( Eucl_dist n);

        let p be Point of [:( TOP-REAL n), ( TOP-REAL n):], N be Neighbourhood of (f . p);

        consider r such that

         A1: 0 < r and

         A2: N = ].((f . p) - r), ((f . p) + r).[ by RCOMP_1:def 6;

        p in the carrier of [:( TOP-REAL n), ( TOP-REAL n):];

        then p in [:the carrier of ( TOP-REAL n), the carrier of ( TOP-REAL n):] by BORSUK_1:def 2;

        then

        consider p1,p2 be object such that

         A3: p1 in the carrier of ( TOP-REAL n) and

         A4: p2 in the carrier of ( TOP-REAL n) and

         A5: p = [p1, p2] by ZFMISC_1: 84;

        reconsider p1, p2 as Point of ( TOP-REAL n) by A3, A4;

        reconsider p19 = p1, p29 = p2 as Element of ( Euclid n) by TOPREAL3: 8;

        

         A6: the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

        then

        reconsider q1 = p1, q2 = p2 as Point of ( TopSpaceMetr ( Euclid n));

        reconsider U = ( Ball (p19,(r / 2))) as a_neighborhood of q1 by A1, GOBOARD6: 91, XREAL_1: 215;

        reconsider W = ( Ball (p29,(r / 2))) as a_neighborhood of q2 by A1, GOBOARD6: 91, XREAL_1: 215;

        reconsider V = [:U, W:] as a_neighborhood of p by A5, A6, Lm1;

        take V;

        let s be object;

        assume

         A7: s in (f .: V);

        then

        reconsider s as Real;

        consider q be Point of [:( TOP-REAL n), ( TOP-REAL n):] such that

         A8: q in V and

         A9: (f . q) = s by A7, FUNCT_2: 65;

        q in the carrier of [:( TOP-REAL n), ( TOP-REAL n):];

        then q in [:the carrier of ( TOP-REAL n), the carrier of ( TOP-REAL n):] by BORSUK_1:def 2;

        then

        consider q1,q2 be object such that

         A10: q1 in the carrier of ( TOP-REAL n) and

         A11: q2 in the carrier of ( TOP-REAL n) and

         A12: q = [q1, q2] by ZFMISC_1: 84;

        reconsider q1, q2 as Point of ( TOP-REAL n) by A10, A11;

        reconsider q19 = q1, q29 = q2 as Element of ( Euclid n) by TOPREAL3: 8;

        reconsider q199 = q19, q299 = q29, p199 = p19, p299 = p29 as Element of ( REAL n);

        

         A13: q19 in ( Ball (p19,(r / 2))) by A8, A12, ZFMISC_1: 87;

        

         A14: q29 in ( Ball (p29,(r / 2))) by A8, A12, ZFMISC_1: 87;

        

         A15: ( dist (q19,p19)) < (r / 2) by A13, METRIC_1: 11;

        

         A16: ( dist (q29,p29)) < (r / 2) by A14, METRIC_1: 11;

        

         A17: |.(q1 - p1).| < (r / 2) by A15, SPPOL_1: 5;

         |.(q2 - p2).| < (r / 2) by A16, SPPOL_1: 5;

        then

         A18: ( |.(q1 - p1).| + |.(q2 - p2).|) < ((r / 2) + (r / 2)) by A17, XREAL_1: 8;

        

         A19: for p,q be Point of ( TOP-REAL n) holds (f . [p, q]) = |.(p - q).|

        proof

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

          

          thus (f . [p, q]) = (f . (p,q))

          .= |.(p - q).| by Def1;

        end;

        then

         A20: (f . p) = |.(p1 - p2).| by A5;

        

         A21: s = |.(q1 - q2).| by A9, A12, A19;

        

         A22: ((q1 - q2) - (p1 - p2)) = (((q1 - q2) - p1) + p2) by RLVECT_1: 29

        .= ((q1 - (q2 + p1)) + p2) by RLVECT_1: 27

        .= (((q1 - p1) - q2) + p2) by RLVECT_1: 27

        .= ((q1 - p1) - (q2 - p2)) by RLVECT_1: 29;

        

         A23: |.((q1 - p1) - (q2 - p2)).| <= ( |.(q1 - p1).| + |.(q2 - p2).|) by TOPRNS_1: 30;

        

         A24: (s - (f . p)) <= |.((q1 - q2) - (p1 - p2)).| by A20, A21, TOPRNS_1: 32;

        ((f . p) - s) <= |.((p1 - p2) - (q1 - q2)).| by A20, A21, TOPRNS_1: 32;

        then ((f . p) - s) <= |.((q1 - q2) - (p1 - p2)).| by TOPRNS_1: 27;

        then ((f . p) - s) <= ( |.(q1 - p1).| + |.(q2 - p2).|) by A22, A23, XXREAL_0: 2;

        then ((f . p) - s) < r by A18, XXREAL_0: 2;

        then

         A25: ((f . p) - r) < s by XREAL_1: 11;

        (s - (f . p)) <= ( |.(q1 - p1).| + |.(q2 - p2).|) by A22, A23, A24, XXREAL_0: 2;

        then (s - (f . p)) < r by A18, XXREAL_0: 2;

        then s < ((f . p) + r) by XREAL_1: 19;

        hence thesis by A2, A25, XXREAL_1: 4;

      end;

    end

    begin

    theorem :: JORDAN_A:7

    

     Th7: for A,B be non empty compact Subset of ( TOP-REAL n) st A misses B holds ( dist_min (A,B)) > 0

    proof

      let A,B be non empty compact Subset of ( TOP-REAL n) such that

       A1: A misses B;

      

       A2: the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      consider A9,B9 be Subset of ( TopSpaceMetr ( Euclid n)) such that

       A3: A = A9 and

       A4: B = B9 and

       A5: ( dist_min (A,B)) = ( min_dist_min (A9,B9)) by JORDAN1K:def 1;

      

       A6: A9 is compact by A2, A3, COMPTS_1: 23;

      B9 is compact by A2, A4, COMPTS_1: 23;

      hence thesis by A1, A3, A4, A5, A6, JGRAPH_1: 38;

    end;

    begin

    theorem :: JORDAN_A:8

    

     Th8: LE (p,q,C) & LE (q,( E-max C),C) & p <> q implies ( Segment (p,q,C)) = ( Segment (( Upper_Arc C),( W-min C),( E-max C),p,q))

    proof

      assume that

       A1: LE (p,q,C) and

       A2: LE (q,( E-max C),C) and

       A3: p <> q;

      

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

      

       A5: LE (p,( E-max C),C) by A1, A2, JORDAN6: 58;

      

       A6: p in ( Upper_Arc C) by A1, A2, JORDAN17: 3, JORDAN6: 58;

      

       A7: q in ( Upper_Arc C) by A2, JORDAN17: 3;

      

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

       A9:

      now

        assume q = ( W-min C);

        then LE (q,p,C) by A6, A8, JORDAN7: 3;

        hence contradiction by A1, A3, JORDAN6: 57;

      end;

      defpred P[ Point of ( TOP-REAL 2)] means LE (p,$1,C) & LE ($1,q,C);

      defpred Q[ Point of ( TOP-REAL 2)] means LE (p,$1,( Upper_Arc C),( W-min C),( E-max C)) & LE ($1,q,( Upper_Arc C),( W-min C),( E-max C));

      

       A10: P[p1] iff Q[p1]

      proof

        hereby

          assume that

           A11: LE (p,p1,C) and

           A12: LE (p1,q,C);

          hereby

            per cases ;

              suppose p1 = ( E-max C);

              hence LE (p,p1,( Upper_Arc C),( W-min C),( E-max C)) by A4, A6, JORDAN5C: 10;

            end;

              suppose p1 = ( W-min C);

              then LE (p1,p,C) by A6, A8, JORDAN7: 3;

              then p = p1 by A11, JORDAN6: 57;

              hence LE (p,p1,( Upper_Arc C),( W-min C),( E-max C)) by A5, JORDAN17: 3, JORDAN5C: 9;

            end;

              suppose that

               A13: p1 <> ( E-max C) and

               A14: p1 <> ( W-min C);

              now

                assume

                 A15: p1 in ( Lower_Arc C);

                p1 in ( Upper_Arc C) by A2, A12, JORDAN17: 3, JORDAN6: 58;

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

                then p1 in {( W-min C), ( E-max C)} by JORDAN6: 50;

                hence contradiction by A13, A14, TARSKI:def 2;

              end;

              hence LE (p,p1,( Upper_Arc C),( W-min C),( E-max C)) by A11, JORDAN6:def 10;

            end;

          end;

          per cases ;

            suppose

             A16: q = ( E-max C);

            then p1 in ( Upper_Arc C) by A12, JORDAN17: 3;

            hence LE (p1,q,( Upper_Arc C),( W-min C),( E-max C)) by A4, A16, JORDAN5C: 10;

          end;

            suppose

             A17: q <> ( E-max C);

            now

              assume q in ( Lower_Arc C);

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

              then q in {( W-min C), ( E-max C)} by JORDAN6: 50;

              hence contradiction by A9, A17, TARSKI:def 2;

            end;

            hence LE (p1,q,( Upper_Arc C),( W-min C),( E-max C)) by A12, JORDAN6:def 10;

          end;

        end;

        assume that

         A18: LE (p,p1,( Upper_Arc C),( W-min C),( E-max C)) and

         A19: LE (p1,q,( Upper_Arc C),( W-min C),( E-max C));

        

         A20: p1 in ( Upper_Arc C) by A18, JORDAN5C:def 3;

        hence LE (p,p1,C) by A6, A18, JORDAN6:def 10;

        thus thesis by A7, A19, A20, JORDAN6:def 10;

      end;

      deffunc F( set) = $1;

      set X = { F(p1) : P[p1] }, Y = { F(p1) : Q[p1] };

      

       A21: X = Y from FRAENKEL:sch 3( A10);

      ( Segment (p,q,C)) = X by A9, JORDAN7:def 1;

      hence thesis by A21, JORDAN6: 26;

    end;

    theorem :: JORDAN_A:9

    

     Th9: LE (( E-max C),q,C) implies ( Segment (( E-max C),q,C)) = ( Segment (( Lower_Arc C),( E-max C),( W-min C),( E-max C),q))

    proof

      set p = ( E-max C);

      assume

       A1: LE (( E-max C),q,C);

      

       A2: ( Lower_Arc C) is_an_arc_of (( E-max C),( W-min C)) by JORDAN6: 50;

      

       A3: p in ( Lower_Arc C) by JORDAN7: 1;

      

       A4: q in ( Lower_Arc C) by A1, JORDAN17: 4;

      

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

       A6:

      now

        assume

         A7: q = ( W-min C);

        then p = q by A1, JORDAN7: 2;

        hence contradiction by A7, TOPREAL5: 19;

      end;

      defpred P[ Point of ( TOP-REAL 2)] means LE (p,$1,C) & LE ($1,q,C);

      defpred Q[ Point of ( TOP-REAL 2)] means LE (p,$1,( Lower_Arc C),( E-max C),( W-min C)) & LE ($1,q,( Lower_Arc C),( E-max C),( W-min C));

      

       A8: P[p1] iff Q[p1]

      proof

        hereby

          assume that

           A9: LE (p,p1,C) and

           A10: LE (p1,q,C);

          

           A11: p1 in ( Lower_Arc C) by A9, JORDAN17: 4;

          hence LE (p,p1,( Lower_Arc C),( E-max C),( W-min C)) by A2, JORDAN5C: 10;

          per cases ;

            suppose

             A12: p1 = ( E-max C);

            then q in ( Lower_Arc C) by A10, JORDAN17: 4;

            hence LE (p1,q,( Lower_Arc C),( E-max C),( W-min C)) by A2, A12, JORDAN5C: 10;

          end;

            suppose

             A13: p1 <> ( E-max C);

             A14:

            now

              assume

               A15: p1 = ( W-min C);

              then LE (p1,p,C) by A3, A5, JORDAN7: 3;

              hence contradiction by A9, A15, JORDAN6: 57, TOPREAL5: 19;

            end;

            now

              assume p1 in ( Upper_Arc C);

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

              then p1 in {( W-min C), ( E-max C)} by JORDAN6: 50;

              hence contradiction by A13, A14, TARSKI:def 2;

            end;

            hence LE (p1,q,( Lower_Arc C),( E-max C),( W-min C)) by A10, JORDAN6:def 10;

          end;

        end;

        assume that

         A16: LE (p,p1,( Lower_Arc C),( E-max C),( W-min C)) and

         A17: LE (p1,q,( Lower_Arc C),( E-max C),( W-min C));

        

         A18: p1 in ( Lower_Arc C) by A16, JORDAN5C:def 3;

        p1 <> ( W-min C) by A2, A6, A17, JORDAN6: 55;

        hence LE (p,p1,C) by A3, A16, A18, JORDAN6:def 10;

        thus thesis by A4, A6, A17, A18, JORDAN6:def 10;

      end;

      deffunc F( set) = $1;

      set X = { F(p1) : P[p1] }, Y = { F(p1) : Q[p1] };

      

       A19: X = Y from FRAENKEL:sch 3( A8);

      ( Segment (p,q,C)) = X by A6, JORDAN7:def 1;

      hence thesis by A19, JORDAN6: 26;

    end;

    theorem :: JORDAN_A:10

    

     Th10: LE (( E-max C),q,C) implies ( Segment (q,( W-min C),C)) = ( Segment (( Lower_Arc C),( E-max C),( W-min C),q,( W-min C)))

    proof

      set p = ( W-min C);

      assume

       A1: LE (( E-max C),q,C);

      

       A2: ( Lower_Arc C) is_an_arc_of (( E-max C),( W-min C)) by JORDAN6: 50;

      

       A3: p in ( Lower_Arc C) by JORDAN7: 1;

      

       A4: q in ( Lower_Arc C) by A1, JORDAN17: 4;

      

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

      defpred P[ Point of ( TOP-REAL 2)] means LE (q,$1,C) or q in C & $1 = ( W-min C);

      defpred Q[ Point of ( TOP-REAL 2)] means LE (q,$1,( Lower_Arc C),( E-max C),( W-min C)) & LE ($1,p,( Lower_Arc C),( E-max C),( W-min C));

      

       A6: P[p1] iff Q[p1]

      proof

        hereby

          assume

           A7: LE (q,p1,C) or q in C & p1 = ( W-min C);

          per cases by A7;

            suppose that

             A8: q = ( E-max C) and

             A9: LE (q,p1,C);

            

             A10: p1 in ( Lower_Arc C) by A8, A9, JORDAN17: 4;

            hence LE (q,p1,( Lower_Arc C),( E-max C),( W-min C)) by A2, A8, JORDAN5C: 10;

            thus LE (p1,p,( Lower_Arc C),( E-max C),( W-min C)) by A2, A10, JORDAN5C: 10;

          end;

            suppose that

             A11: q <> ( E-max C) and

             A12: LE (q,p1,C);

            

             A13: p1 in ( Lower_Arc C) by A1, A12, JORDAN17: 4, JORDAN6: 58;

             A14:

            now

              assume

               A15: q = ( W-min C);

              then LE (q,( E-max C),C) by JORDAN7: 3, SPRECT_1: 14;

              hence contradiction by A1, A15, JORDAN6: 57, TOPREAL5: 19;

            end;

            now

              assume q in ( Upper_Arc C);

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

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

              hence contradiction by A11, A14, TARSKI:def 2;

            end;

            hence LE (q,p1,( Lower_Arc C),( E-max C),( W-min C)) by A12, JORDAN6:def 10;

            thus LE (p1,p,( Lower_Arc C),( E-max C),( W-min C)) by A2, A13, JORDAN5C: 10;

          end;

            suppose that q in C and

             A16: p1 = ( W-min C);

            thus LE (q,p1,( Lower_Arc C),( E-max C),( W-min C)) by A2, A4, A16, JORDAN5C: 10;

            thus LE (p1,p,( Lower_Arc C),( E-max C),( W-min C)) by A3, A16, JORDAN5C: 9;

          end;

        end;

        assume that

         A17: LE (q,p1,( Lower_Arc C),( E-max C),( W-min C)) and LE (p1,p,( Lower_Arc C),( E-max C),( W-min C));

        

         A18: p1 in ( Lower_Arc C) by A17, JORDAN5C:def 3;

        

         A19: q in ( Lower_Arc C) by A17, JORDAN5C:def 3;

        per cases ;

          suppose p1 <> ( W-min C);

          hence thesis by A17, A18, A19, JORDAN6:def 10;

        end;

          suppose p1 = ( W-min C);

          hence thesis by A4, A5;

        end;

      end;

      deffunc F( set) = $1;

      set X = { F(p1) : P[p1] }, Y = { F(p1) : Q[p1] };

      

       A20: X = Y from FRAENKEL:sch 3( A6);

      ( Segment (q,p,C)) = X by JORDAN7:def 1;

      hence thesis by A20, JORDAN6: 26;

    end;

    theorem :: JORDAN_A:11

    

     Th11: LE (p,q,C) & LE (( E-max C),p,C) implies ( Segment (p,q,C)) = ( Segment (( Lower_Arc C),( E-max C),( W-min C),p,q))

    proof

      assume that

       A1: LE (p,q,C) and

       A2: LE (( E-max C),p,C);

      per cases ;

        suppose p = ( E-max C);

        hence thesis by A1, Th9;

      end;

        suppose

         A3: p <> ( E-max C);

        

         A4: ( Lower_Arc C) is_an_arc_of (( E-max C),( W-min C)) by JORDAN6: 50;

        

         A5: q in ( Lower_Arc C) by A1, A2, JORDAN17: 4, JORDAN6: 58;

        

         A6: p in ( Lower_Arc C) by A2, JORDAN17: 4;

        

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

         A8:

        now

          assume

           A9: p = ( W-min C);

          then LE (p,( E-max C),C) by JORDAN17: 2;

          hence contradiction by A2, A9, JORDAN6: 57, TOPREAL5: 19;

        end;

         A10:

        now

          assume

           A11: q = ( W-min C);

          then LE (q,p,C) by A6, A7, JORDAN7: 3;

          hence contradiction by A1, A8, A11, JORDAN6: 57;

        end;

        defpred P[ Point of ( TOP-REAL 2)] means LE (p,$1,C) & LE ($1,q,C);

        defpred Q[ Point of ( TOP-REAL 2)] means LE (p,$1,( Lower_Arc C),( E-max C),( W-min C)) & LE ($1,q,( Lower_Arc C),( E-max C),( W-min C));

        

         A12: P[p1] iff Q[p1]

        proof

          hereby

            assume that

             A13: LE (p,p1,C) and

             A14: LE (p1,q,C);

             A15:

            now

              assume

               A16: p1 = ( W-min C);

              then LE (p1,p,C) by A6, A7, JORDAN7: 3;

              hence contradiction by A8, A13, A16, JORDAN6: 57;

            end;

             A17:

            now

              assume

               A18: p in ( Upper_Arc C);

              p in ( Lower_Arc C) by A2, JORDAN17: 4;

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

              then p in {( W-min C), ( E-max C)} by JORDAN6: 50;

              hence contradiction by A3, A8, TARSKI:def 2;

            end;

            hence LE (p,p1,( Lower_Arc C),( E-max C),( W-min C)) by A13, JORDAN6:def 10;

            

             A19: p1 in ( Lower_Arc C) by A13, A17, JORDAN6:def 10;

            per cases ;

              suppose q = ( E-max C);

              hence LE (p1,q,( Lower_Arc C),( E-max C),( W-min C)) by A1, A2, A3, JORDAN6: 57;

            end;

              suppose p1 = ( E-max C);

              hence LE (p1,q,( Lower_Arc C),( E-max C),( W-min C)) by A4, A5, JORDAN5C: 10;

            end;

              suppose that

               A20: p1 <> ( E-max C);

              now

                assume p1 in ( Upper_Arc C);

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

                then p1 in {( W-min C), ( E-max C)} by JORDAN6: 50;

                hence contradiction by A15, A20, TARSKI:def 2;

              end;

              hence LE (p1,q,( Lower_Arc C),( E-max C),( W-min C)) by A14, JORDAN6:def 10;

            end;

          end;

          assume that

           A21: LE (p,p1,( Lower_Arc C),( E-max C),( W-min C)) and

           A22: LE (p1,q,( Lower_Arc C),( E-max C),( W-min C));

          

           A23: p1 <> ( W-min C) by A4, A10, A22, JORDAN6: 55;

          

           A24: p1 in ( Lower_Arc C) by A21, JORDAN5C:def 3;

          hence LE (p,p1,C) by A6, A21, A23, JORDAN6:def 10;

          thus thesis by A5, A10, A22, A24, JORDAN6:def 10;

        end;

        deffunc F( set) = $1;

        set X = { F(p1) : P[p1] }, Y = { F(p1) : Q[p1] };

        

         A25: X = Y from FRAENKEL:sch 3( A12);

        ( Segment (p,q,C)) = X by A10, JORDAN7:def 1;

        hence thesis by A25, JORDAN6: 26;

      end;

    end;

    theorem :: JORDAN_A:12

    

     Th12: LE (p,( E-max C),C) & LE (( E-max C),q,C) implies ( Segment (p,q,C)) = (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) \/ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)))

    proof

      assume that

       A1: LE (p,( E-max C),C) and

       A2: LE (( E-max C),q,C);

      

       A3: p in ( Upper_Arc C) by A1, JORDAN17: 3;

      

       A4: q in ( Lower_Arc C) by A2, JORDAN17: 4;

       A5:

      now

        assume q = ( W-min C);

        then ( W-min C) = ( E-max C) by A2, JORDAN7: 2;

        hence contradiction by TOPREAL5: 19;

      end;

      

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

      defpred P[ Point of ( TOP-REAL 2)] means LE (p,$1,C) & LE ($1,q,C);

      defpred Q1[ Point of ( TOP-REAL 2)] means LE (p,$1,( Upper_Arc C),( W-min C),( E-max C));

      defpred Q2[ Point of ( TOP-REAL 2)] means LE ($1,q,( Lower_Arc C),( E-max C),( W-min C));

      defpred Q[ Point of ( TOP-REAL 2)] means Q1[$1] or Q2[$1];

      

       A7: P[p1] iff Q[p1]

      proof

        thus LE (p,p1,C) & LE (p1,q,C) implies LE (p,p1,( Upper_Arc C),( W-min C),( E-max C)) or LE (p1,q,( Lower_Arc C),( E-max C),( W-min C))

        proof

          assume that

           A8: LE (p,p1,C) and

           A9: LE (p1,q,C);

           A10:

          now

            assume that

             A11: p1 in ( Lower_Arc C) and

             A12: p1 in ( Upper_Arc C);

            p1 in (( Lower_Arc C) /\ ( Upper_Arc C)) by A11, A12, XBOOLE_0:def 4;

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

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

          end;

          per cases by A10;

            suppose

             A13: p1 = ( W-min C);

            then p = ( W-min C) by A8, JORDAN7: 2;

            hence thesis by A1, A13, JORDAN17: 3, JORDAN5C: 9;

          end;

            suppose p1 = ( E-max C);

            hence thesis by A4, A6, JORDAN5C: 10;

          end;

            suppose not p1 in ( Lower_Arc C);

            hence thesis by A8, JORDAN6:def 10;

          end;

            suppose not p1 in ( Upper_Arc C);

            hence thesis by A9, JORDAN6:def 10;

          end;

        end;

        assume that

         A14: LE (p,p1,( Upper_Arc C),( W-min C),( E-max C)) or LE (p1,q,( Lower_Arc C),( E-max C),( W-min C));

        per cases by A14;

          suppose

           A15: LE (p,p1,( Upper_Arc C),( W-min C),( E-max C));

          then

           A16: p1 in ( Upper_Arc C) by JORDAN5C:def 3;

          hence LE (p,p1,C) by A3, A15, JORDAN6:def 10;

          thus thesis by A4, A5, A16, JORDAN6:def 10;

        end;

          suppose that

           A17: LE (p1,q,( Lower_Arc C),( E-max C),( W-min C)) and

           A18: p1 <> ( W-min C);

          

           A19: p1 in ( Lower_Arc C) by A17, JORDAN5C:def 3;

          hence LE (p,p1,C) by A3, A18, JORDAN6:def 10;

          thus thesis by A4, A5, A17, A19, JORDAN6:def 10;

        end;

          suppose LE (p1,q,( Lower_Arc C),( E-max C),( W-min C)) & p1 = ( W-min C);

          hence thesis by A5, A6, JORDAN6: 55;

        end;

      end;

      set Y1 = { p1 : Q1[p1] }, Y2 = { p1 : Q2[p1] };

      deffunc F( set) = $1;

      set X = { F(p1) : P[p1] }, Y = { F(p1) : Q[p1] }, Y9 = { p1 : Q1[p1] or Q2[p1] };

      

       A20: X = Y from FRAENKEL:sch 3( A7);

      

       A21: ( Segment (p,q,C)) = X by A5, JORDAN7:def 1;

      

       A22: ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) = Y2 by JORDAN6:def 3;

      Y9 = (Y1 \/ Y2) from TOPREAL1:sch 1;

      hence thesis by A20, A21, A22, JORDAN6:def 4;

    end;

    theorem :: JORDAN_A:13

    

     Th13: LE (p,( E-max C),C) implies ( Segment (p,( W-min C),C)) = (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) \/ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),( W-min C))))

    proof

      set q = ( W-min C);

      assume LE (p,( E-max C),C);

      then

       A1: p in ( Upper_Arc C) by JORDAN17: 3;

      

       A2: q in ( Lower_Arc C) by JORDAN7: 1;

      

       A3: ( Lower_Arc C) is_an_arc_of (( E-max C),( W-min C)) by JORDAN6: 50;

      defpred P[ Point of ( TOP-REAL 2)] means LE (p,$1,C) or p in C & $1 = ( W-min C);

      defpred Q1[ Point of ( TOP-REAL 2)] means LE (p,$1,( Upper_Arc C),( W-min C),( E-max C));

      defpred Q2[ Point of ( TOP-REAL 2)] means LE ($1,q,( Lower_Arc C),( E-max C),( W-min C));

      defpred Q[ Point of ( TOP-REAL 2)] means Q1[$1] or Q2[$1];

      

       A4: P[p1] iff Q[p1]

      proof

        thus LE (p,p1,C) or p in C & p1 = ( W-min C) implies LE (p,p1,( Upper_Arc C),( W-min C),( E-max C)) or LE (p1,q,( Lower_Arc C),( E-max C),( W-min C))

        proof

          assume

           A5: LE (p,p1,C) or p in C & p1 = ( W-min C);

           A6:

          now

            assume that

             A7: p1 in ( Lower_Arc C) and

             A8: p1 in ( Upper_Arc C);

            p1 in (( Lower_Arc C) /\ ( Upper_Arc C)) by A7, A8, XBOOLE_0:def 4;

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

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

          end;

          per cases by A6;

            suppose p1 = ( W-min C);

            hence thesis by A2, JORDAN5C: 9;

          end;

            suppose p1 = ( E-max C);

            hence thesis by A2, A3, JORDAN5C: 10;

          end;

            suppose not p1 in ( Lower_Arc C) & p1 <> ( W-min C);

            hence thesis by A5, JORDAN6:def 10;

          end;

            suppose that

             A9: not p1 in ( Upper_Arc C) and

             A10: p1 <> ( W-min C);

            

             A11: p1 in C by A5, A10, JORDAN7: 5;

            C = (( Lower_Arc C) \/ ( Upper_Arc C)) by JORDAN6:def 9;

            then p1 in ( Lower_Arc C) by A9, A11, XBOOLE_0:def 3;

            hence thesis by A3, JORDAN5C: 10;

          end;

        end;

        assume that

         A12: LE (p,p1,( Upper_Arc C),( W-min C),( E-max C)) or LE (p1,q,( Lower_Arc C),( E-max C),( W-min C));

        

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

        per cases by A12;

          suppose

           A14: LE (p,p1,( Upper_Arc C),( W-min C),( E-max C));

          then p1 in ( Upper_Arc C) by JORDAN5C:def 3;

          hence thesis by A1, A14, JORDAN6:def 10;

        end;

          suppose LE (p1,q,( Lower_Arc C),( E-max C),( W-min C));

          then

           A15: p1 in ( Lower_Arc C) by JORDAN5C:def 3;

          now

            per cases ;

              suppose p1 = ( W-min C);

              hence thesis by A1, A13;

            end;

              suppose p1 <> ( W-min C);

              hence thesis by A1, A15, JORDAN6:def 10;

            end;

          end;

          hence thesis;

        end;

      end;

      set Y1 = { p1 : Q1[p1] }, Y2 = { p1 : Q2[p1] };

      deffunc F( set) = $1;

      set X = { F(p1) : P[p1] }, Y = { F(p1) : Q[p1] }, Y9 = { p1 : Q1[p1] or Q2[p1] };

      

       A16: X = Y from FRAENKEL:sch 3( A4);

      

       A17: ( Segment (p,q,C)) = X by JORDAN7:def 1;

      

       A18: ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) = Y2 by JORDAN6:def 3;

      Y9 = (Y1 \/ Y2) from TOPREAL1:sch 1;

      hence thesis by A16, A17, A18, JORDAN6:def 4;

    end;

    theorem :: JORDAN_A:14

    

     Th14: ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) = ( Segment (( Upper_Arc C),( W-min C),( E-max C),p,( E-max C)))

    proof

      ( Upper_Arc C) is_an_arc_of (( W-min C),( E-max C)) by JORDAN6: 50;

      then ( L_Segment (( Upper_Arc C),( W-min C),( E-max C),( E-max C))) = ( Upper_Arc C) by JORDAN6: 22;

      

      hence ( Segment (( Upper_Arc C),( W-min C),( E-max C),p,( E-max C))) = (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) /\ ( Upper_Arc C)) by JORDAN6:def 5

      .= ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) by JORDAN6: 20, XBOOLE_1: 28;

    end;

    theorem :: JORDAN_A:15

    

     Th15: ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),p)) = ( Segment (( Lower_Arc C),( E-max C),( W-min C),( E-max C),p))

    proof

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

      then ( R_Segment (( Lower_Arc C),( E-max C),( W-min C),( E-max C))) = ( Lower_Arc C) by JORDAN6: 24;

      

      hence ( Segment (( Lower_Arc C),( E-max C),( W-min C),( E-max C),p)) = (( Lower_Arc C) /\ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),p))) by JORDAN6:def 5

      .= ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),p)) by JORDAN6: 19, XBOOLE_1: 28;

    end;

    theorem :: JORDAN_A:16

    

     Th16: for p be Point of ( TOP-REAL 2) st p in C & p <> ( W-min C) holds ( Segment (p,( W-min C),C)) is_an_arc_of (p,( W-min C))

    proof

      set q = ( W-min C);

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

       A1: p in C and

       A2: p <> ( W-min C);

      

       A3: ( E-max C) in C by SPRECT_1: 14;

      

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

      

       A5: ( Lower_Arc C) is_an_arc_of (( E-max C),( W-min C)) by JORDAN6: 50;

      

       A6: q <> ( E-max C) by TOPREAL5: 19;

      per cases by A1, A3, JORDAN16: 7;

        suppose that

         A7: p <> ( E-max C) and

         A8: LE (p,( E-max C),C);

         A9:

        now

          assume ( W-min C) in (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) /\ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)));

          then ( W-min C) in ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) by XBOOLE_0:def 4;

          hence contradiction by A2, A4, JORDAN6: 60;

        end;

        p in ( Upper_Arc C) by A8, JORDAN17: 3;

        then

         A10: LE (p,( E-max C),( Upper_Arc C),( W-min C),( E-max C)) by A4, JORDAN5C: 10;

        

         A11: ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) = ( Segment (( Upper_Arc C),( W-min C),( E-max C),p,( E-max C))) by Th14;

        then

         A12: ( E-max C) in ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) by A10, JORDAN16: 5;

        q in ( Lower_Arc C) by JORDAN7: 1;

        then

         A13: LE (( E-max C),q,( Lower_Arc C),( E-max C),( W-min C)) by A5, JORDAN5C: 10;

        

         A14: ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) = ( Segment (( Lower_Arc C),( E-max C),( W-min C),( E-max C),q)) by Th15;

        then ( E-max C) in ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) by A13, JORDAN16: 5;

        then

         A15: ( E-max C) in (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) /\ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q))) by A12, XBOOLE_0:def 4;

        

         A16: ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) c= ( Upper_Arc C) by JORDAN6: 20;

        

         A17: ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) c= ( Lower_Arc C) by JORDAN6: 19;

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

        then

         A18: (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) /\ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q))) = {( E-max C)} by A9, A15, A16, A17, TOPREAL8: 1, XBOOLE_1: 27;

        

         A19: ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) is_an_arc_of (p,( E-max C)) by A4, A7, A10, A11, JORDAN16: 21;

        

         A20: ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) is_an_arc_of (( E-max C),q) by A5, A6, A13, A14, JORDAN16: 21;

        ( Segment (p,( W-min C),C)) = (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) \/ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),( W-min C)))) by A8, Th13;

        hence thesis by A18, A19, A20, TOPREAL1: 2;

      end;

        suppose

         A21: p = ( E-max C);

        then ( Segment (p,q,C)) = ( Lower_Arc C) by JORDAN7: 4;

        hence thesis by A21, JORDAN6: 50;

      end;

        suppose that p <> ( E-max C) and

         A22: LE (( E-max C),p,C);

        

         A23: ( Segment (p,q,C)) = ( Segment (( Lower_Arc C),( E-max C),( W-min C),p,q)) by A22, Th10;

        p in ( Lower_Arc C) by A22, JORDAN17: 4;

        then LE (p,q,( Lower_Arc C),( E-max C),( W-min C)) by A5, JORDAN5C: 10;

        hence thesis by A2, A5, A23, JORDAN16: 21;

      end;

    end;

    theorem :: JORDAN_A:17

    

     Th17: for p,q be Point of ( TOP-REAL 2) st p <> q & LE (p,q,C) holds ( Segment (p,q,C)) is_an_arc_of (p,q)

    proof

      let p,q be Point of ( TOP-REAL 2) such that

       A1: p <> q and

       A2: LE (p,q,C);

      

       A3: ( E-max C) in C by SPRECT_1: 14;

      

       A4: p in C by A2, JORDAN7: 5;

      

       A5: q in C by A2, JORDAN7: 5;

      

       A6: ( Upper_Arc C) is_an_arc_of (( W-min C),( E-max C)) by JORDAN6: 50;

      

       A7: ( Lower_Arc C) is_an_arc_of (( E-max C),( W-min C)) by JORDAN6: 50;

      per cases by A3, A4, A5, JORDAN16: 7;

        suppose q = ( W-min C);

        hence thesis by A1, A4, Th16;

      end;

        suppose that

         A8: LE (q,( E-max C),C) and

         A9: not LE (( E-max C),q,C) and

         A10: q <> ( W-min C);

        

         A11: ( Segment (p,q,C)) = ( Segment (( Upper_Arc C),( W-min C),( E-max C),p,q)) by A1, A2, A8, Th8;

         not q in ( Lower_Arc C) by A9, A10, Th5;

        then LE (p,q,( Upper_Arc C),( W-min C),( E-max C)) by A2, JORDAN6:def 10;

        hence thesis by A1, A6, A11, JORDAN16: 21;

      end;

        suppose that

         A12: p <> ( E-max C) and

         A13: LE (p,( E-max C),C) and

         A14: LE (( E-max C),q,C) and

         A15: q <> ( E-max C);

         A16:

        now

          assume

           A17: ( W-min C) in (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) /\ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)));

          then ( W-min C) in ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) by XBOOLE_0:def 4;

          then

           A18: p = ( W-min C) by A6, JORDAN6: 60;

          ( W-min C) in ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) by A17, XBOOLE_0:def 4;

          hence contradiction by A1, A7, A18, JORDAN6: 59;

        end;

        p in ( Upper_Arc C) by A13, JORDAN17: 3;

        then

         A19: LE (p,( E-max C),( Upper_Arc C),( W-min C),( E-max C)) by A6, JORDAN5C: 10;

        

         A20: ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) = ( Segment (( Upper_Arc C),( W-min C),( E-max C),p,( E-max C))) by Th14;

        then

         A21: ( E-max C) in ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) by A19, JORDAN16: 5;

        q in ( Lower_Arc C) by A14, JORDAN17: 4;

        then

         A22: LE (( E-max C),q,( Lower_Arc C),( E-max C),( W-min C)) by A7, JORDAN5C: 10;

        

         A23: ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) = ( Segment (( Lower_Arc C),( E-max C),( W-min C),( E-max C),q)) by Th15;

        then ( E-max C) in ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) by A22, JORDAN16: 5;

        then

         A24: ( E-max C) in (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) /\ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q))) by A21, XBOOLE_0:def 4;

        

         A25: ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) c= ( Upper_Arc C) by JORDAN6: 20;

        

         A26: ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) c= ( Lower_Arc C) by JORDAN6: 19;

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

        then

         A27: (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) /\ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q))) = {( E-max C)} by A16, A24, A25, A26, TOPREAL8: 1, XBOOLE_1: 27;

        

         A28: ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) is_an_arc_of (p,( E-max C)) by A6, A12, A19, A20, JORDAN16: 21;

        

         A29: ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) is_an_arc_of (( E-max C),q) by A7, A15, A22, A23, JORDAN16: 21;

        ( Segment (p,q,C)) = (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) \/ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q))) by A13, A14, Th12;

        hence thesis by A27, A28, A29, TOPREAL1: 2;

      end;

        suppose that

         A30: q = ( E-max C) and

         A31: LE (p,( E-max C),C) and

         A32: LE (( E-max C),q,C);

        p in ( Upper_Arc C) by A31, JORDAN17: 3;

        then

         A33: LE (p,( E-max C),( Upper_Arc C),( W-min C),( E-max C)) by A6, JORDAN5C: 10;

        

         A34: ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) = ( Segment (( Upper_Arc C),( W-min C),( E-max C),p,( E-max C))) by Th14;

        then

         A35: ( E-max C) in ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) by A33, JORDAN16: 5;

        

         A36: ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) = {( E-max C)} by A7, A30, JORDAN6: 21;

        ( Segment (p,q,C)) = (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) \/ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q))) by A31, A32, Th12

        .= ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) by A35, A36, ZFMISC_1: 40;

        hence thesis by A1, A6, A30, A33, A34, JORDAN16: 21;

      end;

        suppose that

         A37: p = ( E-max C) and

         A38: LE (p,( E-max C),C) and

         A39: LE (( E-max C),q,C);

        q in ( Lower_Arc C) by A39, JORDAN17: 4;

        then

         A40: LE (( E-max C),q,( Lower_Arc C),( E-max C),( W-min C)) by A7, JORDAN5C: 10;

        

         A41: ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) = ( Segment (( Lower_Arc C),( E-max C),( W-min C),( E-max C),q)) by Th15;

        then

         A42: ( E-max C) in ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) by A40, JORDAN16: 5;

        

         A43: ( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) = {( E-max C)} by A6, A37, JORDAN6: 23;

        ( Segment (p,q,C)) = (( R_Segment (( Upper_Arc C),( W-min C),( E-max C),p)) \/ ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q))) by A38, A39, Th12

        .= ( L_Segment (( Lower_Arc C),( E-max C),( W-min C),q)) by A42, A43, ZFMISC_1: 40;

        hence thesis by A1, A7, A37, A40, A41, JORDAN16: 21;

      end;

        suppose that

         A44: LE (( E-max C),p,C) and

         A45: not LE (p,( E-max C),C);

        

         A46: ( Segment (p,q,C)) = ( Segment (( Lower_Arc C),( E-max C),( W-min C),p,q)) by A2, A44, Th11;

         not p in ( Upper_Arc C) by A45, Th6;

        then LE (p,q,( Lower_Arc C),( E-max C),( W-min C)) by A2, JORDAN6:def 10;

        hence thesis by A1, A7, A46, JORDAN16: 21;

      end;

    end;

    theorem :: JORDAN_A:18

    

     Th18: C = ( Segment (( W-min C),( W-min C),C))

    proof

      set X = { p : LE (( W-min C),p,C) or ( W-min C) in C & p = ( W-min C) };

      

       A1: ( Segment (( W-min C),( W-min C),C)) = X by JORDAN7:def 1;

      thus C c= ( Segment (( W-min C),( W-min C),C))

      proof

        let e be object;

        assume

         A2: e in C;

        then

        reconsider p = e as Point of ( TOP-REAL 2);

         LE (( W-min C),p,C) by A2, JORDAN7: 3;

        hence thesis by A1;

      end;

      thus thesis by JORDAN16: 6;

    end;

    theorem :: JORDAN_A:19

    

     Th19: for q be Point of ( TOP-REAL 2) st q in C holds ( Segment (q,( W-min C),C)) is compact

    proof

      let q be Point of ( TOP-REAL 2) such that

       A1: q in C;

      per cases ;

        suppose q = ( W-min C);

        hence thesis by Th18;

      end;

        suppose q <> ( W-min C);

        hence thesis by A1, Th16, JORDAN5A: 1;

      end;

    end;

    theorem :: JORDAN_A:20

    

     Th20: for q1,q2 be Point of ( TOP-REAL 2) st LE (q1,q2,C) holds ( Segment (q1,q2,C)) is compact

    proof

      let q1,q2 be Point of ( TOP-REAL 2) such that

       A1: LE (q1,q2,C);

      

       A2: q1 in C by A1, JORDAN7: 5;

      per cases ;

        suppose q2 = ( W-min C);

        hence thesis by A2, Th19;

      end;

        suppose q1 = q2 & q2 <> ( W-min C);

        then ( Segment (q1,q2,C)) = {q1} by A2, JORDAN7: 8;

        hence thesis;

      end;

        suppose q1 <> q2 & q2 <> ( W-min C);

        hence thesis by A1, Th17, JORDAN5A: 1;

      end;

    end;

    begin

    definition

      let C;

      :: JORDAN_A:def3

      mode Segmentation of C -> FinSequence of ( TOP-REAL 2) means

      : Def3: (it /. 1) = ( W-min C) & it is one-to-one & 8 <= ( len it ) & ( rng it ) c= C & (for i be Nat st 1 <= i & i < ( len it ) holds LE ((it /. i),(it /. (i + 1)),C)) & (for i be Nat st 1 <= i & (i + 1) < ( len it ) holds (( Segment ((it /. i),(it /. (i + 1)),C)) /\ ( Segment ((it /. (i + 1)),(it /. (i + 2)),C))) = {(it /. (i + 1))}) & (( Segment ((it /. ( len it )),(it /. 1),C)) /\ ( Segment ((it /. 1),(it /. 2),C))) = {(it /. 1)} & (( Segment ((it /. (( len it ) -' 1)),(it /. ( len it )),C)) /\ ( Segment ((it /. ( len it )),(it /. 1),C))) = {(it /. ( len it ))} & ( Segment ((it /. (( len it ) -' 1)),(it /. ( len it )),C)) misses ( Segment ((it /. 1),(it /. 2),C)) & (for i,j be Nat st 1 <= i & i < j & j < ( len it ) & (i,j) aren't_adjacent holds ( Segment ((it /. i),(it /. (i + 1)),C)) misses ( Segment ((it /. j),(it /. (j + 1)),C))) & for i be Nat st 1 < i & (i + 1) < ( len it ) holds ( Segment ((it /. ( len it )),(it /. 1),C)) misses ( Segment ((it /. i),(it /. (i + 1)),C));

      existence

      proof

        consider h be FinSequence of the carrier of ( TOP-REAL 2) such that

         A1: (h . 1) = ( W-min C) and

         A2: h is one-to-one and

         A3: 8 <= ( len h) and

         A4: ( rng h) c= C and

         A5: for i be Nat st 1 <= i & i < ( len h) holds LE ((h /. i),(h /. (i + 1)),C) and for i be Nat, W be Subset of ( Euclid 2) st 1 <= i & i < ( len h) & W = ( Segment ((h /. i),(h /. (i + 1)),C)) holds ( diameter W) < 1 and for W be Subset of ( Euclid 2) st W = ( Segment ((h /. ( len h)),(h /. 1),C)) holds ( diameter W) < 1 and

         A6: for i be Nat st 1 <= i & (i + 1) < ( len h) holds (( Segment ((h /. i),(h /. (i + 1)),C)) /\ ( Segment ((h /. (i + 1)),(h /. (i + 2)),C))) = {(h /. (i + 1))} and

         A7: (( Segment ((h /. ( len h)),(h /. 1),C)) /\ ( Segment ((h /. 1),(h /. 2),C))) = {(h /. 1)} and

         A8: (( Segment ((h /. (( len h) -' 1)),(h /. ( len h)),C)) /\ ( Segment ((h /. ( len h)),(h /. 1),C))) = {(h /. ( len h))} and

         A9: ( Segment ((h /. (( len h) -' 1)),(h /. ( len h)),C)) misses ( Segment ((h /. 1),(h /. 2),C)) and

         A10: for i,j be Nat st 1 <= i & i < j & j < ( len h) & (i,j) aren't_adjacent holds ( Segment ((h /. i),(h /. (i + 1)),C)) misses ( Segment ((h /. j),(h /. (j + 1)),C)) and

         A11: for i be Nat st 1 < i & (i + 1) < ( len h) holds ( Segment ((h /. ( len h)),(h /. 1),C)) misses ( Segment ((h /. i),(h /. (i + 1)),C)) by JORDAN7: 20;

        reconsider h as non empty FinSequence of the carrier of ( TOP-REAL 2) by A3, CARD_1: 27;

        take h;

        1 in ( dom h) by FINSEQ_5: 6;

        hence (h /. 1) = ( W-min C) by A1, PARTFUN1:def 6;

        thus h is one-to-one by A2;

        thus 8 <= ( len h) by A3;

        thus ( rng h) c= C by A4;

        thus for i be Nat st 1 <= i & i < ( len h) holds LE ((h /. i),(h /. (i + 1)),C) by A5;

        thus for i be Nat st 1 <= i & (i + 1) < ( len h) holds (( Segment ((h /. i),(h /. (i + 1)),C)) /\ ( Segment ((h /. (i + 1)),(h /. (i + 2)),C))) = {(h /. (i + 1))} by A6;

        thus (( Segment ((h /. ( len h)),(h /. 1),C)) /\ ( Segment ((h /. 1),(h /. 2),C))) = {(h /. 1)} by A7;

        thus (( Segment ((h /. (( len h) -' 1)),(h /. ( len h)),C)) /\ ( Segment ((h /. ( len h)),(h /. 1),C))) = {(h /. ( len h))} by A8;

        thus ( Segment ((h /. (( len h) -' 1)),(h /. ( len h)),C)) misses ( Segment ((h /. 1),(h /. 2),C)) by A9;

        thus for i,j be Nat st 1 <= i & i < j & j < ( len h) & (i,j) aren't_adjacent holds ( Segment ((h /. i),(h /. (i + 1)),C)) misses ( Segment ((h /. j),(h /. (j + 1)),C)) by A10;

        thus thesis by A11;

      end;

    end

    registration

      let C;

      cluster -> non trivial for Segmentation of C;

      coherence

      proof

        let S be Segmentation of C;

        ( len S) >= 8 by Def3;

        then ( len S) >= 2 by XXREAL_0: 2;

        hence thesis by NAT_D: 60;

      end;

    end

    theorem :: JORDAN_A:21

    

     Th21: for S be Segmentation of C, i st 1 <= i & i <= ( len S) holds (S /. i) in C

    proof

      let S be Segmentation of C, i;

      assume that

       A1: 1 <= i and

       A2: i <= ( len S);

      i in ( dom S) by A1, A2, FINSEQ_3: 25;

      then

       A3: (S /. i) in ( rng S) by PARTFUN2: 2;

      ( rng S) c= C by Def3;

      hence thesis by A3;

    end;

    begin

    definition

      let C;

      let i be Nat;

      let S be Segmentation of C;

      :: JORDAN_A:def4

      func Segm (S,i) -> Subset of ( TOP-REAL 2) equals

      : Def4: ( Segment ((S /. i),(S /. (i + 1)),C)) if 1 <= i & i < ( len S)

      otherwise ( Segment ((S /. ( len S)),(S /. 1),C));

      correctness ;

    end

    theorem :: JORDAN_A:22

    for S be Segmentation of C st i in ( dom S) holds ( Segm (S,i)) c= C

    proof

      let S be Segmentation of C;

      assume i in ( dom S);

      then

       A1: 1 <= i by FINSEQ_3: 25;

      i < ( len S) or i >= ( len S);

      then ( Segm (S,i)) = ( Segment ((S /. i),(S /. (i + 1)),C)) or ( Segm (S,i)) = ( Segment ((S /. ( len S)),(S /. 1),C)) by A1, Def4;

      hence thesis by JORDAN16: 6;

    end;

    registration

      let C;

      let S be Segmentation of C, i;

      cluster ( Segm (S,i)) -> non empty compact;

      coherence

      proof

        per cases ;

          suppose

           A1: 1 <= i & i < ( len S);

          then

           A2: ( Segm (S,i)) = ( Segment ((S /. i),(S /. (i + 1)),C)) by Def4;

           LE ((S /. i),(S /. (i + 1)),C) by A1, Def3;

          hence thesis by A2, Th20, JORDAN7: 6;

        end;

          suppose not (1 <= i & i < ( len S));

          then

           A3: ( Segm (S,i)) = ( Segment ((S /. ( len S)),(S /. 1),C)) by Def4;

          8 <= ( len S) by Def3;

          then 1 <= ( len S) by XXREAL_0: 2;

          then

           A4: (S /. ( len S)) in C by Th21;

          (S /. 1) = ( W-min C) by Def3;

          hence thesis by A3, A4, Th19, JORDAN16: 19;

        end;

      end;

    end

    theorem :: JORDAN_A:23

    for S be Segmentation of C, p st p in C holds ex i be Nat st i in ( dom S) & p in ( Segm (S,i))

    proof

      let S be Segmentation of C, p such that

       A1: p in C;

      set X = { i : i in ( dom S) & LE ((S /. i),p,C) };

      

       A2: X c= ( dom S)

      proof

        let e be object;

        assume e in X;

        then ex i st e = i & i in ( dom S) & LE ((S /. i),p,C);

        hence thesis;

      end;

      

       A3: 1 in ( dom S) by FINSEQ_5: 6;

      

       A4: ( W-min C) = (S /. 1) by Def3;

      then LE ((S /. 1),p,C) by A1, JORDAN7: 3;

      then 1 in X by A3;

      then

      reconsider X as finite non empty Subset of NAT by A2, XBOOLE_1: 1;

      reconsider mX = ( max X) as Nat by TARSKI: 1;

      take mX;

      

       A5: ( max X) in X by XXREAL_2:def 8;

      hence mX in ( dom S) by A2;

      

       A6: 1 <= ( max X) by A2, A5, FINSEQ_3: 25;

      

       A7: ( max X) <= ( len S) by A2, A5, FINSEQ_3: 25;

      

       A8: ex i st ( max X) = i & i in ( dom S) & LE ((S /. i),p,C) by A5;

      per cases by A7, XXREAL_0: 1;

        suppose

         A9: ( max X) < ( len S);

        

         A10: 1 <= (( max X) + 1) by NAT_1: 11;

        (( max X) + 1) <= ( len S) by A9, NAT_1: 13;

        then

         A11: (mX + 1) in ( dom S) by A10, FINSEQ_3: 25;

        

         A12: S is one-to-one by Def3;

        (( max X) + 1) >= (1 + 1) by A6, XREAL_1: 6;

        then (( max X) + 1) <> 1;

        then

         A13: (S /. (( max X) + 1)) <> (S /. 1) by A3, A11, A12, PARTFUN2: 10;

        

         A14: (S /. (( max X) + 1)) in ( rng S) by A11, PARTFUN2: 2;

        

         A15: ( rng S) c= C by Def3;

        now

          assume LE ((S /. (( max X) + 1)),p,C);

          then (( max X) + 1) in X by A11;

          then (( max X) + 1) <= ( max X) by XXREAL_2:def 8;

          hence contradiction by XREAL_1: 29;

        end;

        then LE (p,(S /. (( max X) + 1)),C) by A1, A14, A15, JORDAN16: 7;

        then p in { p1 : LE ((S /. ( max X)),p1,C) & LE (p1,(S /. (( max X) + 1)),C) } by A8;

        then p in ( Segment ((S /. ( max X)),(S /. (( max X) + 1)),C)) by A4, A13, JORDAN7:def 1;

        hence thesis by A6, A9, Def4;

      end;

        suppose

         A16: ( max X) = ( len S);

        now

          per cases ;

            case p <> ( W-min C);

            thus LE ((S /. ( len S)),p,C) by A8, A16;

          end;

            case p = ( W-min C);

            

             A17: (S /. ( len S)) in ( rng S) by FINSEQ_6: 168;

            ( rng S) c= C by Def3;

            hence (S /. ( len S)) in C by A17;

          end;

        end;

        then p in { p1 : LE ((S /. ( len S)),p1,C) or (S /. ( len S)) in C & p1 = ( W-min C) };

        then p in ( Segment ((S /. ( len S)),(S /. 1),C)) by A4, JORDAN7:def 1;

        hence thesis by A16, Def4;

      end;

    end;

    theorem :: JORDAN_A:24

    

     Th24: for S be Segmentation of C holds for i, j st 1 <= i & i < j & j < ( len S) & (i,j) aren't_adjacent holds ( Segm (S,i)) misses ( Segm (S,j))

    proof

      let S be Segmentation of C;

      let i, j such that

       A1: 1 <= i and

       A2: i < j and

       A3: j < ( len S) and

       A4: (i,j) aren't_adjacent ;

      i < ( len S) by A2, A3, XXREAL_0: 2;

      then

       A5: ( Segm (S,i)) = ( Segment ((S /. i),(S /. (i + 1)),C)) by A1, Def4;

      1 < j by A1, A2, XXREAL_0: 2;

      then ( Segm (S,j)) = ( Segment ((S /. j),(S /. (j + 1)),C)) by A3, Def4;

      hence thesis by A1, A2, A3, A4, A5, Def3;

    end;

    theorem :: JORDAN_A:25

    

     Th25: for S be Segmentation of C holds for j st 1 < j & j < (( len S) -' 1) holds ( Segm (S,( len S))) misses ( Segm (S,j))

    proof

      let S be Segmentation of C;

      let j such that

       A1: 1 < j and

       A2: j < (( len S) -' 1);

      

       A3: ( Segm (S,( len S))) = ( Segment ((S /. ( len S)),(S /. 1),C)) by Def4;

      

       A4: (j + 1) < ( len S) by A2, NAT_D: 53;

      j < ( len S) by A2, NAT_D: 44;

      then ( Segm (S,j)) = ( Segment ((S /. j),(S /. (j + 1)),C)) by A1, Def4;

      hence thesis by A1, A3, A4, Def3;

    end;

    theorem :: JORDAN_A:26

    

     Th26: for S be Segmentation of C holds for i, j st 1 <= i & i < j & j < ( len S) & (i,j) are_adjacent holds (( Segm (S,i)) /\ ( Segm (S,j))) = {(S /. (i + 1))}

    proof

      let S be Segmentation of C;

      let i, j such that

       A1: 1 <= i and

       A2: i < j and

       A3: j < ( len S) and

       A4: (i,j) are_adjacent ;

      i < ( len S) by A2, A3, XXREAL_0: 2;

      then

       A5: ( Segm (S,i)) = ( Segment ((S /. i),(S /. (i + 1)),C)) by A1, Def4;

      1 < j by A1, A2, XXREAL_0: 2;

      then

       A6: ( Segm (S,j)) = ( Segment ((S /. j),(S /. (j + 1)),C)) by A3, Def4;

      (j + 1) > i by A2, NAT_1: 13;

      then j = (i + 1) by A4, GOBRD10:def 1;

      then (j + 1) = (i + (1 + 1));

      hence thesis by A1, A3, A5, A6, Def3;

    end;

    theorem :: JORDAN_A:27

    

     Th27: for S be Segmentation of C holds for i, j st 1 <= i & i < j & j < ( len S) & (i,j) are_adjacent holds ( Segm (S,i)) meets ( Segm (S,j))

    proof

      let S be Segmentation of C;

      let i, j;

      assume that

       A1: 1 <= i and

       A2: i < j and

       A3: j < ( len S) and

       A4: (i,j) are_adjacent ;

      (( Segm (S,i)) /\ ( Segm (S,j))) = {(S /. (i + 1))} by A1, A2, A3, A4, Th26;

      hence thesis;

    end;

    theorem :: JORDAN_A:28

    

     Th28: for S be Segmentation of C holds (( Segm (S,( len S))) /\ ( Segm (S,1))) = {(S /. 1)}

    proof

      let S be Segmentation of C;

      

       A1: ( Segm (S,( len S))) = ( Segment ((S /. ( len S)),(S /. 1),C)) by Def4;

      ( len S) >= 8 by Def3;

      then 1 < ( len S) by XXREAL_0: 2;

      then ( Segm (S,1)) = ( Segment ((S /. 1),(S /. (1 + 1)),C)) by Def4;

      hence thesis by A1, Def3;

    end;

    theorem :: JORDAN_A:29

    

     Th29: for S be Segmentation of C holds ( Segm (S,( len S))) meets ( Segm (S,1))

    proof

      let S be Segmentation of C;

      (( Segm (S,( len S))) /\ ( Segm (S,1))) = {(S /. 1)} by Th28;

      hence thesis;

    end;

    theorem :: JORDAN_A:30

    

     Th30: for S be Segmentation of C holds (( Segm (S,( len S))) /\ ( Segm (S,(( len S) -' 1)))) = {(S /. ( len S))}

    proof

      let S be Segmentation of C;

      

       A1: ( Segm (S,( len S))) = ( Segment ((S /. ( len S)),(S /. 1),C)) by Def4;

      

       A2: ( len S) >= 8 by Def3;

      then ( len S) >= (1 + 1) by XXREAL_0: 2;

      then

       A3: 1 <= (( len S) -' 1) by NAT_D: 55;

      

       A4: ((( len S) -' 1) + 1) = ( len S) by A2, XREAL_1: 235, XXREAL_0: 2;

      then (( len S) -' 1) < ( len S) by NAT_1: 13;

      then ( Segm (S,(( len S) -' 1))) = ( Segment ((S /. (( len S) -' 1)),(S /. ( len S)),C)) by A3, A4, Def4;

      hence thesis by A1, Def3;

    end;

    theorem :: JORDAN_A:31

    

     Th31: for S be Segmentation of C holds ( Segm (S,( len S))) meets ( Segm (S,(( len S) -' 1)))

    proof

      let S be Segmentation of C;

      (( Segm (S,( len S))) /\ ( Segm (S,(( len S) -' 1)))) = {(S /. ( len S))} by Th30;

      hence thesis;

    end;

    begin

    definition

      let n;

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

      :: JORDAN_A:def5

      func diameter C -> Real means

      : Def5: ex W be Subset of ( Euclid n) st W = C & it = ( diameter W);

      existence

      proof

         the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8

        .= TopStruct (# the carrier of ( Euclid n), ( Family_open_set ( Euclid n)) #) by PCOMPS_1:def 5;

        then

        reconsider W = C as Subset of ( Euclid n);

        take ( diameter W), W;

        thus thesis;

      end;

      correctness ;

    end

    definition

      let C;

      let S be Segmentation of C;

      :: JORDAN_A:def6

      func diameter S -> Real means

      : Def6: ex S1 be non empty finite Subset of REAL st S1 = { ( diameter ( Segm (S,i))) where i be Element of NAT : i in ( dom S) } & it = ( max S1);

      existence

      proof

        deffunc F( Nat) = ( In (( diameter ( Segm (S,$1))), REAL ));

        defpred P[ set] means $1 in ( dom S);

        set S1 = { F(i) where i be Element of NAT : P[i] };

        set S2 = { F(i) where i be Element of NAT : i in ( dom S) };

        

         A1: ( dom S) is finite;

        

         A2: S2 is finite from FRAENKEL:sch 21( A1);

        

         A3: S1 is Subset of REAL from DOMAIN_1:sch 8;

        1 in ( dom S) by FINSEQ_5: 6;

        then F() in S1;

        then

        reconsider S1 as non empty finite Subset of REAL by A2, A3;

        reconsider mS1 = ( max S1) as Real;

        take mS1, S1;

        deffunc G( Nat) = ( diameter ( Segm (S,$1)));

        

         A4: for i be Element of NAT holds F(i) = G(i);

        { F(i) where i be Element of NAT : P[i] } = { G(j) where j be Element of NAT : P[j] } from FRAENKEL:sch 5( A4);

        hence thesis;

      end;

      correctness ;

    end

    theorem :: JORDAN_A:32

    for S be Segmentation of C, i holds ( diameter ( Segm (S,i))) <= ( diameter S)

    proof

      let S be Segmentation of C, i;

      consider S1 be non empty finite Subset of REAL such that

       A1: S1 = { ( diameter ( Segm (S,j))) where j be Element of NAT : j in ( dom S) } and

       A2: ( diameter S) = ( max S1) by Def6;

      per cases ;

        suppose 1 <= i & i < ( len S);

        then i in ( dom S) by FINSEQ_3: 25;

        then ( diameter ( Segm (S,i))) in S1 by A1;

        hence thesis by A2, XXREAL_2:def 8;

      end;

        suppose

         A3: not (1 <= i & i < ( len S));

        

         A4: ( Segm (S,( len S))) = ( Segment ((S /. ( len S)),(S /. 1),C)) by Def4

        .= ( Segm (S,i)) by A3, Def4;

        ( len S) in ( dom S) by FINSEQ_5: 6;

        then ( diameter ( Segm (S,i))) in S1 by A1, A4;

        hence thesis by A2, XXREAL_2:def 8;

      end;

    end;

    theorem :: JORDAN_A:33

    

     Th33: for S be Segmentation of C, e be Real st for i holds ( diameter ( Segm (S,i))) < e holds ( diameter S) < e

    proof

      let S be Segmentation of C, e be Real such that

       A1: for i holds ( diameter ( Segm (S,i))) < e;

      consider S1 be non empty finite Subset of REAL such that

       A2: S1 = { ( diameter ( Segm (S,i))) where i be Element of NAT : i in ( dom S) } and

       A3: ( diameter S) = ( max S1) by Def6;

      ( diameter S) in S1 by A3, XXREAL_2:def 8;

      then ex i be Element of NAT st ( diameter S) = ( diameter ( Segm (S,i))) & i in ( dom S) by A2;

      hence thesis by A1;

    end;

    theorem :: JORDAN_A:34

    for e be Real st e > 0 holds ex S be Segmentation of C st ( diameter S) < e

    proof

      let e be Real;

      assume e > 0 ;

      then

      consider h be FinSequence of the carrier of ( TOP-REAL 2) such that

       A1: (h . 1) = ( W-min C) and

       A2: h is one-to-one and

       A3: 8 <= ( len h) and

       A4: ( rng h) c= C and

       A5: for i be Nat st 1 <= i & i < ( len h) holds LE ((h /. i),(h /. (i + 1)),C) and

       A6: for i be Nat, W be Subset of ( Euclid 2) st 1 <= i & i < ( len h) & W = ( Segment ((h /. i),(h /. (i + 1)),C)) holds ( diameter W) < e and

       A7: for W be Subset of ( Euclid 2) st W = ( Segment ((h /. ( len h)),(h /. 1),C)) holds ( diameter W) < e and

       A8: for i be Nat st 1 <= i & (i + 1) < ( len h) holds (( Segment ((h /. i),(h /. (i + 1)),C)) /\ ( Segment ((h /. (i + 1)),(h /. (i + 2)),C))) = {(h /. (i + 1))} and

       A9: (( Segment ((h /. ( len h)),(h /. 1),C)) /\ ( Segment ((h /. 1),(h /. 2),C))) = {(h /. 1)} and

       A10: (( Segment ((h /. (( len h) -' 1)),(h /. ( len h)),C)) /\ ( Segment ((h /. ( len h)),(h /. 1),C))) = {(h /. ( len h))} and

       A11: ( Segment ((h /. (( len h) -' 1)),(h /. ( len h)),C)) misses ( Segment ((h /. 1),(h /. 2),C)) and

       A12: for i,j be Nat st 1 <= i & i < j & j < ( len h) & (i,j) aren't_adjacent holds ( Segment ((h /. i),(h /. (i + 1)),C)) misses ( Segment ((h /. j),(h /. (j + 1)),C)) and

       A13: for i be Nat st 1 < i & (i + 1) < ( len h) holds ( Segment ((h /. ( len h)),(h /. 1),C)) misses ( Segment ((h /. i),(h /. (i + 1)),C)) by JORDAN7: 20;

      h <> {} by A3, CARD_1: 27;

      then 1 in ( dom h) by FINSEQ_5: 6;

      then (h /. 1) = ( W-min C) by A1, PARTFUN1:def 6;

      then

      reconsider h as Segmentation of C by A2, A3, A4, A5, A8, A9, A10, A11, A12, A13, Def3;

      take h;

      ( diameter ( Segm (h,i))) < e

      proof

        

         A14: ex W be Subset of ( Euclid 2) st (W = ( Segm (h,i))) & (( diameter ( Segm (h,i))) = ( diameter W)) by Def5;

        per cases ;

          suppose

           A15: 1 <= i & i < ( len h);

          then ( Segm (h,i)) = ( Segment ((h /. i),(h /. (i + 1)),C)) by Def4;

          hence thesis by A6, A14, A15;

        end;

          suppose not (1 <= i & i < ( len h));

          then ( Segm (h,i)) = ( Segment ((h /. ( len h)),(h /. 1),C)) by Def4;

          hence thesis by A7, A14;

        end;

      end;

      hence thesis by Th33;

    end;

    begin

    definition

      let C;

      let S be Segmentation of C;

      :: JORDAN_A:def7

      func S-Gap S -> Real means

      : Def7: ex S1,S2 be non empty finite Subset of REAL st S1 = { ( dist_min (( Segm (S,i)),( Segm (S,j)))) where i,j be Element of NAT : 1 <= i & i < j & j < ( len S) & (i,j) aren't_adjacent } & S2 = { ( dist_min (( Segm (S,( len S))),( Segm (S,k)))) where k be Element of NAT : 1 < k & k < (( len S) -' 1) } & it = ( min (( min S1),( min S2)));

      existence

      proof

        deffunc F( Nat) = ( dist_min (( Segm (S,( len S))),( Segm (S,$1))));

        deffunc F( Nat, Nat) = ( dist_min (( Segm (S,$1)),( Segm (S,$2))));

        defpred P[ Nat] means 1 < $1 & $1 < (( len S) -' 1);

        defpred Q[ Nat] means $1 in ( dom S);

        defpred R[ Nat, Nat] means 1 <= $1 & $1 < $2 & $2 < ( len S) & ($1,$2) aren't_adjacent ;

        defpred W[ Nat, Nat] means Q[$1] & Q[$2];

        set S1 = { F(i,j) where i,j be Element of NAT : R[i, j] };

        set S2 = { F(j) where j be Element of NAT : P[j] };

        set B = { F(i,j) where i,j be Element of NAT : W[i, j] };

        set B9 = { F(i,j) where i,j be Element of NAT : i in ( dom S) & j in ( dom S) };

        set A = { F(j) where j be Element of NAT : Q[j] };

        set A9 = { F(j) where j be Element of NAT : j in ( dom S) };

        

         A1: for j be Element of NAT st P[j] holds Q[j]

        proof

          let j be Element of NAT ;

          assume

           A2: 1 < j;

          

           A3: (( len S) -' 1) <= ( len S) by NAT_D: 35;

          assume j < (( len S) -' 1);

          then j < ( len S) by A3, XXREAL_0: 2;

          hence thesis by A2, FINSEQ_3: 25;

        end;

        

         A4: S2 c= A from FRAENKEL:sch 1( A1);

        

         A5: for i,j be Element of NAT holds R[i, j] implies W[i, j]

        proof

          let i,j be Element of NAT such that

           A6: 1 <= i and

           A7: i < j and

           A8: j < ( len S) and (i,j) aren't_adjacent ;

          i < ( len S) by A7, A8, XXREAL_0: 2;

          hence i in ( dom S) by A6, FINSEQ_3: 25;

          1 < j by A6, A7, XXREAL_0: 2;

          hence thesis by A8, FINSEQ_3: 25;

        end;

        

         A9: S1 c= B from FRAENKEL:sch 2( A5);

        

         A10: S1 c= REAL

        proof

          let x be object;

          assume x in S1;

          then ex i,j be Element of NAT st x = ( dist_min (( Segm (S,i)),( Segm (S,j)))) & 1 <= i & i < j & j < ( len S) & (i,j) aren't_adjacent ;

          hence thesis by XREAL_0:def 1;

        end;

        

         A11: S2 c= REAL

        proof

          let x be object;

          assume x in S2;

          then ex j be Element of NAT st x = ( dist_min (( Segm (S,( len S))),( Segm (S,j)))) & 1 < j & j < (( len S) -' 1);

          hence thesis by XREAL_0:def 1;

        end;

        

         A12: ( dom S) is finite;

        

         A13: A9 is finite from FRAENKEL:sch 21( A12);

        

         A14: B9 is finite from FRAENKEL:sch 22( A12, A12);

        

         A15: 3 <> (1 + 1);

        1 <> (3 + 1);

        then

         A16: (1,3) aren't_adjacent by A15, GOBRD10:def 1;

        

         A17: ( len S) >= (7 + 1) by Def3;

        then 3 < ( len S) by XXREAL_0: 2;

        then

         A18: ( dist_min (( Segm (S,1)),( Segm (S,3)))) in S1 by A16;

        (2 + 1) < ( len S) by A17, XXREAL_0: 2;

        then 2 < (( len S) -' 1) by NAT_D: 52;

        then ( dist_min (( Segm (S,( len S))),( Segm (S,2)))) in S2;

        then

        reconsider S1, S2 as non empty finite Subset of REAL by A4, A9, A10, A11, A13, A14, A18;

        reconsider mm = ( min (( min S1),( min S2))) as Element of REAL by XREAL_0:def 1;

        take mm, S1, S2;

        thus thesis;

      end;

      correctness ;

    end

    theorem :: JORDAN_A:35

    

     Th35: for S be Segmentation of C holds ex F be finite non empty Subset of REAL st F = { ( dist_min (( Segm (S,i)),( Segm (S,j)))) : 1 <= i & i < j & j <= ( len S) & ( Segm (S,i)) misses ( Segm (S,j)) } & ( S-Gap S) = ( min F)

    proof

      let S be Segmentation of C;

      consider S1,S2 be non empty finite Subset of REAL such that

       A1: S1 = { ( dist_min (( Segm (S,i)),( Segm (S,j)))) where i,j be Element of NAT : 1 <= i & i < j & j < ( len S) & (i,j) aren't_adjacent } and

       A2: S2 = { ( dist_min (( Segm (S,( len S))),( Segm (S,k)))) where k be Element of NAT : 1 < k & k < (( len S) -' 1) } and

       A3: ( S-Gap S) = ( min (( min S1),( min S2))) by Def7;

      take F = (S1 \/ S2);

      set X = { ( dist_min (( Segm (S,i)),( Segm (S,j)))) : 1 <= i & i < j & j <= ( len S) & ( Segm (S,i)) misses ( Segm (S,j)) };

      thus F c= X

      proof

        let e be object;

        assume

         A4: e in F;

        per cases by A4, XBOOLE_0:def 3;

          suppose e in S1;

          then

          consider i,j be Element of NAT such that

           A5: e = ( dist_min (( Segm (S,i)),( Segm (S,j)))) and

           A6: 1 <= i and

           A7: i < j and

           A8: j < ( len S) and

           A9: (i,j) aren't_adjacent by A1;

          ( Segm (S,i)) misses ( Segm (S,j)) by A6, A7, A8, A9, Th24;

          hence thesis by A5, A6, A7, A8;

        end;

          suppose e in S2;

          then

          consider j be Element of NAT such that

           A10: e = ( dist_min (( Segm (S,( len S))),( Segm (S,j)))) and

           A11: 1 < j and

           A12: j < (( len S) -' 1) by A2;

          

           A13: j < ( len S) by A12, NAT_D: 44;

          ( Segm (S,( len S))) misses ( Segm (S,j)) by A11, A12, Th25;

          hence thesis by A10, A11, A13;

        end;

      end;

      thus X c= F

      proof

        let e be object;

        assume e in X;

        then

        consider i, j such that

         A14: e = ( dist_min (( Segm (S,i)),( Segm (S,j)))) and

         A15: 1 <= i and

         A16: i < j and

         A17: j <= ( len S) and

         A18: ( Segm (S,i)) misses ( Segm (S,j));

        

         A19: i < ( len S) by A16, A17, XXREAL_0: 2;

        

         A20: i in NAT & j in NAT by ORDINAL1:def 12;

        per cases by A17, XXREAL_0: 1;

          suppose that

           A21: j < ( len S);

          (i,j) aren't_adjacent by A15, A16, A18, A21, Th27;

          then e in S1 by A1, A14, A15, A16, A21, A20;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose

           A22: j = ( len S);

          then 1 <> i by A18, Th29;

          then

           A23: 1 < i by A15, XXREAL_0: 1;

          

           A24: i <= (( len S) -' 1) by A19, NAT_D: 49;

          i <> (( len S) -' 1) by A18, A22, Th31;

          then i < (( len S) -' 1) by A24, XXREAL_0: 1;

          then e in S2 by A2, A14, A22, A23, A20;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      thus thesis by A3, XXREAL_2: 9;

    end;

    theorem :: JORDAN_A:36

    for S be Segmentation of C holds ( S-Gap S) > 0

    proof

      let S be Segmentation of C;

      consider F be finite non empty Subset of REAL such that

       A1: F = { ( dist_min (( Segm (S,i)),( Segm (S,j)))) : 1 <= i & i < j & j <= ( len S) & ( Segm (S,i)) misses ( Segm (S,j)) } and

       A2: ( S-Gap S) = ( min F) by Th35;

      ( S-Gap S) in F by A2, XXREAL_2:def 7;

      then ex i, j st ( S-Gap S) = ( dist_min (( Segm (S,i)),( Segm (S,j)))) & 1 <= i & i < j & j <= ( len S) & ( Segm (S,i)) misses ( Segm (S,j)) by A1;

      hence thesis by Th7;

    end;