jordan1h.miz



    begin

    reserve m,k,j,j1,i,i1,i2,n for Nat,

r,s for Real,

C for compact non vertical non horizontal Subset of ( TOP-REAL 2),

G for Go-board,

p for Point of ( TOP-REAL 2);

    registration

      let D be non empty with_non-empty_element set;

      cluster non empty non-empty for FinSequence of (D * );

      existence

      proof

        consider X be non empty set such that

         A1: X in D by SETFAM_1:def 10;

        

         A2: ( rng <* <*X*>*>) = { <*X*>} by FINSEQ_1: 39;

         <*X*> in (D * ) by A1, FUNCT_7: 18;

        then ( rng <* <*X*>*>) c= (D * ) by A2, ZFMISC_1: 31;

        then

        reconsider F = <* <*X*>*> as FinSequence of (D * ) by FINSEQ_1:def 4;

        take F;

        thus F is non empty;

        assume {} in ( rng F);

        hence thesis by A2;

      end;

    end

    registration

      let F be non-empty Function-yielding Function;

      cluster ( rngs F) -> non-empty;

      coherence

      proof

        now

          let n be object;

          assume n in ( dom ( rngs F));

          then n in ( dom F) by FUNCT_6: 60;

          then (( rngs F) . n) = ( rng (F . n)) & (F . n) is non empty by FUNCT_1:def 9, FUNCT_6: 22;

          hence (( rngs F) . n) is non empty;

        end;

        hence thesis by FUNCT_1:def 9;

      end;

    end

    theorem :: JORDAN1H:1

    

     Th1: for p,q be Point of ( TOP-REAL 2) st p <> q holds p in ( Cl (( LSeg (p,q)) \ {p, q}))

    proof

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

       A1: p <> q;

      for G be Subset of ( TOP-REAL 2) st G is open holds p in G implies (( LSeg (p,q)) \ {p, q}) meets G

      proof

        reconsider x = p, y = q as Point of ( Euclid 2) by TOPREAL3: 8;

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

         A2: G is open and

         A3: p in G;

        

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

        then

        reconsider P = G as Subset of ( TopSpaceMetr ( Euclid 2));

        P is open by A2, A4, PRE_TOPC: 30;

        then

        consider r be Real such that

         A5: r > 0 and

         A6: ( Ball (x,r)) c= P by A3, TOPMETR: 15;

        reconsider r as Real;

        

         A7: (r / 2) > 0 by A5, XREAL_1: 139;

        set t = ( min ((r / 2),(( dist (x,y)) / 2))), s = (t / ( dist (x,y)));

        set pp = (((1 - s) * p) + (s * q));

        reconsider z = pp as Point of ( Euclid 2) by TOPREAL3: 8;

        reconsider x9 = x, y9 = y, z9 = z as Element of ( REAL 2);

        reconsider a = x9, b = y9 as Element of (2 -tuples_on REAL );

        reconsider u = (a - b) as Element of ( REAL 2);

        

         A8: 0 < ( dist (x,y)) by A1, METRIC_1: 7;

        then 0 < (( dist (x,y)) / 2) by XREAL_1: 139;

        then

         A9: 0 < t by A7, XXREAL_0: 21;

        ( dist (x,z)) = |.(x9 - z9).| by SPPOL_1: 5

        .= |.((a - ((1 - s) * a)) - (s * b)).| by RVSUM_1: 39

        .= |.(((1 * a) - ((1 - s) * a)) - (s * b)).| by RVSUM_1: 52

        .= |.(((1 * a) + ((( - 1) * (1 - s)) * a)) - (s * b)).| by RVSUM_1: 49

        .= |.(((1 + ( - (1 - s))) * a) - (s * b)).| by RVSUM_1: 50

        .= |.((s * a) + ((( - 1) * s) * b)).| by RVSUM_1: 49

        .= |.((s * a) + (s * (( - 1) * b))).| by RVSUM_1: 49

        .= |.(s * (a + (( - 1) * b))).| by RVSUM_1: 51

        .= |.(s * (a + ( - b))).|

        .= |.(s * (a - b)).|

        .= ( |.s.| * |.u.|) by EUCLID: 11

        .= (s * |.(a - b).|) by A8, A9, ABSVALUE:def 1

        .= (s * ( dist (x,y))) by SPPOL_1: 5

        .= t by A8, XCMPLX_1: 87;

        then

         A10: ( dist (x,z)) <= (r / 2) by XXREAL_0: 17;

        (r / 2) < (r / 1) by A5, XREAL_1: 76;

        then ( dist (x,z)) < r by A10, XXREAL_0: 2;

        then

         A11: z in ( Ball (x,r)) by METRIC_1: 11;

        

         A12: (((1 - s) * p) + (s * p)) = (((1 - s) + s) * p) by RLVECT_1:def 6

        .= p by RLVECT_1:def 8;

        t <= (( dist (x,y)) / 2) & (( dist (x,y)) / 2) < (( dist (x,y)) / 1) by A8, XREAL_1: 76, XXREAL_0: 17;

        then

         A13: t < ( dist (x,y)) by XXREAL_0: 2;

        then s < 1 by A9, XREAL_1: 189;

        then

         A14: pp in ( LSeg (p,q)) by A8, A9;

        

         A15: (((1 - s) * q) + (s * q)) = (((1 - s) + s) * q) by RLVECT_1:def 6

        .= q by RLVECT_1:def 8;

        

         A16: (1 - s) <> 0 by A9, A13, XREAL_1: 189;

         A17:

        now

          assume pp = q;

          

          then ((1 - s) * q) = (pp - (s * q)) by A15, RLVECT_4: 1

          .= ((1 - s) * p) by RLVECT_4: 1;

          hence contradiction by A1, A16, RLVECT_1: 36;

        end;

        

         A18: 0 < s by A8, A9, XREAL_1: 139;

        now

          assume pp = p;

          

          then (s * p) = (pp - ((1 - s) * p)) by A12, RLVECT_4: 1

          .= (s * q) by RLVECT_4: 1;

          hence contradiction by A1, A18, RLVECT_1: 36;

        end;

        then not pp in {p, q} by A17, TARSKI:def 2;

        then pp in (( LSeg (p,q)) \ {p, q}) by A14, XBOOLE_0:def 5;

        hence thesis by A6, A11, XBOOLE_0: 3;

      end;

      hence thesis by TOPS_1: 12;

    end;

    theorem :: JORDAN1H:2

    

     Th2: for p,q be Point of ( TOP-REAL 2) st p <> q holds ( Cl (( LSeg (p,q)) \ {p, q})) = ( LSeg (p,q))

    proof

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

       A1: p <> q;

      ( Cl (( LSeg (p,q)) \ {p, q})) c= ( Cl ( LSeg (p,q))) by PRE_TOPC: 19, XBOOLE_1: 36;

      hence ( Cl (( LSeg (p,q)) \ {p, q})) c= ( LSeg (p,q)) by PRE_TOPC: 22;

      let e be object;

      p in ( LSeg (p,q)) & q in ( LSeg (p,q)) by RLTOPSP1: 68;

      then {p, q} c= ( LSeg (p,q)) by ZFMISC_1: 32;

      then

       A2: ( LSeg (p,q)) = ((( LSeg (p,q)) \ {p, q}) \/ {p, q}) by XBOOLE_1: 45;

      assume e in ( LSeg (p,q));

      then

       A3: e in (( LSeg (p,q)) \ {p, q}) or e in {p, q} by A2, XBOOLE_0:def 3;

      per cases by A3, TARSKI:def 2;

        suppose

         A4: e in (( LSeg (p,q)) \ {p, q});

        (( LSeg (p,q)) \ {p, q}) c= ( Cl (( LSeg (p,q)) \ {p, q})) by PRE_TOPC: 18;

        hence thesis by A4;

      end;

        suppose e = p or e = q;

        hence thesis by A1, Th1;

      end;

    end;

    theorem :: JORDAN1H:3

    for S be Subset of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2) st p <> q & (( LSeg (p,q)) \ {p, q}) c= S holds ( LSeg (p,q)) c= ( Cl S)

    proof

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

       A1: p <> q;

      assume (( LSeg (p,q)) \ {p, q}) c= S;

      then ( Cl (( LSeg (p,q)) \ {p, q})) c= ( Cl S) by PRE_TOPC: 19;

      hence thesis by A1, Th2;

    end;

    begin

    definition

      :: JORDAN1H:def1

      func RealOrd -> Relation of REAL equals { [r, s] : r <= s };

      coherence

      proof

        set R = { [r, s] : r <= s };

        R c= [: REAL , REAL :]

        proof

          let x be object;

          assume x in R;

          then

          consider r, s such that

           A1: x = [r, s] & r <= s;

          r in REAL & s in REAL by XREAL_0:def 1;

          hence thesis by A1, ZFMISC_1: 87;

        end;

        hence thesis;

      end;

    end

    theorem :: JORDAN1H:4

    

     Th4: [r, s] in RealOrd implies r <= s

    proof

      hereby

        assume [r, s] in RealOrd ;

        then

        consider r1,s1 be Real such that

         A1: [r, s] = [r1, s1] and

         A2: r1 <= s1;

        r = r1 by A1, XTUPLE_0: 1;

        hence r <= s by A1, A2, XTUPLE_0: 1;

      end;

    end;

    

     Lm1: RealOrd is_reflexive_in REAL ;

    

     Lm2: RealOrd is_antisymmetric_in REAL

    proof

      let x,y be object such that

       A1: x in REAL & y in REAL and

       A2: [x, y] in RealOrd & [y, x] in RealOrd ;

      reconsider x, y as Element of REAL by A1;

      x <= y & y <= x by A2, Th4;

      hence thesis by XXREAL_0: 1;

    end;

    

     Lm3: RealOrd is_transitive_in REAL

    proof

      let x,y,z be object such that

       A1: x in REAL & y in REAL & z in REAL and

       A2: [x, y] in RealOrd & [y, z] in RealOrd ;

      reconsider x, y, z as Element of REAL by A1;

      x <= y & y <= z by A2, Th4;

      then x <= z by XXREAL_0: 2;

      hence thesis;

    end;

    

     Lm4: RealOrd is_connected_in REAL

    proof

      let x,y be object;

      assume x in REAL & y in REAL ;

      then

      reconsider x, y as Element of REAL ;

      x <= y or y <= x;

      hence thesis;

    end;

    theorem :: JORDAN1H:5

    

     Th5: ( field RealOrd ) = REAL

    proof

      ( field RealOrd ) c= ( REAL \/ REAL ) by RELSET_1: 8;

      hence ( field RealOrd ) c= REAL ;

      thus thesis by Lm1, PARTIT_2: 8;

    end;

    registration

      cluster RealOrd -> total reflexive antisymmetric transitive being_linear-order;

      coherence

      proof

         REAL c= ( dom RealOrd )

        proof

          let x be object;

          assume x in REAL ;

          then

          reconsider x as Element of REAL ;

           [x, x] in RealOrd ;

          hence thesis by XTUPLE_0:def 12;

        end;

        then ( dom RealOrd ) = REAL ;

        hence RealOrd is total by PARTFUN1:def 2;

        thus RealOrd is reflexive by Lm1, Th5;

        thus RealOrd is antisymmetric by Lm2, Th5;

        thus RealOrd is transitive by Lm3, Th5;

        thus RealOrd is_reflexive_in ( field RealOrd ) by Th5;

        thus RealOrd is_transitive_in ( field RealOrd ) by Lm3, Th5;

        thus RealOrd is_antisymmetric_in ( field RealOrd ) by Lm2, Th5;

        thus RealOrd is_connected_in ( field RealOrd ) by Lm4, Th5;

      end;

    end

    theorem :: JORDAN1H:6

    

     Th6: RealOrd linearly_orders REAL

    proof

      thus RealOrd is_reflexive_in REAL ;

      thus RealOrd is_transitive_in REAL by Lm3;

      thus RealOrd is_antisymmetric_in REAL by Lm2;

      thus thesis by Lm4;

    end;

    theorem :: JORDAN1H:7

    

     Th7: for A be finite Subset of REAL holds ( SgmX ( RealOrd ,A)) is increasing

    proof

      let A be finite Subset of REAL ;

      set IT = ( SgmX ( RealOrd ,A));

      let n,m be Nat such that

       A1: n in ( dom IT) & m in ( dom IT) and

       A2: n < m;

      

       A3: RealOrd linearly_orders A by Th6, ORDERS_1: 38;

      (IT /. n) = (IT . n) & (IT /. m) = (IT . m) by A1, PARTFUN1:def 6;

      then [(IT . n), (IT . m)] in RealOrd by A1, A2, A3, PRE_POLY:def 2;

      then

       A4: (IT . n) <= (IT . m) by Th4;

      IT is one-to-one by Th6, ORDERS_1: 38, PRE_POLY: 10;

      then (IT . n) <> (IT . m) by A1, A2, FUNCT_1:def 4;

      hence thesis by A4, XXREAL_0: 1;

    end;

    theorem :: JORDAN1H:8

    

     Th8: for f be FinSequence of REAL , A be finite Subset of REAL st A = ( rng f) holds ( SgmX ( RealOrd ,A)) = ( Incr f)

    proof

      let f be FinSequence of REAL , A be finite Subset of REAL such that

       A1: A = ( rng f);

      reconsider F = ( SgmX ( RealOrd ,A)) as increasing FinSequence of REAL by Th7;

       RealOrd linearly_orders A by Th6, ORDERS_1: 38;

      then

       A2: ( rng ( SgmX ( RealOrd ,A))) = ( rng f) by A1, PRE_POLY:def 2;

      ( len F) = ( card ( rng f)) by A1, Th6, ORDERS_1: 38, PRE_POLY: 11;

      hence thesis by A2, SEQ_4:def 21;

    end;

    registration

      let A be finite Subset of REAL ;

      cluster ( SgmX ( RealOrd ,A)) -> increasing;

      coherence by Th7;

    end

    theorem :: JORDAN1H:9

    

     Th9: for X be non empty set, A be finite Subset of X, R be being_linear-order Order of X holds ( len ( SgmX (R,A))) = ( card A)

    proof

      let X be non empty set, A be finite Subset of X, R be being_linear-order Order of X;

      ( field R) = X & R linearly_orders ( field R) by ORDERS_1: 15, ORDERS_1: 37;

      hence thesis by ORDERS_1: 38, PRE_POLY: 11;

    end;

    begin

    theorem :: JORDAN1H:10

    

     Th10: for f be FinSequence of ( TOP-REAL 2) holds ( X_axis f) = ( proj1 * f)

    proof

      let f be FinSequence of ( TOP-REAL 2);

      reconsider pf = ( proj1 * f) as FinSequence of REAL by FINSEQ_2: 32;

      

       A1: ( len ( X_axis f)) = ( len f) by GOBOARD1:def 1;

      then

       A2: ( dom ( X_axis f)) = ( dom f) by FINSEQ_3: 29;

      

       A3: for k be Nat st k in ( dom ( X_axis f)) holds (( X_axis f) . k) = (pf . k)

      proof

        let k be Nat such that

         A4: k in ( dom ( X_axis f));

        

         A5: (f /. k) = (f . k) by A2, A4, PARTFUN1:def 6;

        

        thus (( X_axis f) . k) = ((f /. k) `1 ) by A4, GOBOARD1:def 1

        .= ( proj1 . (f . k)) by A5, PSCOMP_1:def 5

        .= (pf . k) by A2, A4, FUNCT_1: 13;

      end;

      ( len pf) = ( len f) by FINSEQ_2: 33;

      then ( dom ( X_axis f)) = ( dom pf) by A1, FINSEQ_3: 29;

      hence thesis by A3, FINSEQ_1: 13;

    end;

    theorem :: JORDAN1H:11

    

     Th11: for f be FinSequence of ( TOP-REAL 2) holds ( Y_axis f) = ( proj2 * f)

    proof

      let f be FinSequence of ( TOP-REAL 2);

      reconsider pf = ( proj2 * f) as FinSequence of REAL by FINSEQ_2: 32;

      

       A1: ( len ( Y_axis f)) = ( len f) by GOBOARD1:def 2;

      then

       A2: ( dom ( Y_axis f)) = ( dom f) by FINSEQ_3: 29;

      

       A3: for k be Nat st k in ( dom ( Y_axis f)) holds (( Y_axis f) . k) = (pf . k)

      proof

        let k be Nat such that

         A4: k in ( dom ( Y_axis f));

        

         A5: (f /. k) = (f . k) by A2, A4, PARTFUN1:def 6;

        

        thus (( Y_axis f) . k) = ((f /. k) `2 ) by A4, GOBOARD1:def 2

        .= ( proj2 . (f . k)) by A5, PSCOMP_1:def 6

        .= (pf . k) by A2, A4, FUNCT_1: 13;

      end;

      ( len pf) = ( len f) by FINSEQ_2: 33;

      then ( dom ( Y_axis f)) = ( dom pf) by A1, FINSEQ_3: 29;

      hence thesis by A3, FINSEQ_1: 13;

    end;

    definition

      let D be non empty set;

      let M be FinSequence of (D * );

      :: original: Values

      redefine

      func Values M -> Subset of D ;

      coherence

      proof

        set A = { ( rng f) where f be Element of (D * ) : f in ( rng M) };

        for X be set st X in A holds X c= D

        proof

          let X be set;

          assume X in A;

          then ex f be Element of (D * ) st X = ( rng f) & f in ( rng M);

          hence thesis;

        end;

        then ( union A) c= D by ZFMISC_1: 76;

        hence thesis by MATRIX_0: 35;

      end;

    end

    registration

      let D be non empty with_non-empty_elements set;

      let M be non empty non-empty FinSequence of (D * );

      cluster ( Values M) -> non empty;

      coherence

      proof

        ( dom ( rngs M)) = ( dom M) by FUNCT_6: 60;

        then

        reconsider X = ( rng ( rngs M)) as non empty with_non-empty_elements set by RELAT_1: 42;

        ( Values M) = ( Union ( rngs M)) by MATRIX_0:def 9

        .= ( union X) by CARD_3:def 4;

        hence thesis;

      end;

    end

    theorem :: JORDAN1H:12

    

     Th12: for D be non empty set, M be Matrix of D, i st i in ( Seg ( width M)) holds ( rng ( Col (M,i))) c= ( Values M)

    proof

      let D be non empty set;

      let M be Matrix of D, k;

      assume k in ( Seg ( width M));

      then

       A1: 1 <= k & k <= ( width M) by FINSEQ_1: 1;

      let e be object;

      assume e in ( rng ( Col (M,k)));

      then

      consider u be object such that

       A2: u in ( dom ( Col (M,k))) and

       A3: e = (( Col (M,k)) . u) by FUNCT_1:def 3;

      reconsider u as Nat by A2;

      

       A4: 1 <= u by A2, FINSEQ_3: 25;

      

       A5: ( len ( Col (M,k))) = ( len M) by MATRIX_0:def 8;

      then u <= ( len M) by A2, FINSEQ_3: 25;

      then

       A6: [u, k] in ( Indices M) by A4, A1, MATRIX_0: 30;

      

       A7: ( Values M) = { (M * (i,j)) where i,j be Nat : [i, j] in ( Indices M) } by MATRIX_0: 39;

      ( dom ( Col (M,k))) = ( dom M) by A5, FINSEQ_3: 29;

      then (( Col (M,k)) . u) = (M * (u,k)) by A2, MATRIX_0:def 8;

      hence thesis by A7, A3, A6;

    end;

    theorem :: JORDAN1H:13

    

     Th13: for D be non empty set, M be Matrix of D, i st i in ( dom M) holds ( rng ( Line (M,i))) c= ( Values M)

    proof

      let D be non empty set;

      let M be Matrix of D, k;

      assume k in ( dom M);

      then

       A1: 1 <= k & k <= ( len M) by FINSEQ_3: 25;

      let e be object;

      assume e in ( rng ( Line (M,k)));

      then

      consider u be object such that

       A2: u in ( dom ( Line (M,k))) and

       A3: e = (( Line (M,k)) . u) by FUNCT_1:def 3;

      reconsider u as Nat by A2;

      

       A4: 1 <= u by A2, FINSEQ_3: 25;

      

       A5: ( len ( Line (M,k))) = ( width M) by MATRIX_0:def 7;

      then u <= ( width M) by A2, FINSEQ_3: 25;

      then

       A6: [k, u] in ( Indices M) by A1, A4, MATRIX_0: 30;

      

       A7: ( Values M) = { (M * (i,j)) where i,j be Nat : [i, j] in ( Indices M) } by MATRIX_0: 39;

      ( dom ( Line (M,k))) = ( Seg ( width M)) by A5, FINSEQ_1:def 3;

      then (( Line (M,k)) . u) = (M * (k,u)) by A2, MATRIX_0:def 7;

      hence thesis by A7, A3, A6;

    end;

    theorem :: JORDAN1H:14

    

     Th14: for G be X_increasing-in-column non empty-yielding Matrix of ( TOP-REAL 2) holds ( len G) <= ( card ( proj1 .: ( Values G)))

    proof

      let G be X_increasing-in-column non empty-yielding Matrix of ( TOP-REAL 2);

       0 <> ( width G) by MATRIX_0:def 10;

      then 1 <= ( width G) by NAT_1: 14;

      then

       A1: 1 in ( Seg ( width G)) by FINSEQ_1: 1;

      then

      reconsider L = ( X_axis ( Col (G,1))) as increasing FinSequence of REAL by GOBOARD1:def 7;

      

       A2: ( card ( rng L)) = ( len L) by FINSEQ_4: 62

      .= ( len ( Col (G,1))) by GOBOARD1:def 1

      .= ( len G) by MATRIX_0:def 8;

      

       A3: ( rng L) = ( rng ( proj1 * ( Col (G,1)))) by Th10

      .= ( proj1 .: ( rng ( Col (G,1)))) by RELAT_1: 127;

      ( rng ( Col (G,1))) c= ( Values G) by A1, Th12;

      hence thesis by A3, A2, NAT_1: 43, RELAT_1: 123;

    end;

    theorem :: JORDAN1H:15

    

     Th15: for G be X_equal-in-line Matrix of ( TOP-REAL 2) holds ( card ( proj1 .: ( Values G))) <= ( len G)

    proof

      let G be X_equal-in-line Matrix of ( TOP-REAL 2);

      deffunc F( Nat) = ( proj1 . (G * ($1,1)));

      consider f be FinSequence such that

       A1: ( len f) = ( len G) and

       A2: for k be Nat st k in ( dom f) holds (f . k) = F(k) from FINSEQ_1:sch 2;

      

       A3: ( dom f) = ( dom G) by A1, FINSEQ_3: 29;

      ( proj1 .: ( Values G)) c= ( rng f)

      proof

        let y be object;

        

         A4: ( Values G) = { (G * (i,j)) where i,j be Nat : [i, j] in ( Indices G) } by MATRIX_0: 39;

        assume y in ( proj1 .: ( Values G));

        then

        consider x be object such that

         A5: x in the carrier of ( TOP-REAL 2) and

         A6: x in ( Values G) and

         A7: y = ( proj1 . x) by FUNCT_2: 64;

        consider i, j such that

         A8: x = (G * (i,j)) and

         A9: [i, j] in ( Indices G) by A6, A4;

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

        

         A10: 1 <= j & j <= ( width G) by A9, MATRIX_0: 32;

        

         A11: 1 <= i & i <= ( len G) by A9, MATRIX_0: 32;

        then

         A12: i in ( dom G) by FINSEQ_3: 25;

        y = (x `1 ) by A7, PSCOMP_1:def 5

        .= ((G * (i,1)) `1 ) by A8, A11, A10, GOBOARD5: 2

        .= ( proj1 . (G * (i,1))) by PSCOMP_1:def 5

        .= (f . i) by A2, A3, A12;

        hence thesis by A3, A12, FUNCT_1: 3;

      end;

      then ( Segm ( card ( proj1 .: ( Values G)))) c= ( Segm ( card ( dom G))) by A3, CARD_1: 12;

      then ( card ( proj1 .: ( Values G))) <= ( card ( dom G)) by NAT_1: 39;

      hence thesis by CARD_1: 62;

    end;

    theorem :: JORDAN1H:16

    

     Th16: for G be X_equal-in-line X_increasing-in-column non empty-yielding Matrix of ( TOP-REAL 2) holds ( len G) = ( card ( proj1 .: ( Values G)))

    proof

      let G be X_equal-in-line X_increasing-in-column non empty-yielding Matrix of ( TOP-REAL 2);

      ( len G) <= ( card ( proj1 .: ( Values G))) & ( card ( proj1 .: ( Values G))) <= ( len G) by Th14, Th15;

      hence thesis by XXREAL_0: 1;

    end;

    theorem :: JORDAN1H:17

    

     Th17: for G be Y_increasing-in-line non empty-yielding Matrix of ( TOP-REAL 2) holds ( width G) <= ( card ( proj2 .: ( Values G)))

    proof

      let G be Y_increasing-in-line non empty-yielding Matrix of ( TOP-REAL 2);

       0 <> ( len G) by MATRIX_0:def 10;

      then 1 <= ( len G) by NAT_1: 14;

      then

       A1: 1 in ( dom G) by FINSEQ_3: 25;

      then

      reconsider L = ( Y_axis ( Line (G,1))) as increasing FinSequence of REAL by GOBOARD1:def 6;

      

       A2: ( card ( rng L)) = ( len L) by FINSEQ_4: 62

      .= ( len ( Line (G,1))) by GOBOARD1:def 2

      .= ( width G) by MATRIX_0:def 7;

      

       A3: ( rng L) = ( rng ( proj2 * ( Line (G,1)))) by Th11

      .= ( proj2 .: ( rng ( Line (G,1)))) by RELAT_1: 127;

      ( rng ( Line (G,1))) c= ( Values G) by A1, Th13;

      hence thesis by A3, A2, NAT_1: 43, RELAT_1: 123;

    end;

    theorem :: JORDAN1H:18

    

     Th18: for G be Y_equal-in-column non empty-yielding Matrix of ( TOP-REAL 2) holds ( card ( proj2 .: ( Values G))) <= ( width G)

    proof

      let G be Y_equal-in-column non empty-yielding Matrix of ( TOP-REAL 2);

      deffunc F( Nat) = ( proj2 . (G * (1,$1)));

      consider f be FinSequence such that

       A1: ( len f) = ( width G) and

       A2: for k be Nat st k in ( dom f) holds (f . k) = F(k) from FINSEQ_1:sch 2;

      

       A3: ( dom f) = ( Seg ( width G)) by A1, FINSEQ_1:def 3;

      ( proj2 .: ( Values G)) c= ( rng f)

      proof

        let y be object;

        

         A4: ( Values G) = { (G * (i,j)) where i,j be Nat : [i, j] in ( Indices G) } by MATRIX_0: 39;

        assume y in ( proj2 .: ( Values G));

        then

        consider x be object such that

         A5: x in the carrier of ( TOP-REAL 2) and

         A6: x in ( Values G) and

         A7: y = ( proj2 . x) by FUNCT_2: 64;

        consider i, j such that

         A8: x = (G * (i,j)) and

         A9: [i, j] in ( Indices G) by A6, A4;

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

        

         A10: 1 <= i & i <= ( len G) by A9, MATRIX_0: 32;

        

         A11: 1 <= j & j <= ( width G) by A9, MATRIX_0: 32;

        then

         A12: j in ( Seg ( width G)) by FINSEQ_1: 1;

        y = (x `2 ) by A7, PSCOMP_1:def 6

        .= ((G * (1,j)) `2 ) by A8, A11, A10, GOBOARD5: 1

        .= ( proj2 . (G * (1,j))) by PSCOMP_1:def 6

        .= (f . j) by A2, A3, A12;

        hence thesis by A3, A12, FUNCT_1: 3;

      end;

      then ( Segm ( card ( proj2 .: ( Values G)))) c= ( Segm ( card ( Seg ( width G)))) by A3, CARD_1: 12;

      then ( card ( proj2 .: ( Values G))) <= ( card ( Seg ( width G))) by NAT_1: 39;

      hence thesis by FINSEQ_1: 57;

    end;

    theorem :: JORDAN1H:19

    

     Th19: for G be Y_equal-in-column Y_increasing-in-line non empty-yielding Matrix of ( TOP-REAL 2) holds ( width G) = ( card ( proj2 .: ( Values G)))

    proof

      let G be Y_equal-in-column Y_increasing-in-line non empty-yielding Matrix of ( TOP-REAL 2);

      ( width G) <= ( card ( proj2 .: ( Values G))) & ( card ( proj2 .: ( Values G))) <= ( width G) by Th17, Th18;

      hence thesis by XXREAL_0: 1;

    end;

    begin

    theorem :: JORDAN1H:20

    for G be Go-board holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on G holds for k be Nat st 1 <= k & (k + 1) <= ( len f) holds ( LSeg (f,k)) c= ( left_cell (f,k,G))

    proof

      let G be Go-board;

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is_sequence_on G;

      let k be Nat;

      assume

       A2: 1 <= k & (k + 1) <= ( len f);

      then

       A3: k in ( dom f) by SEQ_4: 134;

      then

      consider i1,j1 be Nat such that

       A4: [i1, j1] in ( Indices G) and

       A5: (f /. k) = (G * (i1,j1)) by A1, GOBOARD1:def 9;

      

       A6: (k + 1) in ( dom f) by A2, SEQ_4: 134;

      then

      consider i2,j2 be Nat such that

       A7: [i2, j2] in ( Indices G) and

       A8: (f /. (k + 1)) = (G * (i2,j2)) by A1, GOBOARD1:def 9;

      

       A9: 1 <= i2 by A7, MATRIX_0: 32;

      

       A10: 1 <= j1 by A4, MATRIX_0: 32;

      ( left_cell (f,k,G)) = ( left_cell (f,k,G));

      then

       A11: i1 = i2 & (j1 + 1) = j2 & ( left_cell (f,k,G)) = ( cell (G,(i1 -' 1),j1)) or (i1 + 1) = i2 & j1 = j2 & ( left_cell (f,k,G)) = ( cell (G,i1,j1)) or i1 = (i2 + 1) & j1 = j2 & ( left_cell (f,k,G)) = ( cell (G,i2,(j2 -' 1))) or i1 = i2 & j1 = (j2 + 1) & ( left_cell (f,k,G)) = ( cell (G,i1,j2)) by A1, A2, A4, A5, A7, A8, GOBRD13:def 3;

      

       A12: 1 <= j2 by A7, MATRIX_0: 32;

      

       A13: j1 <= ( width G) by A4, MATRIX_0: 32;

      

       A14: j2 <= ( width G) by A7, MATRIX_0: 32;

      

       A15: i2 <= ( len G) by A7, MATRIX_0: 32;

      

       A16: 1 <= i1 by A4, MATRIX_0: 32;

      ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A1, A3, A6, A4, A5, A7, A8, GOBOARD1:def 9;

      then

       A17: |.(i1 - i2).| = 1 & j1 = j2 or |.(j1 - j2).| = 1 & i1 = i2 by SEQM_3: 42;

      

       A18: i1 <= ( len G) by A4, MATRIX_0: 32;

      per cases by A17, SEQM_3: 41;

        suppose

         A19: i1 = i2 & (j1 + 1) = j2;

        then

         A20: j1 < ( width G) by A14, NAT_1: 13;

        

         A21: ((i1 -' 1) + 1) = i1 by A16, XREAL_1: 235;

        then (i1 -' 1) < ( len G) by A18, NAT_1: 13;

        then ( LSeg ((f /. k),(f /. (k + 1)))) c= ( cell (G,(i1 -' 1),j1)) by A5, A8, A10, A19, A21, A20, GOBOARD5: 18;

        hence thesis by A2, A11, A19, TOPREAL1:def 3;

      end;

        suppose

         A22: (i1 + 1) = i2 & j1 = j2;

        then i1 < ( len G) by A15, NAT_1: 13;

        then ( LSeg ((f /. k),(f /. (k + 1)))) c= ( cell (G,i1,j1)) by A5, A8, A16, A10, A13, A22, GOBOARD5: 22;

        hence thesis by A2, A11, A22, TOPREAL1:def 3;

      end;

        suppose

         A23: i1 = (i2 + 1) & j1 = j2;

        then

         A24: i2 < ( len G) by A18, NAT_1: 13;

        

         A25: ((j2 -' 1) + 1) = j2 by A12, XREAL_1: 235;

        then (j2 -' 1) < ( width G) by A14, NAT_1: 13;

        then ( LSeg ((f /. k),(f /. (k + 1)))) c= ( cell (G,i2,(j2 -' 1))) by A5, A8, A9, A23, A25, A24, GOBOARD5: 21;

        hence thesis by A2, A11, A23, TOPREAL1:def 3;

      end;

        suppose

         A26: i1 = i2 & j1 = (j2 + 1);

        then j2 < ( width G) by A13, NAT_1: 13;

        then ( LSeg ((f /. k),(f /. (k + 1)))) c= ( left_cell (f,k,G)) by A5, A8, A16, A18, A12, A11, A26, GOBOARD5: 19;

        hence thesis by A2, TOPREAL1:def 3;

      end;

    end;

    theorem :: JORDAN1H:21

    for f be standard special_circular_sequence st 1 <= k & (k + 1) <= ( len f) holds ( left_cell (f,k,( GoB f))) = ( left_cell (f,k))

    proof

      let f be standard special_circular_sequence such that

       A1: 1 <= k and

       A2: (k + 1) <= ( len f);

      set G = ( GoB f);

      

       A3: f is_sequence_on ( GoB f) by GOBOARD5:def 5;

      for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices G) & [i2, j2] in ( Indices G) & (f /. k) = (G * (i1,j1)) & (f /. (k + 1)) = (G * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & ( left_cell (f,k)) = ( cell (( GoB f),(i1 -' 1),j1)) or (i1 + 1) = i2 & j1 = j2 & ( left_cell (f,k)) = ( cell (( GoB f),i1,j1)) or i1 = (i2 + 1) & j1 = j2 & ( left_cell (f,k)) = ( cell (( GoB f),i2,(j2 -' 1))) or i1 = i2 & j1 = (j2 + 1) & ( left_cell (f,k)) = ( cell (( GoB f),i1,j2))

      proof

        1 <= (k + 1) by NAT_1: 11;

        then

         A4: (k + 1) in ( dom f) by A2, FINSEQ_3: 25;

        let i1,j1,i2,j2 be Nat such that

         A5: [i1, j1] in ( Indices G) & [i2, j2] in ( Indices G) & (f /. k) = (G * (i1,j1)) & (f /. (k + 1)) = (G * (i2,j2));

        k < ( len f) by A2, NAT_1: 13;

        then k in ( dom f) by A1, FINSEQ_3: 25;

        then ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A3, A5, A4, GOBOARD1:def 9;

        then

         A6: |.(i1 - i2).| = 1 & j1 = j2 or |.(j1 - j2).| = 1 & i1 = i2 by SEQM_3: 42;

        ( left_cell (f,k)) = ( left_cell (f,k));

        then

         A7: i1 = i2 & (j1 + 1) = j2 & ( left_cell (f,k)) = ( cell (( GoB f),(i1 -' 1),j1)) or (i1 + 1) = i2 & j1 = j2 & ( left_cell (f,k)) = ( cell (( GoB f),i1,j1)) or i1 = (i2 + 1) & j1 = j2 & ( left_cell (f,k)) = ( cell (( GoB f),i2,(j2 -' 1))) or i1 = i2 & j1 = (j2 + 1) & ( left_cell (f,k)) = ( cell (( GoB f),i1,j2)) by A1, A2, A5, GOBOARD5:def 7;

        per cases by A6, SEQM_3: 41;

          case i1 = i2 & (j1 + 1) = j2;

          hence thesis by A7;

        end;

          case (i1 + 1) = i2 & j1 = j2;

          hence thesis by A7;

        end;

          case i1 = (i2 + 1) & j1 = j2;

          hence thesis by A7;

        end;

          case i1 = i2 & j1 = (j2 + 1);

          hence thesis by A7;

        end;

      end;

      hence thesis by A1, A2, A3, GOBRD13:def 3;

    end;

    theorem :: JORDAN1H:22

    

     Th22: for G be Go-board holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on G holds for k be Nat st 1 <= k & (k + 1) <= ( len f) holds ( LSeg (f,k)) c= ( right_cell (f,k,G))

    proof

      let G be Go-board;

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is_sequence_on G;

      let k be Nat;

      assume

       A2: 1 <= k & (k + 1) <= ( len f);

      then

       A3: k in ( dom f) by SEQ_4: 134;

      then

      consider i1,j1 be Nat such that

       A4: [i1, j1] in ( Indices G) and

       A5: (f /. k) = (G * (i1,j1)) by A1, GOBOARD1:def 9;

      

       A6: (k + 1) in ( dom f) by A2, SEQ_4: 134;

      then

      consider i2,j2 be Nat such that

       A7: [i2, j2] in ( Indices G) and

       A8: (f /. (k + 1)) = (G * (i2,j2)) by A1, GOBOARD1:def 9;

      

       A9: 1 <= i2 by A7, MATRIX_0: 32;

      

       A10: 1 <= j1 by A4, MATRIX_0: 32;

      ( right_cell (f,k,G)) = ( right_cell (f,k,G));

      then

       A11: i1 = i2 & (j1 + 1) = j2 & ( right_cell (f,k,G)) = ( cell (G,i1,j1)) or (i1 + 1) = i2 & j1 = j2 & ( right_cell (f,k,G)) = ( cell (G,i1,(j1 -' 1))) or i1 = (i2 + 1) & j1 = j2 & ( right_cell (f,k,G)) = ( cell (G,i2,j2)) or i1 = i2 & j1 = (j2 + 1) & ( right_cell (f,k,G)) = ( cell (G,(i1 -' 1),j2)) by A1, A2, A4, A5, A7, A8, GOBRD13:def 2;

      

       A12: 1 <= j2 by A7, MATRIX_0: 32;

      

       A13: j1 <= ( width G) by A4, MATRIX_0: 32;

      

       A14: j2 <= ( width G) by A7, MATRIX_0: 32;

      

       A15: i2 <= ( len G) by A7, MATRIX_0: 32;

      

       A16: 1 <= i1 by A4, MATRIX_0: 32;

      ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A1, A3, A6, A4, A5, A7, A8, GOBOARD1:def 9;

      then

       A17: |.(i1 - i2).| = 1 & j1 = j2 or |.(j1 - j2).| = 1 & i1 = i2 by SEQM_3: 42;

      

       A18: i1 <= ( len G) by A4, MATRIX_0: 32;

      per cases by A17, SEQM_3: 41;

        suppose

         A19: i1 = i2 & (j1 + 1) = j2;

        then j1 < ( width G) by A14, NAT_1: 13;

        then ( LSeg ((f /. k),(f /. (k + 1)))) c= ( cell (G,i1,j1)) by A5, A8, A16, A18, A10, A19, GOBOARD5: 19;

        hence thesis by A2, A11, A19, TOPREAL1:def 3;

      end;

        suppose

         A20: (i1 + 1) = i2 & j1 = j2;

        then

         A21: i1 < ( len G) by A15, NAT_1: 13;

        

         A22: ((j1 -' 1) + 1) = j1 by A10, XREAL_1: 235;

        then (j1 -' 1) < ( width G) by A13, NAT_1: 13;

        then ( LSeg ((f /. k),(f /. (k + 1)))) c= ( cell (G,i1,(j1 -' 1))) by A5, A8, A16, A20, A22, A21, GOBOARD5: 21;

        hence thesis by A2, A11, A20, TOPREAL1:def 3;

      end;

        suppose

         A23: i1 = (i2 + 1) & j1 = j2;

        then i2 < ( len G) by A18, NAT_1: 13;

        then ( LSeg ((f /. k),(f /. (k + 1)))) c= ( cell (G,i2,j2)) by A5, A8, A9, A12, A14, A23, GOBOARD5: 22;

        hence thesis by A2, A11, A23, TOPREAL1:def 3;

      end;

        suppose

         A24: i1 = i2 & j1 = (j2 + 1);

        then

         A25: j2 < ( width G) by A13, NAT_1: 13;

        

         A26: ((i1 -' 1) + 1) = i1 by A16, XREAL_1: 235;

        then (i1 -' 1) < ( len G) by A18, NAT_1: 13;

        then ( LSeg ((f /. k),(f /. (k + 1)))) c= ( right_cell (f,k,G)) by A5, A8, A12, A11, A24, A26, A25, GOBOARD5: 18;

        hence thesis by A2, TOPREAL1:def 3;

      end;

    end;

    theorem :: JORDAN1H:23

    

     Th23: for f be standard special_circular_sequence st 1 <= k & (k + 1) <= ( len f) holds ( right_cell (f,k,( GoB f))) = ( right_cell (f,k))

    proof

      let f be standard special_circular_sequence such that

       A1: 1 <= k and

       A2: (k + 1) <= ( len f);

      set G = ( GoB f);

      

       A3: f is_sequence_on ( GoB f) by GOBOARD5:def 5;

      for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices G) & [i2, j2] in ( Indices G) & (f /. k) = (G * (i1,j1)) & (f /. (k + 1)) = (G * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & ( right_cell (f,k)) = ( cell (G,i1,j1)) or (i1 + 1) = i2 & j1 = j2 & ( right_cell (f,k)) = ( cell (G,i1,(j1 -' 1))) or i1 = (i2 + 1) & j1 = j2 & ( right_cell (f,k)) = ( cell (G,i2,j2)) or i1 = i2 & j1 = (j2 + 1) & ( right_cell (f,k)) = ( cell (G,(i1 -' 1),j2))

      proof

        1 <= (k + 1) by NAT_1: 11;

        then

         A4: (k + 1) in ( dom f) by A2, FINSEQ_3: 25;

        set IT = ( right_cell (f,k));

        let i1,j1,i2,j2 be Nat such that

         A5: [i1, j1] in ( Indices G) & [i2, j2] in ( Indices G) & (f /. k) = (G * (i1,j1)) & (f /. (k + 1)) = (G * (i2,j2));

        k < ( len f) by A2, NAT_1: 13;

        then k in ( dom f) by A1, FINSEQ_3: 25;

        then ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A3, A5, A4, GOBOARD1:def 9;

        then

         A6: |.(i1 - i2).| = 1 & j1 = j2 or |.(j1 - j2).| = 1 & i1 = i2 by SEQM_3: 42;

        ( right_cell (f,k)) = ( right_cell (f,k));

        then

         A7: i1 = i2 & (j1 + 1) = j2 & IT = ( cell (( GoB f),i1,j1)) or (i1 + 1) = i2 & j1 = j2 & IT = ( cell (( GoB f),i1,(j1 -' 1))) or i1 = (i2 + 1) & j1 = j2 & IT = ( cell (( GoB f),i2,j2)) or i1 = i2 & j1 = (j2 + 1) & IT = ( cell (( GoB f),(i1 -' 1),j2)) by A1, A2, A5, GOBOARD5:def 6;

        per cases by A6, SEQM_3: 41;

          case i1 = i2 & (j1 + 1) = j2;

          hence thesis by A7;

        end;

          case (i1 + 1) = i2 & j1 = j2;

          hence thesis by A7;

        end;

          case i1 = (i2 + 1) & j1 = j2;

          hence thesis by A7;

        end;

          case i1 = i2 & j1 = (j2 + 1);

          hence thesis by A7;

        end;

      end;

      hence thesis by A1, A2, A3, GOBRD13:def 2;

    end;

    theorem :: JORDAN1H:24

    for P be Subset of ( TOP-REAL 2), f be non constant standard special_circular_sequence st P is_a_component_of (( L~ f) ` ) holds P = ( RightComp f) or P = ( LeftComp f)

    proof

      let P be Subset of ( TOP-REAL 2), f be non constant standard special_circular_sequence;

      assume P is_a_component_of (( L~ f) ` );

      then ex B1 be Subset of (( TOP-REAL 2) | (( L~ f) ` )) st B1 = P & B1 is a_component by CONNSP_1:def 6;

      hence thesis by GOBRD14: 12;

    end;

    theorem :: JORDAN1H:25

    for f be non constant standard special_circular_sequence st f is_sequence_on G holds for k st 1 <= k & (k + 1) <= ( len f) holds ( Int ( right_cell (f,k,G))) c= ( RightComp f) & ( Int ( left_cell (f,k,G))) c= ( LeftComp f)

    proof

      let f be non constant standard special_circular_sequence such that

       A1: f is_sequence_on G;

      let k such that

       A2: 1 <= k & (k + 1) <= ( len f);

      ( Int ( right_cell (f,k,G))) misses ( L~ f) by A1, A2, JORDAN9: 15;

      then

       A3: ( Int ( right_cell (f,k,G))) c= (( right_cell (f,k,G)) \ ( L~ f)) by TOPS_1: 16, XBOOLE_1: 86;

      ( Int ( left_cell (f,k,G))) misses ( L~ f) by A1, A2, JORDAN9: 15;

      then

       A4: ( Int ( left_cell (f,k,G))) c= (( left_cell (f,k,G)) \ ( L~ f)) by TOPS_1: 16, XBOOLE_1: 86;

      (( right_cell (f,k,G)) \ ( L~ f)) c= ( RightComp f) by A1, A2, JORDAN9: 27;

      hence ( Int ( right_cell (f,k,G))) c= ( RightComp f) by A3;

      (( left_cell (f,k,G)) \ ( L~ f)) c= ( LeftComp f) by A1, A2, JORDAN9: 27;

      hence thesis by A4;

    end;

    theorem :: JORDAN1H:26

    

     Th26: for i1,j1,i2,j2 be Nat, G be Go-board st [i1, j1] in ( Indices G) & [i2, j2] in ( Indices G) & (G * (i1,j1)) = (G * (i2,j2)) holds i1 = i2 & j1 = j2

    proof

      let i1,j1,i2,j2 be Nat, G be Go-board such that

       A1: [i1, j1] in ( Indices G) and

       A2: [i2, j2] in ( Indices G) and

       A3: (G * (i1,j1)) = (G * (i2,j2));

      

       A4: 1 <= i1 by A1, MATRIX_0: 32;

      

       A5: j1 <= ( width G) by A1, MATRIX_0: 32;

      

       A6: 1 <= j1 by A1, MATRIX_0: 32;

      

       A7: 1 <= i2 by A2, MATRIX_0: 32;

      

       A8: i1 <= ( len G) by A1, MATRIX_0: 32;

      

       A9: i2 <= ( len G) by A2, MATRIX_0: 32;

      

       A10: j2 <= ( width G) by A2, MATRIX_0: 32;

      

       A11: 1 <= j2 by A2, MATRIX_0: 32;

      

      then

       A12: ((G * (i1,j2)) `2 ) = ((G * (1,j2)) `2 ) by A4, A8, A10, GOBOARD5: 1

      .= ((G * (i1,j1)) `2 ) by A3, A7, A9, A11, A10, GOBOARD5: 1;

      

       A13: ((G * (i1,j2)) `1 ) = ((G * (i1,1)) `1 ) by A4, A8, A11, A10, GOBOARD5: 2

      .= ((G * (i1,j1)) `1 ) by A4, A8, A6, A5, GOBOARD5: 2;

      assume

       A14: not thesis;

      per cases by A14, XXREAL_0: 1;

        suppose i1 < i2;

        hence contradiction by A3, A4, A9, A11, A10, A13, GOBOARD5: 3;

      end;

        suppose i1 > i2;

        hence contradiction by A3, A8, A7, A11, A10, A13, GOBOARD5: 3;

      end;

        suppose j1 < j2;

        hence contradiction by A4, A8, A6, A10, A12, GOBOARD5: 4;

      end;

        suppose j1 > j2;

        hence contradiction by A4, A8, A5, A11, A12, GOBOARD5: 4;

      end;

    end;

    theorem :: JORDAN1H:27

    

     Th27: for f be FinSequence of ( TOP-REAL 2), M be Go-board holds f is_sequence_on M implies ( mid (f,i1,i2)) is_sequence_on M

    proof

      let f be FinSequence of ( TOP-REAL 2), M be Go-board;

      assume

       A1: f is_sequence_on M;

      per cases ;

        suppose

         A2: i1 <= i2;

        

         A3: (f /^ (i1 -' 1)) is_sequence_on M by A1, JORDAN8: 2;

        ( mid (f,i1,i2)) = ((f /^ (i1 -' 1)) | ((i2 -' i1) + 1)) by A2, FINSEQ_6:def 3;

        hence thesis by A3, GOBOARD1: 22;

      end;

        suppose

         A4: i1 > i2;

        (f /^ (i2 -' 1)) is_sequence_on M by A1, JORDAN8: 2;

        then

         A5: ((f /^ (i2 -' 1)) | ((i1 -' i2) + 1)) is_sequence_on M by GOBOARD1: 22;

        ( mid (f,i1,i2)) = ( Rev ((f /^ (i2 -' 1)) | ((i1 -' i2) + 1))) by A4, FINSEQ_6:def 3;

        hence thesis by A5, JORDAN9: 5;

      end;

    end;

    registration

      cluster -> non empty non-empty for Go-board;

      coherence

      proof

        let G be Go-board;

        thus G is non empty;

        consider n0 be Nat such that

         A1: for x be object st x in ( rng G) holds ex s be FinSequence st s = x & ( len s) = n0 by MATRIX_0:def 1;

        ( len G) <> 0 by MATRIX_0:def 10;

        then

        consider s0 be FinSequence such that

         A2: s0 in ( rng G) and

         A3: ( len s0) = ( width G) by MATRIX_0:def 3;

        

         A4: ex s be FinSequence st s = s0 & ( len s) = n0 by A2, A1;

        assume not G is non-empty;

        then

        consider n be object such that

         A5: n in ( dom G) and

         A6: (G . n) is empty by FUNCT_1:def 9;

        

         A7: ( card (G . n)) is empty by A6;

        ex s1 be FinSequence st s1 = (G . n) & ( len s1) = n0 by A5, A1, FUNCT_1: 3;

        hence contradiction by A3, A4, A7, MATRIX_0:def 10;

      end;

    end

    theorem :: JORDAN1H:28

    

     Th28: for G be Go-board st 1 <= i & i <= ( len G) holds (( SgmX ( RealOrd ,( proj1 .: ( Values G)))) . i) = ((G * (i,1)) `1 )

    proof

      let G be Go-board;

      assume 1 <= i & i <= ( len G);

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

      then

       A1: i in ( Seg ( len G)) by FINSEQ_1:def 3;

       0 <> ( width G) by MATRIX_0:def 10;

      then

       A2: 1 <= ( width G) by NAT_1: 14;

      reconsider A = ( proj1 .: ( Values G)) as finite Subset of REAL ;

      deffunc F( Nat) = ( In (((G * ($1,1)) `1 ), REAL ));

      consider f be FinSequence of REAL such that

       A3: ( len f) = ( len G) and

       A4: for i be Nat st i in ( dom f) holds (f . i) = F(i) from FINSEQ_2:sch 1;

      

       A5: ( dom f) = ( Seg ( len G)) by A3, FINSEQ_1:def 3;

      

       A6: ( rng f) = A

      proof

        

         A7: ( Values G) = { (G * (m,n)) : [m, n] in ( Indices G) } by MATRIX_0: 39;

        thus ( rng f) c= A

        proof

          let x be object;

          assume

           A8: x in ( rng f);

          then

          reconsider x as Element of REAL ;

          consider y be object such that

           A9: y in ( dom f) and

           A10: x = (f . y) by A8, FUNCT_1:def 3;

          reconsider y as Nat by A9;

          1 <= y & y <= ( len G) by A3, A9, FINSEQ_3: 25;

          then [y, 1] in ( Indices G) by A2, MATRIX_0: 30;

          then

           A11: (G * (y,1)) in ( Values G) by A7;

          x = F(y) by A4, A9, A10

          .= ( proj1 . (G * (y,1))) by PSCOMP_1:def 5;

          hence thesis by A11, FUNCT_2: 35;

        end;

        let x be object;

        assume

         A12: x in A;

        then

        reconsider x as Element of REAL ;

        consider p be Element of ( TOP-REAL 2) such that

         A13: p in ( Values G) and

         A14: x = ( proj1 . p) by A12, FUNCT_2: 65;

        consider m, n such that

         A15: p = (G * (m,n)) and

         A16: [m, n] in ( Indices G) by A7, A13;

        

         A17: 1 <= n & n <= ( width G) by A16, MATRIX_0: 32;

        

         A18: 1 <= m & m <= ( len G) by A16, MATRIX_0: 32;

        then

         A19: m in ( Seg ( len G)) by FINSEQ_1: 1;

        

         A20: m in ( dom f) by A3, A18, FINSEQ_3: 25;

        x = (p `1 ) by A14, PSCOMP_1:def 5

        .= F(m) by A15, A17, A18, GOBOARD5: 2

        .= (f . m) by A4, A5, A19;

        hence thesis by A20, FUNCT_1:def 3;

      end;

      for n,m be Nat st n in ( dom f) & m in ( dom f) & n < m holds (f /. n) <> (f /. m) & [(f /. n), (f /. m)] in RealOrd

      proof

        let n,m be Nat such that

         A21: n in ( dom f) & m in ( dom f) and

         A22: n < m;

        

         A23: 1 <= n & m <= ( len G) by A3, A21, FINSEQ_3: 25;

        reconsider n9 = n, m9 = m as Nat;

        

         A24: (f /. n) = (f . n) & (f /. m) = (f . m) by A21, PARTFUN1:def 6;

        

         A25: (f . n) = F(n9) & (f . m) = F(m9) by A4, A21;

        hence (f /. n) <> (f /. m) by A2, A22, A23, A24, GOBOARD5: 3;

        (f . n9) < (f . m9) by A2, A22, A25, A23, GOBOARD5: 3;

        hence thesis by A24;

      end;

      then f = ( SgmX ( RealOrd ,( proj1 .: ( Values G)))) by A6, PRE_POLY: 9;

      then (( SgmX ( RealOrd ,( proj1 .: ( Values G)))) . i) = F(i) by A4, A5, A1;

      hence thesis;

    end;

    theorem :: JORDAN1H:29

    

     Th29: for G be Go-board st 1 <= j & j <= ( width G) holds (( SgmX ( RealOrd ,( proj2 .: ( Values G)))) . j) = ((G * (1,j)) `2 )

    proof

      let G be Go-board;

      assume 1 <= j & j <= ( width G);

      then

       A1: j in ( Seg ( width G)) by FINSEQ_1: 1;

      

       A2: 1 <= ( len G) by NAT_1: 14;

      reconsider A = ( proj2 .: ( Values G)) as finite Subset of REAL ;

      deffunc F( Nat) = ( In (((G * (1,$1)) `2 ), REAL ));

      consider f be FinSequence of REAL such that

       A3: ( len f) = ( width G) and

       A4: for i be Nat st i in ( dom f) holds (f . i) = F(i) from FINSEQ_2:sch 1;

      

       A5: ( dom f) = ( Seg ( width G)) by A3, FINSEQ_1:def 3;

      

       A6: ( rng f) = A

      proof

        

         A7: ( Values G) = { (G * (m,n)) : [m, n] in ( Indices G) } by MATRIX_0: 39;

        thus ( rng f) c= A

        proof

          let x be object;

          assume

           A8: x in ( rng f);

          then

          reconsider x as Element of REAL ;

          consider y be object such that

           A9: y in ( dom f) and

           A10: x = (f . y) by A8, FUNCT_1:def 3;

          reconsider y as Nat by A9;

          1 <= y & y <= ( width G) by A3, A9, FINSEQ_3: 25;

          then [1, y] in ( Indices G) by A2, MATRIX_0: 30;

          then

           A11: (G * (1,y)) in ( Values G) by A7;

          x = F(y) by A4, A9, A10

          .= ( proj2 . (G * (1,y))) by PSCOMP_1:def 6;

          hence thesis by A11, FUNCT_2: 35;

        end;

        let x be object;

        assume

         A12: x in A;

        then

        reconsider x as Element of REAL ;

        consider p be Element of ( TOP-REAL 2) such that

         A13: p in ( Values G) and

         A14: x = ( proj2 . p) by A12, FUNCT_2: 65;

        consider m, n such that

         A15: p = (G * (m,n)) and

         A16: [m, n] in ( Indices G) by A7, A13;

        

         A17: 1 <= m & m <= ( len G) by A16, MATRIX_0: 32;

        

         A18: 1 <= n & n <= ( width G) by A16, MATRIX_0: 32;

        then

         A19: n in ( Seg ( width G)) by FINSEQ_1: 1;

        

         A20: n in ( dom f) by A3, A18, FINSEQ_3: 25;

        x = (p `2 ) by A14, PSCOMP_1:def 6

        .= F(n) by A15, A17, A18, GOBOARD5: 1

        .= (f . n) by A4, A5, A19;

        hence thesis by A20, FUNCT_1:def 3;

      end;

      for n,m be Nat st n in ( dom f) & m in ( dom f) & n < m holds (f /. n) <> (f /. m) & [(f /. n), (f /. m)] in RealOrd

      proof

        let n,m be Nat such that

         A21: n in ( dom f) & m in ( dom f) and

         A22: n < m;

        

         A23: 1 <= n & m <= ( width G) by A3, A21, FINSEQ_3: 25;

        reconsider n9 = n, m9 = m as Nat;

        

         A24: (f /. n) = (f . n) & (f /. m) = (f . m) by A21, PARTFUN1:def 6;

        

         A25: (f . n) = F(n9) & (f . m) = F(m9) by A4, A21;

        hence (f /. n) <> (f /. m) by A2, A22, A23, A24, GOBOARD5: 4;

        (f . n9) < (f . m9) by A2, A22, A25, A23, GOBOARD5: 4;

        hence thesis by A24;

      end;

      then f = ( SgmX ( RealOrd ,( proj2 .: ( Values G)))) by A6, PRE_POLY: 9;

      then (( SgmX ( RealOrd ,( proj2 .: ( Values G)))) . j) = F(j) by A4, A5, A1;

      hence thesis;

    end;

    theorem :: JORDAN1H:30

    

     Th30: for f be non empty FinSequence of ( TOP-REAL 2), G be Go-board st f is_sequence_on G & (ex i st [1, i] in ( Indices G) & (G * (1,i)) in ( rng f)) & (ex i st [( len G), i] in ( Indices G) & (G * (( len G),i)) in ( rng f)) holds ( proj1 .: ( rng f)) = ( proj1 .: ( Values G))

    proof

      let f be non empty FinSequence of ( TOP-REAL 2), G be Go-board such that

       A1: f is_sequence_on G;

      given i1 be Nat such that

       A2: [1, i1] in ( Indices G) and

       A3: (G * (1,i1)) in ( rng f);

      consider k1 be object such that

       A4: k1 in ( dom f) and

       A5: (G * (1,i1)) = (f . k1) by A3, FUNCT_1:def 3;

      reconsider k1 as Nat by A4;

      

       A6: 1 <= k1 by A4, FINSEQ_3: 25;

      given i2 be Nat such that

       A7: [( len G), i2] in ( Indices G) and

       A8: (G * (( len G),i2)) in ( rng f);

      consider k2 be object such that

       A9: k2 in ( dom f) and

       A10: (G * (( len G),i2)) = (f . k2) by A8, FUNCT_1:def 3;

      reconsider k2 as Nat by A9;

      

       A11: k2 <= ( len f) by A9, FINSEQ_3: 25;

      

       A12: k1 <= ( len f) by A4, FINSEQ_3: 25;

      set g = ( mid (f,k1,k2));

      

       A13: g is_sequence_on G by A1, Th27;

      

       A14: 1 <= k2 by A9, FINSEQ_3: 25;

       A15:

      now

        per cases ;

          suppose k1 <= k2;

          then ( len g) = ((k2 -' k1) + 1) by A6, A11, JORDAN4: 8;

          hence ( len g) >= ( 0 qua Nat + 1) by XREAL_1: 6;

        end;

          suppose k1 > k2;

          then ( len g) = ((k1 -' k2) + 1) by A12, A14, JORDAN4: 9;

          hence ( len g) >= ( 0 qua Nat + 1) by XREAL_1: 6;

        end;

      end;

      

       A16: ( Values G) = { (G * (i,j)) where i,j be Nat : [i, j] in ( Indices G) } by MATRIX_0: 39;

      

       A17: ( proj1 .: ( Values G)) c= ( proj1 .: ( rng g))

      proof

        assume not thesis;

        then

        consider x be Element of REAL such that

         A18: x in ( proj1 .: ( Values G)) and

         A19: not x in ( proj1 .: ( rng g));

        consider p be Element of ( TOP-REAL 2) such that

         A20: p in ( Values G) and

         A21: x = ( proj1 . p) by A18, FUNCT_2: 65;

        consider i0,j0 be Nat such that

         A22: p = (G * (i0,j0)) and

         A23: [i0, j0] in ( Indices G) by A16, A20;

        

         A24: i0 <= ( len G) by A23, MATRIX_0: 32;

        defpred P[ Nat] means 1 <= $1 & $1 <= ( len g) implies for i, j st [i, j] in ( Indices G) & (G * (i,j)) = (g . $1) holds i < i0;

        

         A25: 1 <= i0 by A23, MATRIX_0: 32;

        

         A26: 1 <= j0 & j0 <= ( width G) by A23, MATRIX_0: 32;

        

         A27: for n st P[n] holds P[(n + 1)]

        proof

          let n such that

           A28: 1 <= n & n <= ( len g) implies for i, j st [i, j] in ( Indices G) & (G * (i,j)) = (g . n) holds i < i0 and

           A29: 1 <= (n + 1) and

           A30: (n + 1) <= ( len g);

          let i, j such that

           A31: [i, j] in ( Indices G) and

           A32: (G * (i,j)) = (g . (n + 1));

           A33:

          now

            

             A34: (n + 1) in ( dom g) by A29, A30, FINSEQ_3: 25;

            then

             A35: (G * (i,j)) = (g /. (n + 1)) by A32, PARTFUN1:def 6;

            then

             A36: ( dom proj1 ) = the carrier of ( TOP-REAL 2) & (g /. (n + 1)) in ( rng g) by A32, A34, FUNCT_1: 3, FUNCT_2:def 1;

            

             A37: 1 <= j & j <= ( width G) by A31, MATRIX_0: 32;

            assume

             A38: i = i0;

            x = (p `1 ) by A21, PSCOMP_1:def 5

            .= ((G * (i0,1)) `1 ) by A22, A25, A24, A26, GOBOARD5: 2

            .= ((G * (i,j)) `1 ) by A25, A24, A38, A37, GOBOARD5: 2

            .= ( proj1 . (g /. (n + 1))) by A35, PSCOMP_1:def 5;

            hence contradiction by A19, A36, FUNCT_1:def 6;

          end;

          per cases ;

            suppose n = 0 ;

            then (G * (i,j)) = (G * (1,i1)) by A5, A6, A12, A14, A11, A32, FINSEQ_6: 118;

            then i = 1 by A2, A31, Th26;

            hence thesis by A25, A33, XXREAL_0: 1;

          end;

            suppose

             A39: n <> 0 ;

            then

             A40: 1 <= n by NAT_1: 14;

            

             A41: n <= (n + 1) by NAT_1: 11;

            then n <= ( len g) by A30, XXREAL_0: 2;

            then

             A42: n in ( dom g) by A40, FINSEQ_3: 25;

            then

            consider i1,j1 be Nat such that

             A43: [i1, j1] in ( Indices G) & (g /. n) = (G * (i1,j1)) by A13, GOBOARD1:def 9;

            

             A44: (n + 1) in ( dom g) by A29, A30, FINSEQ_3: 25;

            then (g /. (n + 1)) = (G * (i,j)) by A32, PARTFUN1:def 6;

            then ( |.(i1 - i).| + |.(j1 - j).|) = 1 by A13, A31, A42, A43, A44, GOBOARD1:def 9;

            then

             A45: |.(i1 - i).| = 1 & j1 = j or |.(j1 - j).| = 1 & i1 = i by SEQM_3: 42;

            now

              (g . n) = (g /. n) by A42, PARTFUN1:def 6;

              then

               A46: i1 < i0 by A28, A30, A39, A41, A43, NAT_1: 14, XXREAL_0: 2;

              per cases by A45, SEQM_3: 41;

                suppose i1 = i or i < i1;

                hence thesis by A46, XXREAL_0: 2;

              end;

                suppose i = (i1 + 1);

                then i <= i0 by A46, NAT_1: 13;

                hence thesis by A33, XXREAL_0: 1;

              end;

            end;

            hence thesis;

          end;

        end;

        

         A47: (G * (( len G),i2)) = (g . ( len g)) by A6, A12, A10, A14, A11, JORDAN4: 11;

        

         A48: P[ 0 ];

        for n holds P[n] from NAT_1:sch 2( A48, A27);

        then ( len G) < i0 by A7, A15, A47;

        hence contradiction by A23, MATRIX_0: 32;

      end;

      thus ( proj1 .: ( rng f)) c= ( proj1 .: ( Values G)) by A1, GOBRD13: 8, RELAT_1: 123;

      ( proj1 .: ( rng g)) c= ( proj1 .: ( rng f)) by FINSEQ_6: 119, RELAT_1: 123;

      hence thesis by A17;

    end;

    theorem :: JORDAN1H:31

    

     Th31: for f be non empty FinSequence of ( TOP-REAL 2), G be Go-board st f is_sequence_on G & (ex i st [i, 1] in ( Indices G) & (G * (i,1)) in ( rng f)) & (ex i st [i, ( width G)] in ( Indices G) & (G * (i,( width G))) in ( rng f)) holds ( proj2 .: ( rng f)) = ( proj2 .: ( Values G))

    proof

      let f be non empty FinSequence of ( TOP-REAL 2), G be Go-board such that

       A1: f is_sequence_on G;

      given i1 be Nat such that

       A2: [i1, 1] in ( Indices G) and

       A3: (G * (i1,1)) in ( rng f);

      consider k1 be object such that

       A4: k1 in ( dom f) and

       A5: (G * (i1,1)) = (f . k1) by A3, FUNCT_1:def 3;

      reconsider k1 as Nat by A4;

      

       A6: 1 <= k1 by A4, FINSEQ_3: 25;

      given i2 be Nat such that

       A7: [i2, ( width G)] in ( Indices G) and

       A8: (G * (i2,( width G))) in ( rng f);

      consider k2 be object such that

       A9: k2 in ( dom f) and

       A10: (G * (i2,( width G))) = (f . k2) by A8, FUNCT_1:def 3;

      reconsider k2 as Nat by A9;

      

       A11: k2 <= ( len f) by A9, FINSEQ_3: 25;

      

       A12: k1 <= ( len f) by A4, FINSEQ_3: 25;

      set g = ( mid (f,k1,k2));

      

       A13: g is_sequence_on G by A1, Th27;

      

       A14: 1 <= k2 by A9, FINSEQ_3: 25;

       A15:

      now

        per cases ;

          suppose k1 <= k2;

          then ( len g) = ((k2 -' k1) + 1) by A6, A11, JORDAN4: 8;

          hence ( len g) >= ( 0 qua Nat + 1) by XREAL_1: 6;

        end;

          suppose k1 > k2;

          then ( len g) = ((k1 -' k2) + 1) by A12, A14, JORDAN4: 9;

          hence ( len g) >= ( 0 qua Nat + 1) by XREAL_1: 6;

        end;

      end;

      

       A16: ( Values G) = { (G * (i,j)) where i,j be Nat : [i, j] in ( Indices G) } by MATRIX_0: 39;

      

       A17: ( proj2 .: ( Values G)) c= ( proj2 .: ( rng g))

      proof

        assume not thesis;

        then

        consider x be Element of REAL such that

         A18: x in ( proj2 .: ( Values G)) and

         A19: not x in ( proj2 .: ( rng g));

        consider p be Element of ( TOP-REAL 2) such that

         A20: p in ( Values G) and

         A21: x = ( proj2 . p) by A18, FUNCT_2: 65;

        consider i0,j0 be Nat such that

         A22: p = (G * (i0,j0)) and

         A23: [i0, j0] in ( Indices G) by A16, A20;

        

         A24: j0 <= ( width G) by A23, MATRIX_0: 32;

        defpred P[ Nat] means 1 <= $1 & $1 <= ( len g) implies for i, j st [i, j] in ( Indices G) & (G * (i,j)) = (g . $1) holds j < j0;

        

         A25: 1 <= j0 by A23, MATRIX_0: 32;

        

         A26: 1 <= i0 & i0 <= ( len G) by A23, MATRIX_0: 32;

        

         A27: for n st P[n] holds P[(n + 1)]

        proof

          let n such that

           A28: 1 <= n & n <= ( len g) implies for i, j st [i, j] in ( Indices G) & (G * (i,j)) = (g . n) holds j < j0 and

           A29: 1 <= (n + 1) and

           A30: (n + 1) <= ( len g);

          let i, j such that

           A31: [i, j] in ( Indices G) and

           A32: (G * (i,j)) = (g . (n + 1));

           A33:

          now

            

             A34: (n + 1) in ( dom g) by A29, A30, FINSEQ_3: 25;

            then

             A35: (G * (i,j)) = (g /. (n + 1)) by A32, PARTFUN1:def 6;

            then

             A36: ( dom proj2 ) = the carrier of ( TOP-REAL 2) & (g /. (n + 1)) in ( rng g) by A32, A34, FUNCT_1: 3, FUNCT_2:def 1;

            

             A37: 1 <= i & i <= ( len G) by A31, MATRIX_0: 32;

            assume

             A38: j = j0;

            x = (p `2 ) by A21, PSCOMP_1:def 6

            .= ((G * (1,j0)) `2 ) by A22, A26, A25, A24, GOBOARD5: 1

            .= ((G * (i,j)) `2 ) by A25, A24, A38, A37, GOBOARD5: 1

            .= ( proj2 . (g /. (n + 1))) by A35, PSCOMP_1:def 6;

            hence contradiction by A19, A36, FUNCT_1:def 6;

          end;

          per cases ;

            suppose n = 0 ;

            then (G * (i,j)) = (G * (i1,1)) by A5, A6, A12, A14, A11, A32, FINSEQ_6: 118;

            then j = 1 by A2, A31, Th26;

            hence thesis by A25, A33, XXREAL_0: 1;

          end;

            suppose

             A39: n <> 0 ;

            then

             A40: 1 <= n by NAT_1: 14;

            

             A41: n <= (n + 1) by NAT_1: 11;

            then n <= ( len g) by A30, XXREAL_0: 2;

            then

             A42: n in ( dom g) by A40, FINSEQ_3: 25;

            then

            consider i1,j1 be Nat such that

             A43: [i1, j1] in ( Indices G) & (g /. n) = (G * (i1,j1)) by A13, GOBOARD1:def 9;

            

             A44: (n + 1) in ( dom g) by A29, A30, FINSEQ_3: 25;

            then (g /. (n + 1)) = (G * (i,j)) by A32, PARTFUN1:def 6;

            then ( |.(i1 - i).| + |.(j1 - j).|) = 1 by A13, A31, A42, A43, A44, GOBOARD1:def 9;

            then

             A45: |.(i1 - i).| = 1 & j1 = j or |.(j1 - j).| = 1 & i1 = i by SEQM_3: 42;

            now

              (g . n) = (g /. n) by A42, PARTFUN1:def 6;

              then

               A46: j1 < j0 by A28, A30, A39, A41, A43, NAT_1: 14, XXREAL_0: 2;

              per cases by A45, SEQM_3: 41;

                suppose j1 = j or j < j1;

                hence thesis by A46, XXREAL_0: 2;

              end;

                suppose j = (j1 + 1);

                then j <= j0 by A46, NAT_1: 13;

                hence thesis by A33, XXREAL_0: 1;

              end;

            end;

            hence thesis;

          end;

        end;

        

         A47: (G * (i2,( width G))) = (g . ( len g)) by A6, A12, A10, A14, A11, JORDAN4: 11;

        

         A48: P[ 0 ];

        for n holds P[n] from NAT_1:sch 2( A48, A27);

        then ( width G) < j0 by A7, A15, A47;

        hence contradiction by A23, MATRIX_0: 32;

      end;

      thus ( proj2 .: ( rng f)) c= ( proj2 .: ( Values G)) by A1, GOBRD13: 8, RELAT_1: 123;

      ( proj2 .: ( rng g)) c= ( proj2 .: ( rng f)) by FINSEQ_6: 119, RELAT_1: 123;

      hence thesis by A17;

    end;

    registration

      let G be Go-board;

      cluster ( Values G) -> non empty;

      coherence

      proof

        ( dom G) is non empty;

        then

        reconsider f = ( rngs G) as non empty non-empty Function by FUNCT_6: 60, RELAT_1: 38;

        ( Union f) is non empty;

        hence thesis by MATRIX_0:def 9;

      end;

    end

    theorem :: JORDAN1H:32

    

     Th32: for G be Go-board holds G = ( GoB (( SgmX ( RealOrd ,( proj1 .: ( Values G)))),( SgmX ( RealOrd ,( proj2 .: ( Values G))))))

    proof

      let G be Go-board;

      set v1 = ( SgmX ( RealOrd ,( proj1 .: ( Values G)))), v2 = ( SgmX ( RealOrd ,( proj2 .: ( Values G))));

      

       A1: ( width G) = ( card ( proj2 .: ( Values G))) by Th19

      .= ( len v2) by Th9;

      

       A2: for n, m st [n, m] in ( Indices G) holds (G * (n,m)) = |[(v1 . n), (v2 . m)]|

      proof

        let n, m;

        assume

         A3: [n, m] in ( Indices G);

        then

         A4: 1 <= n & n <= ( len G) by MATRIX_0: 32;

        

         A5: 1 <= m & m <= ( width G) by A3, MATRIX_0: 32;

        (v1 . n) = ((G * (n,1)) `1 ) by A4, Th28;

        then

         A6: (v1 . n) = ((G * (n,m)) `1 ) by A4, A5, GOBOARD5: 2;

        (v2 . m) = ((G * (1,m)) `2 ) by A5, Th29;

        then (v2 . m) = ((G * (n,m)) `2 ) by A4, A5, GOBOARD5: 1;

        hence thesis by A6, EUCLID: 53;

      end;

      ( len G) = ( card ( proj1 .: ( Values G))) by Th16

      .= ( len v1) by Th9;

      hence thesis by A1, A2, GOBOARD2:def 1;

    end;

    theorem :: JORDAN1H:33

    

     Th33: for f be non empty FinSequence of ( TOP-REAL 2), G be Go-board st ( proj1 .: ( rng f)) = ( proj1 .: ( Values G)) & ( proj2 .: ( rng f)) = ( proj2 .: ( Values G)) holds G = ( GoB f)

    proof

      let f be non empty FinSequence of ( TOP-REAL 2), G be Go-board;

      ( X_axis f) = ( proj1 * f) by Th10;

      then ( rng ( X_axis f)) = ( proj1 .: ( rng f)) by RELAT_1: 127;

      then

       A1: ( Incr ( X_axis f)) = ( SgmX ( RealOrd ,( proj1 .: ( rng f)))) by Th8;

      ( Y_axis f) = ( proj2 * f) by Th11;

      then ( rng ( Y_axis f)) = ( proj2 .: ( rng f)) by RELAT_1: 127;

      then

       A2: ( Incr ( Y_axis f)) = ( SgmX ( RealOrd ,( proj2 .: ( rng f)))) by Th8;

      assume ( proj1 .: ( rng f)) = ( proj1 .: ( Values G)) & ( proj2 .: ( rng f)) = ( proj2 .: ( Values G));

      

      hence G = ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) by A1, A2, Th32

      .= ( GoB f) by GOBOARD2:def 2;

    end;

    theorem :: JORDAN1H:34

    

     Th34: for f be non empty FinSequence of ( TOP-REAL 2), G be Go-board st f is_sequence_on G & (ex i st [1, i] in ( Indices G) & (G * (1,i)) in ( rng f)) & (ex i st [i, 1] in ( Indices G) & (G * (i,1)) in ( rng f)) & (ex i st [( len G), i] in ( Indices G) & (G * (( len G),i)) in ( rng f)) & (ex i st [i, ( width G)] in ( Indices G) & (G * (i,( width G))) in ( rng f)) holds G = ( GoB f)

    proof

      let f be non empty FinSequence of ( TOP-REAL 2), G be Go-board such that

       A1: f is_sequence_on G;

      given i1 be Nat such that

       A2: [1, i1] in ( Indices G) & (G * (1,i1)) in ( rng f);

      given i2 be Nat such that

       A3: [i2, 1] in ( Indices G) & (G * (i2,1)) in ( rng f);

      given i3 be Nat such that

       A4: [( len G), i3] in ( Indices G) & (G * (( len G),i3)) in ( rng f);

      given i4 be Nat such that

       A5: [i4, ( width G)] in ( Indices G) & (G * (i4,( width G))) in ( rng f);

      

       A6: ( proj2 .: ( rng f)) = ( proj2 .: ( Values G)) by A1, A3, A5, Th31;

      ( proj1 .: ( rng f)) = ( proj1 .: ( Values G)) by A1, A2, A4, Th30;

      hence thesis by A6, Th33;

    end;

    begin

    theorem :: JORDAN1H:35

    

     Th35: 1 <= i implies [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT

    proof

      set i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/];

      ((((i - 2) / (2 |^ (n -' m))) + 2) - 1) = (((i - 2) / (2 |^ (n -' m))) + (2 - 1));

      then

       A1: (((i - 2) / (2 |^ (n -' m))) + 1) < i1 by INT_1:def 6;

      ((n -' m) + 1) >= ( 0 qua Nat + 1) & ((n -' m) + 1) <= (2 |^ (n -' m)) by NEWTON: 85, XREAL_1: 6;

      then ( 0 qua Nat + 1) <= (2 |^ (n -' m)) by XXREAL_0: 2;

      then

       A2: (( - 1) / 1) <= (( - 1) / (2 |^ (n -' m))) by XREAL_1: 120;

      assume 1 <= i;

      then (1 - 2) <= (i - 2) by XREAL_1: 9;

      then (( - 1) / (2 |^ (n -' m))) <= ((i - 2) / (2 |^ (n -' m))) by XREAL_1: 72;

      then ( - 1) <= ((i - 2) / (2 |^ (n -' m))) by A2, XXREAL_0: 2;

      then (( - 1) + 1) <= (((i - 2) / (2 |^ (n -' m))) + 1) by XREAL_1: 6;

      hence thesis by A1, INT_1: 3;

    end;

    theorem :: JORDAN1H:36

    

     Th36: m <= n & 1 <= i & (i + 1) <= ( len ( Gauge (C,n))) implies 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & ( [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1) <= ( len ( Gauge (C,m)))

    proof

      assume that

       A1: m <= n and

       A2: 1 <= i and

       A3: (i + 1) <= ( len ( Gauge (C,n)));

      

       A4: ((n -' m) + 1) <= (2 |^ (n -' m)) by NEWTON: 85;

      (i + 1) <= ((2 |^ n) + (2 + 1)) by A3, JORDAN8:def 1;

      then (i + 1) <= (((2 |^ n) + 2) + 1);

      then i <= ((2 |^ n) + 2) by XREAL_1: 6;

      then (i - 2) <= (2 |^ n) by XREAL_1: 20;

      then (i - 2) <= (2 |^ (m + (n -' m))) by A1, XREAL_1: 235;

      then ((i - 2) * 1) <= ((2 |^ m) * (2 |^ (n -' m))) by NEWTON: 8;

      then ((i - 2) / (2 |^ (n -' m))) <= ((2 |^ m) / 1) by A4, XREAL_1: 102;

      then (((i - 2) / (2 |^ (n -' m))) + 3) <= ((2 |^ m) + 3) by XREAL_1: 6;

      then

       A5: (((i - 2) / (2 |^ (n -' m))) + 3) <= ( len ( Gauge (C,m))) by JORDAN8:def 1;

      set i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/];

      ((((i - 2) / (2 |^ (n -' m))) + 2) - 1) = (((i - 2) / (2 |^ (n -' m))) + (2 - 1));

      then

       A6: (((i - 2) / (2 |^ (n -' m))) + 1) < i1 by INT_1:def 6;

      ((n -' m) + 1) >= ( 0 qua Nat + 1) by XREAL_1: 6;

      then ( 0 qua Nat + 1) <= (2 |^ (n -' m)) by A4, XXREAL_0: 2;

      then

       A7: (( - 1) / 1) <= (( - 1) / (2 |^ (n -' m))) by XREAL_1: 120;

      (1 - 2) <= (i - 2) by A2, XREAL_1: 9;

      then (( - 1) / (2 |^ (n -' m))) <= ((i - 2) / (2 |^ (n -' m))) by XREAL_1: 72;

      then ( - 1) <= ((i - 2) / (2 |^ (n -' m))) by A7, XXREAL_0: 2;

      then (( - 1) + 1) <= (((i - 2) / (2 |^ (n -' m))) + 1) by XREAL_1: 6;

      then i1 >= (1 + 0 qua Nat) by A6, INT_1: 7;

      hence 1 <= i1;

      i1 <= (((i - 2) / (2 |^ (n -' m))) + 2) by INT_1:def 6;

      then (i1 + 1) <= ((((i - 2) / (2 |^ (n -' m))) + 2) + 1) by XREAL_1: 6;

      hence thesis by A5, XXREAL_0: 2;

    end;

    theorem :: JORDAN1H:37

    

     Th37: m <= n & 1 <= i & (i + 1) <= ( len ( Gauge (C,n))) & 1 <= j & (j + 1) <= ( width ( Gauge (C,n))) implies ex i1, j1 st i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & ( cell (( Gauge (C,n)),i,j)) c= ( cell (( Gauge (C,m)),i1,j1))

    proof

      assume that

       A1: m <= n and

       A2: 1 <= i and

       A3: (i + 1) <= ( len ( Gauge (C,n))) and

       A4: 1 <= j and

       A5: (j + 1) <= ( width ( Gauge (C,n)));

      reconsider i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/], j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] as Nat by A2, A4, Th35;

      set Gm = ( Gauge (C,m)), Gn = ( Gauge (C,n));

      

       A6: (2 |^ (n -' m)) > (n -' m) by NEWTON: 86;

      take i1, j1;

      thus i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/];

      thus j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/];

      let e be object;

      assume

       A7: e in ( cell (( Gauge (C,n)),i,j));

      then

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

      

       A8: (p `2 ) <= ((Gn * (i,(j + 1))) `2 ) by A2, A3, A4, A5, A7, JORDAN9: 17;

      i <= ( len Gn) & j <= ( width Gn) by A3, A5, NAT_1: 13;

      then [i, j] in ( Indices Gn) by A2, A4, MATRIX_0: 30;

      then

       A9: (Gn * (i,j)) = |[(( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ n)) * (i - 2))), (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ n)) * (j - 2)))]| by JORDAN8:def 1;

      

      then

       A10: ((Gn * (i,j)) `1 ) = (( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ n)) * ((i - 2) / 1))) by EUCLID: 52

      .= (( W-bound C) + (((( E-bound C) - ( W-bound C)) / 1) * ((i - 2) / (2 |^ n)))) by XCMPLX_1: 85;

      

       A11: ((Gn * (i,j)) `1 ) <= (p `1 ) by A2, A3, A4, A5, A7, JORDAN9: 17;

      

       A12: ((Gn * (i,j)) `2 ) = (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ n)) * ((j - 2) / 1))) by A9, EUCLID: 52

      .= (( S-bound C) + (((( N-bound C) - ( S-bound C)) / 1) * ((j - 2) / (2 |^ n)))) by XCMPLX_1: 85;

      

       A13: (p `1 ) <= ((Gn * ((i + 1),j)) `1 ) by A2, A3, A4, A5, A7, JORDAN9: 17;

      ( E-bound C) >= (( W-bound C) + 0 qua Nat) by SPRECT_1: 21;

      then

       A14: (( E-bound C) - ( W-bound C)) >= 0 by XREAL_1: 19;

      1 <= (j + 1) & i <= ( len Gn) by A3, NAT_1: 11, NAT_1: 13;

      then [i, (j + 1)] in ( Indices Gn) by A2, A5, MATRIX_0: 30;

      then (Gn * (i,(j + 1))) = |[(( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ n)) * (i - 2))), (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ n)) * ((j + 1) - 2)))]| by JORDAN8:def 1;

      

      then

       A15: ((Gn * (i,(j + 1))) `2 ) = (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ n)) * (((j + 1) - 2) / 1))) by EUCLID: 52

      .= (( S-bound C) + (((( N-bound C) - ( S-bound C)) / 1) * (((j + 1) - 2) / (2 |^ n)))) by XCMPLX_1: 85;

      ((n -' m) + 1) >= ( 0 qua Nat + 1) & ((n -' m) + 1) <= (2 |^ (n -' m)) by NEWTON: 85, XREAL_1: 6;

      then ( 0 qua Nat + 1) <= (2 |^ (n -' m)) by XXREAL_0: 2;

      then

       A16: (( - 1) / 1) <= (( - 1) / (2 |^ (n -' m))) by XREAL_1: 120;

      

       A17: ((Gn * (i,j)) `2 ) <= (p `2 ) by A2, A3, A4, A5, A7, JORDAN9: 17;

      1 <= (i + 1) & j <= ( width Gn) by A5, NAT_1: 11, NAT_1: 13;

      then [(i + 1), j] in ( Indices Gn) by A3, A4, MATRIX_0: 30;

      then (Gn * ((i + 1),j)) = |[(( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ n)) * ((i + 1) - 2))), (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ n)) * (j - 2)))]| by JORDAN8:def 1;

      

      then

       A18: ((Gn * ((i + 1),j)) `1 ) = (( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ n)) * (((i + 1) - 2) / 1))) by EUCLID: 52

      .= (( W-bound C) + (((( E-bound C) - ( W-bound C)) / 1) * (((i + 1) - 2) / (2 |^ n)))) by XCMPLX_1: 85;

      ((((i - 2) / (2 |^ (n -' m))) + 2) - 1) = (((i - 2) / (2 |^ (n -' m))) + (2 - 1));

      then

       A19: (((i - 2) / (2 |^ (n -' m))) + 1) < i1 by INT_1:def 6;

      (1 - 2) <= (i - 2) by A2, XREAL_1: 9;

      then (( - 1) / (2 |^ (n -' m))) <= ((i - 2) / (2 |^ (n -' m))) by XREAL_1: 72;

      then ( - 1) <= ((i - 2) / (2 |^ (n -' m))) by A16, XXREAL_0: 2;

      then (( - 1) + 1) <= (((i - 2) / (2 |^ (n -' m))) + 1) by XREAL_1: 6;

      then

       A20: i1 >= (1 + 0 qua Nat) by A19, INT_1: 7;

      ( N-bound C) >= (( S-bound C) + 0 qua Nat) by SPRECT_1: 22;

      then

       A21: (( N-bound C) - ( S-bound C)) >= 0 by XREAL_1: 19;

      ((((i - 2) / (2 |^ (n -' m))) + 2) - 1) < i1 by INT_1:def 6;

      then (((i - 2) / (2 |^ (n -' m))) + 2) < (i1 + 1) by XREAL_1: 19;

      then ((i - 2) / (2 |^ (n -' m))) < ((i1 + 1) - 2) by XREAL_1: 20;

      then ((i - 2) + 1) <= (((i1 + 1) - 2) * (2 |^ (n -' m))) by A6, INT_1: 7, XREAL_1: 77;

      then (((i + 1) - 2) / (2 |^ (n -' m))) <= ((i1 + 1) - 2) by A6, XREAL_1: 79;

      then ((((i + 1) - 2) / (2 |^ (n -' m))) / (2 |^ m)) <= (((i1 + 1) - 2) / (2 |^ m)) by XREAL_1: 72;

      then (((i + 1) - 2) / ((2 |^ (n -' m)) * (2 |^ m))) <= (((i1 + 1) - 2) / (2 |^ m)) by XCMPLX_1: 78;

      then (((i + 1) - 2) / (2 |^ ((n -' m) + m))) <= (((i1 + 1) - 2) / (2 |^ m)) by NEWTON: 8;

      then (((i + 1) - 2) / (2 |^ n)) <= (((i1 + 1) - 2) / (2 |^ m)) by A1, XREAL_1: 235;

      then

       A22: ((( E-bound C) - ( W-bound C)) * (((i + 1) - 2) / (2 |^ n))) <= ((( E-bound C) - ( W-bound C)) * (((i1 + 1) - 2) / (2 |^ m))) by A14, XREAL_1: 64;

      i1 <= (((i - 2) / (2 |^ (n -' m))) + 2) by INT_1:def 6;

      then (i1 - 2) <= ((i - 2) / (2 |^ (n -' m))) by XREAL_1: 20;

      then ((i1 - 2) / (2 |^ m)) <= (((i - 2) / (2 |^ (n -' m))) / (2 |^ m)) by XREAL_1: 72;

      then ((i1 - 2) / (2 |^ m)) <= ((i - 2) / ((2 |^ (n -' m)) * (2 |^ m))) by XCMPLX_1: 78;

      then ((i1 - 2) / (2 |^ m)) <= ((i - 2) / (2 |^ ((n -' m) + m))) by NEWTON: 8;

      then ((i1 - 2) / (2 |^ m)) <= ((i - 2) / (2 |^ n)) by A1, XREAL_1: 235;

      then

       A23: ((( E-bound C) - ( W-bound C)) * ((i1 - 2) / (2 |^ m))) <= ((( E-bound C) - ( W-bound C)) * ((i - 2) / (2 |^ n))) by A14, XREAL_1: 64;

      j1 <= (((j - 2) / (2 |^ (n -' m))) + 2) by INT_1:def 6;

      then (j1 - 2) <= ((j - 2) / (2 |^ (n -' m))) by XREAL_1: 20;

      then ((j1 - 2) / (2 |^ m)) <= (((j - 2) / (2 |^ (n -' m))) / (2 |^ m)) by XREAL_1: 72;

      then ((j1 - 2) / (2 |^ m)) <= ((j - 2) / ((2 |^ (n -' m)) * (2 |^ m))) by XCMPLX_1: 78;

      then ((j1 - 2) / (2 |^ m)) <= ((j - 2) / (2 |^ ((n -' m) + m))) by NEWTON: 8;

      then ((j1 - 2) / (2 |^ m)) <= ((j - 2) / (2 |^ n)) by A1, XREAL_1: 235;

      then

       A24: ((( N-bound C) - ( S-bound C)) * ((j1 - 2) / (2 |^ m))) <= ((( N-bound C) - ( S-bound C)) * ((j - 2) / (2 |^ n))) by A21, XREAL_1: 64;

      ((((j - 2) / (2 |^ (n -' m))) + 2) - 1) = (((j - 2) / (2 |^ (n -' m))) + (2 - 1));

      then

       A25: (((j - 2) / (2 |^ (n -' m))) + 1) < j1 by INT_1:def 6;

      (1 - 2) <= (j - 2) by A4, XREAL_1: 9;

      then (( - 1) / (2 |^ (n -' m))) <= ((j - 2) / (2 |^ (n -' m))) by XREAL_1: 72;

      then ( - 1) <= ((j - 2) / (2 |^ (n -' m))) by A16, XXREAL_0: 2;

      then (( - 1) + 1) <= (((j - 2) / (2 |^ (n -' m))) + 1) by XREAL_1: 6;

      then

       A26: j1 >= (1 + 0 qua Nat) by A25, INT_1: 7;

      ((((j - 2) / (2 |^ (n -' m))) + 2) - 1) < j1 by INT_1:def 6;

      then (((j - 2) / (2 |^ (n -' m))) + 2) < (j1 + 1) by XREAL_1: 19;

      then ((j - 2) / (2 |^ (n -' m))) < ((j1 + 1) - 2) by XREAL_1: 20;

      then ((j - 2) + 1) <= (((j1 + 1) - 2) * (2 |^ (n -' m))) by A6, INT_1: 7, XREAL_1: 77;

      then (((j + 1) - 2) / (2 |^ (n -' m))) <= ((j1 + 1) - 2) by A6, XREAL_1: 79;

      then ((((j + 1) - 2) / (2 |^ (n -' m))) / (2 |^ m)) <= (((j1 + 1) - 2) / (2 |^ m)) by XREAL_1: 72;

      then (((j + 1) - 2) / ((2 |^ (n -' m)) * (2 |^ m))) <= (((j1 + 1) - 2) / (2 |^ m)) by XCMPLX_1: 78;

      then (((j + 1) - 2) / (2 |^ ((n -' m) + m))) <= (((j1 + 1) - 2) / (2 |^ m)) by NEWTON: 8;

      then (((j + 1) - 2) / (2 |^ n)) <= (((j1 + 1) - 2) / (2 |^ m)) by A1, XREAL_1: 235;

      then

       A27: ((( N-bound C) - ( S-bound C)) * (((j + 1) - 2) / (2 |^ n))) <= ((( N-bound C) - ( S-bound C)) * (((j1 + 1) - 2) / (2 |^ m))) by A21, XREAL_1: 64;

      ( len ( Gauge (C,m))) = ( width ( Gauge (C,m))) & ( len ( Gauge (C,n))) = ( width ( Gauge (C,n))) by JORDAN8:def 1;

      then

       A28: (j1 + 1) <= ( width ( Gauge (C,m))) by A1, A4, A5, Th36;

      then

       A29: j1 <= ( width ( Gauge (C,m))) by NAT_1: 13;

      

       A30: (i1 + 1) <= ( len ( Gauge (C,m))) by A1, A2, A3, Th36;

      then 1 <= (j1 + 1) & i1 <= ( len ( Gauge (C,m))) by NAT_1: 11, NAT_1: 13;

      then [i1, (j1 + 1)] in ( Indices Gm) by A20, A28, MATRIX_0: 30;

      then (Gm * (i1,(j1 + 1))) = |[(( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ m)) * (i1 - 2))), (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ m)) * ((j1 + 1) - 2)))]| by JORDAN8:def 1;

      

      then ((Gm * (i1,(j1 + 1))) `2 ) = (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ m)) * (((j1 + 1) - 2) / 1))) by EUCLID: 52

      .= (( S-bound C) + (((( N-bound C) - ( S-bound C)) / 1) * (((j1 + 1) - 2) / (2 |^ m)))) by XCMPLX_1: 85;

      then ((Gn * (i,(j + 1))) `2 ) <= ((Gm * (i1,(j1 + 1))) `2 ) by A15, A27, XREAL_1: 6;

      then

       A31: (p `2 ) <= ((Gm * (i1,(j1 + 1))) `2 ) by A8, XXREAL_0: 2;

      i1 <= ( len ( Gauge (C,m))) by A30, NAT_1: 13;

      then [i1, j1] in ( Indices Gm) by A20, A26, A29, MATRIX_0: 30;

      then

       A32: (Gm * (i1,j1)) = |[(( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ m)) * (i1 - 2))), (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ m)) * (j1 - 2)))]| by JORDAN8:def 1;

      

      then ((Gm * (i1,j1)) `1 ) = (( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ m)) * ((i1 - 2) / 1))) by EUCLID: 52

      .= (( W-bound C) + (((( E-bound C) - ( W-bound C)) / 1) * ((i1 - 2) / (2 |^ m)))) by XCMPLX_1: 85;

      then ((Gm * (i1,j1)) `1 ) <= ((Gn * (i,j)) `1 ) by A10, A23, XREAL_1: 6;

      then

       A33: ((Gm * (i1,j1)) `1 ) <= (p `1 ) by A11, XXREAL_0: 2;

      ((Gm * (i1,j1)) `2 ) = (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ m)) * ((j1 - 2) / 1))) by A32, EUCLID: 52

      .= (( S-bound C) + (((( N-bound C) - ( S-bound C)) / 1) * ((j1 - 2) / (2 |^ m)))) by XCMPLX_1: 85;

      then ((Gm * (i1,j1)) `2 ) <= ((Gn * (i,j)) `2 ) by A12, A24, XREAL_1: 6;

      then

       A34: ((Gm * (i1,j1)) `2 ) <= (p `2 ) by A17, XXREAL_0: 2;

      1 <= (i1 + 1) & j1 <= ( width ( Gauge (C,m))) by A28, NAT_1: 11, NAT_1: 13;

      then [(i1 + 1), j1] in ( Indices Gm) by A26, A30, MATRIX_0: 30;

      then (Gm * ((i1 + 1),j1)) = |[(( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ m)) * ((i1 + 1) - 2))), (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ m)) * (j1 - 2)))]| by JORDAN8:def 1;

      

      then ((Gm * ((i1 + 1),j1)) `1 ) = (( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ m)) * (((i1 + 1) - 2) / 1))) by EUCLID: 52

      .= (( W-bound C) + (((( E-bound C) - ( W-bound C)) / 1) * (((i1 + 1) - 2) / (2 |^ m)))) by XCMPLX_1: 85;

      then ((Gn * ((i + 1),j)) `1 ) <= ((Gm * ((i1 + 1),j1)) `1 ) by A18, A22, XREAL_1: 6;

      then (p `1 ) <= ((Gm * ((i1 + 1),j1)) `1 ) by A13, XXREAL_0: 2;

      hence thesis by A20, A26, A30, A28, A33, A34, A31, JORDAN9: 17;

    end;

    theorem :: JORDAN1H:38

    

     Th38: m <= n & 1 <= i & (i + 1) <= ( len ( Gauge (C,n))) & 1 <= j & (j + 1) <= ( width ( Gauge (C,n))) implies ex i1, j1 st 1 <= i1 & (i1 + 1) <= ( len ( Gauge (C,m))) & 1 <= j1 & (j1 + 1) <= ( width ( Gauge (C,m))) & ( cell (( Gauge (C,n)),i,j)) c= ( cell (( Gauge (C,m)),i1,j1))

    proof

      assume that

       A1: m <= n and

       A2: 1 <= i & (i + 1) <= ( len ( Gauge (C,n))) and

       A3: 1 <= j & (j + 1) <= ( width ( Gauge (C,n)));

      consider i1, j1 such that

       A4: i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] and

       A5: j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] and

       A6: ( cell (( Gauge (C,n)),i,j)) c= ( cell (( Gauge (C,m)),i1,j1)) by A1, A2, A3, Th37;

      take i1, j1;

      thus 1 <= i1 & (i1 + 1) <= ( len ( Gauge (C,m))) by A1, A2, A4, Th36;

      ( len ( Gauge (C,m))) = ( width ( Gauge (C,m))) & ( len ( Gauge (C,n))) = ( width ( Gauge (C,n))) by JORDAN8:def 1;

      hence 1 <= j1 & (j1 + 1) <= ( width ( Gauge (C,m))) by A1, A3, A5, Th36;

      thus thesis by A6;

    end;

    theorem :: JORDAN1H:39

    for P be Subset of ( TOP-REAL 2) st P is bounded holds not ( UBD P) is bounded

    proof

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

      assume P is bounded;

      then ( UBD P) is_outside_component_of P by JORDAN2C: 68;

      hence thesis by JORDAN2C:def 3;

    end;

    theorem :: JORDAN1H:40

    

     Th40: for f be non constant standard special_circular_sequence st ( Rotate (f,p)) is clockwise_oriented holds f is clockwise_oriented

    proof

      let f be non constant standard special_circular_sequence;

      assume ( Rotate (f,p)) is clockwise_oriented;

      then

      reconsider g = ( Rotate (f,p)) as clockwise_oriented non constant standard special_circular_sequence;

      1 < i & i < ( len f) implies (f /. i) <> (f /. 1) by GOBOARD7: 36;

      then f = ( Rotate (g,(f /. 1))) by FINSEQ_6: 181;

      hence thesis;

    end;

    theorem :: JORDAN1H:41

    for f be non constant standard special_circular_sequence st ( LeftComp f) = ( UBD ( L~ f)) holds f is clockwise_oriented

    proof

      let f be non constant standard special_circular_sequence such that

       A1: ( LeftComp f) = ( UBD ( L~ f));

      set g = ( Rotate (f,( N-min ( L~ f))));

      assume not thesis;

      then not g is clockwise_oriented by Th40;

      then

       A2: ( Rev g) is clockwise_oriented by REVROT_1: 38;

      ( L~ f) = ( L~ g) by REVROT_1: 33;

      

      then ( UBD ( L~ f)) = ( UBD ( L~ ( Rev g))) by SPPOL_2: 22

      .= ( LeftComp ( Rev g)) by A2, GOBRD14: 36

      .= ( RightComp g) by GOBOARD9: 23

      .= ( RightComp f) by REVROT_1: 37;

      hence contradiction by A1, SPRECT_4: 6;

    end;

    begin

    theorem :: JORDAN1H:42

    

     Th42: for f be non constant standard special_circular_sequence holds (( Cl ( LeftComp f)) ` ) = ( RightComp f)

    proof

      let f be non constant standard special_circular_sequence;

      

       A1: (( Cl ( LeftComp f)) ` ) misses ( Cl ( LeftComp f)) by SUBSET_1: 24;

      (( Cl ( LeftComp f)) \/ ( RightComp f)) = ((( L~ f) \/ ( LeftComp f)) \/ ( RightComp f)) by GOBRD14: 22

      .= ((( L~ f) \/ ( RightComp f)) \/ ( LeftComp f)) by XBOOLE_1: 4

      .= the carrier of ( TOP-REAL 2) by GOBRD14: 15;

      hence (( Cl ( LeftComp f)) ` ) c= ( RightComp f) by A1, XBOOLE_1: 73;

      

       A2: ( RightComp f) misses ( LeftComp f) by GOBRD14: 14;

      ( Cl ( LeftComp f)) = (( LeftComp f) \/ ( L~ f)) & ( L~ f) misses ( RightComp f) by GOBRD14: 22, SPRECT_3: 25;

      then ( Cl ( LeftComp f)) misses ( RightComp f) by A2, XBOOLE_1: 70;

      hence thesis by SUBSET_1: 23;

    end;

    theorem :: JORDAN1H:43

    for f be non constant standard special_circular_sequence holds (( Cl ( RightComp f)) ` ) = ( LeftComp f)

    proof

      let f be non constant standard special_circular_sequence;

      

       A1: (( Cl ( RightComp f)) ` ) misses ( Cl ( RightComp f)) by SUBSET_1: 24;

      (( Cl ( RightComp f)) \/ ( LeftComp f)) = ((( L~ f) \/ ( RightComp f)) \/ ( LeftComp f)) by GOBRD14: 21

      .= the carrier of ( TOP-REAL 2) by GOBRD14: 15;

      hence (( Cl ( RightComp f)) ` ) c= ( LeftComp f) by A1, XBOOLE_1: 73;

      

       A2: ( LeftComp f) misses ( RightComp f) by GOBRD14: 14;

      ( Cl ( RightComp f)) = (( RightComp f) \/ ( L~ f)) & ( L~ f) misses ( LeftComp f) by GOBRD14: 21, SPRECT_3: 26;

      then ( Cl ( RightComp f)) misses ( LeftComp f) by A2, XBOOLE_1: 70;

      hence thesis by SUBSET_1: 23;

    end;

    theorem :: JORDAN1H:44

    

     Th44: C is connected implies ( GoB ( Cage (C,n))) = ( Gauge (C,n))

    proof

      

       A1: ( S-max ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) & ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 42, SPRECT_2: 46;

      assume

       A2: C is connected;

      then

      consider iw be Nat such that

       A3: 1 <= iw & iw <= ( width ( Gauge (C,n))) and

       A4: ( W-min ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (1,iw)) by JORDAN1D: 30;

      

       A5: ( N-min ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) & ( Cage (C,n)) is_sequence_on ( Gauge (C,n)) by A2, JORDAN9:def 1, SPRECT_2: 39;

      consider ie be Nat such that

       A6: 1 <= ie & ie <= ( width ( Gauge (C,n))) and

       A7: (( Gauge (C,n)) * (( len ( Gauge (C,n))),ie)) = ( E-max ( L~ ( Cage (C,n)))) by A2, JORDAN1D: 25;

      

       A8: 1 <= ( len ( Gauge (C,n))) by GOBRD11: 34;

      then

       A9: [( len ( Gauge (C,n))), ie] in ( Indices ( Gauge (C,n))) by A6, MATRIX_0: 30;

      consider iS be Nat such that

       A10: 1 <= iS & iS <= ( len ( Gauge (C,n))) and

       A11: (( Gauge (C,n)) * (iS,1)) = ( S-max ( L~ ( Cage (C,n)))) by A2, JORDAN1D: 28;

      

       A12: 1 <= ( width ( Gauge (C,n))) by GOBRD11: 34;

      then

       A13: [iS, 1] in ( Indices ( Gauge (C,n))) by A10, MATRIX_0: 30;

      consider IN be Nat such that

       A14: 1 <= IN & IN <= ( len ( Gauge (C,n))) and

       A15: (( Gauge (C,n)) * (IN,( width ( Gauge (C,n))))) = ( N-min ( L~ ( Cage (C,n)))) by A2, JORDAN1D: 21;

      

       A16: [IN, ( width ( Gauge (C,n)))] in ( Indices ( Gauge (C,n))) by A12, A14, MATRIX_0: 30;

       [1, iw] in ( Indices ( Gauge (C,n))) by A8, A3, MATRIX_0: 30;

      hence thesis by A4, A11, A13, A7, A9, A1, A15, A16, A5, Th34, SPRECT_2: 43;

    end;

    theorem :: JORDAN1H:45

    C is connected implies ( N-min C) in ( right_cell (( Cage (C,n)),1))

    proof

      assume

       A1: C is connected;

      then

      consider i such that

       A2: 1 <= i and

       A3: (i + 1) <= ( len ( Gauge (C,n))) and

       A4: (( Cage (C,n)) /. 1) = (( Gauge (C,n)) * (i,( width ( Gauge (C,n))))) and

       A5: (( Cage (C,n)) /. 2) = (( Gauge (C,n)) * ((i + 1),( width ( Gauge (C,n))))) and

       A6: ( N-min C) in ( cell (( Gauge (C,n)),i,(( width ( Gauge (C,n))) -' 1))) and ( N-min C) <> (( Gauge (C,n)) * (i,(( width ( Gauge (C,n))) -' 1))) by JORDAN9:def 1;

      

       A7: for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices ( GoB ( Cage (C,n)))) & [i2, j2] in ( Indices ( GoB ( Cage (C,n)))) & (( Cage (C,n)) /. 1) = (( GoB ( Cage (C,n))) * (i1,j1)) & (( Cage (C,n)) /. (1 + 1)) = (( GoB ( Cage (C,n))) * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & ( cell (( Gauge (C,n)),i,(( width ( Gauge (C,n))) -' 1))) = ( cell (( GoB ( Cage (C,n))),i1,j1)) or (i1 + 1) = i2 & j1 = j2 & ( cell (( Gauge (C,n)),i,(( width ( Gauge (C,n))) -' 1))) = ( cell (( GoB ( Cage (C,n))),i1,(j1 -' 1))) or i1 = (i2 + 1) & j1 = j2 & ( cell (( Gauge (C,n)),i,(( width ( Gauge (C,n))) -' 1))) = ( cell (( GoB ( Cage (C,n))),i2,j2)) or i1 = i2 & j1 = (j2 + 1) & ( cell (( Gauge (C,n)),i,(( width ( Gauge (C,n))) -' 1))) = ( cell (( GoB ( Cage (C,n))),(i1 -' 1),j2))

      proof

         0 <> ( width ( Gauge (C,n))) by MATRIX_0:def 10;

        then

         A8: 1 <= ( width ( Gauge (C,n))) by NAT_1: 14;

        

         A9: ( GoB ( Cage (C,n))) = ( Gauge (C,n)) by A1, Th44;

        let i1,j1,i2,j2 be Nat such that

         A10: [i1, j1] in ( Indices ( GoB ( Cage (C,n)))) and

         A11: [i2, j2] in ( Indices ( GoB ( Cage (C,n)))) and

         A12: (( Cage (C,n)) /. 1) = (( GoB ( Cage (C,n))) * (i1,j1)) and

         A13: (( Cage (C,n)) /. (1 + 1)) = (( GoB ( Cage (C,n))) * (i2,j2));

        1 <= (i + 1) by NAT_1: 11;

        then

         A14: [(i + 1), ( width ( Gauge (C,n)))] in ( Indices ( Gauge (C,n))) by A3, A8, MATRIX_0: 30;

        then

         A15: i2 = (i + 1) by A5, A11, A13, A9, GOBOARD1: 5;

        i < ( len ( Gauge (C,n))) by A3, NAT_1: 13;

        then

         A16: [i, ( width ( Gauge (C,n)))] in ( Indices ( Gauge (C,n))) by A2, A8, MATRIX_0: 30;

        then

         A17: i1 = i by A4, A10, A12, A9, GOBOARD1: 5;

        

         A18: j2 = ( width ( Gauge (C,n))) by A5, A11, A13, A9, A14, GOBOARD1: 5;

        per cases by A4, A10, A12, A9, A16, A15, A18, GOBOARD1: 5;

          case i1 = i2 & (j1 + 1) = j2;

          hence thesis by A17, A15;

        end;

          case (i1 + 1) = i2 & j1 = j2;

          thus thesis by A4, A10, A12, A9, A16, A17, GOBOARD1: 5;

        end;

          case i1 = (i2 + 1) & j1 = j2;

          hence thesis by A17, A15;

        end;

          case i1 = i2 & j1 = (j2 + 1);

          hence thesis by A17, A15;

        end;

      end;

      (1 + 1) <= ( len ( Cage (C,n))) by GOBOARD7: 34, XXREAL_0: 2;

      hence thesis by A6, A7, GOBOARD5:def 6;

    end;

    theorem :: JORDAN1H:46

    

     Th46: C is connected & i <= j implies ( L~ ( Cage (C,j))) c= ( Cl ( RightComp ( Cage (C,i))))

    proof

      assume that

       A1: C is connected and

       A2: i <= j and

       A3: not ( L~ ( Cage (C,j))) c= ( Cl ( RightComp ( Cage (C,i))));

      

       A4: ( Cage (C,j)) is_sequence_on ( Gauge (C,j)) by A1, JORDAN9:def 1;

      

       A5: ( GoB ( Cage (C,i))) = ( Gauge (C,i)) by A1, Th44;

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

       A6: p in ( L~ ( Cage (C,j))) and

       A7: not p in ( Cl ( RightComp ( Cage (C,i)))) by A3;

      consider i1 such that

       A8: 1 <= i1 and

       A9: (i1 + 1) <= ( len ( Cage (C,j))) and

       A10: p in ( LSeg (( Cage (C,j)),i1)) by A6, SPPOL_2: 13;

      

       A11: ( GoB ( Cage (C,j))) = ( Gauge (C,j)) by A1, Th44;

      then

       A12: ( right_cell (( Cage (C,j)),i1,( Gauge (C,j)))) = ( right_cell (( Cage (C,j)),i1)) by A8, A9, Th23;

      

       A13: i1 < ( len ( Cage (C,j))) by A9, NAT_1: 13;

      now

        ex i2,j2 be Nat st 1 <= i2 & (i2 + 1) <= ( len ( Gauge (C,i))) & 1 <= j2 & (j2 + 1) <= ( width ( Gauge (C,i))) & ( right_cell (( Cage (C,j)),i1)) c= ( cell (( Gauge (C,i)),i2,j2))

        proof

          set f = ( Cage (C,j));

          

           A14: i1 in ( dom f) by A8, A13, FINSEQ_3: 25;

          then

          consider i4,j4 be Nat such that

           A15: [i4, j4] in ( Indices ( Gauge (C,j))) and

           A16: (f /. i1) = (( Gauge (C,j)) * (i4,j4)) by A4, GOBOARD1:def 9;

          

           A17: 1 <= i4 by A15, MATRIX_0: 32;

          

           A18: j4 <= ( width ( Gauge (C,j))) by A15, MATRIX_0: 32;

          

           A19: 1 <= j4 by A15, MATRIX_0: 32;

          

           A20: i4 <= ( len ( Gauge (C,j))) by A15, MATRIX_0: 32;

          1 <= (i1 + 1) by NAT_1: 11;

          then

           A21: (i1 + 1) in ( dom f) by A9, FINSEQ_3: 25;

          then

          consider i5,j5 be Nat such that

           A22: [i5, j5] in ( Indices ( Gauge (C,j))) and

           A23: (f /. (i1 + 1)) = (( Gauge (C,j)) * (i5,j5)) by A4, GOBOARD1:def 9;

          

           A24: 1 <= i5 by A22, MATRIX_0: 32;

          ( right_cell (f,i1)) = ( right_cell (f,i1));

          then

           A25: i4 = i5 & (j4 + 1) = j5 & ( right_cell (f,i1)) = ( cell (( GoB f),i4,j4)) or (i4 + 1) = i5 & j4 = j5 & ( right_cell (f,i1)) = ( cell (( GoB f),i4,(j4 -' 1))) or i4 = (i5 + 1) & j4 = j5 & ( right_cell (f,i1)) = ( cell (( GoB f),i5,j5)) or i4 = i5 & j4 = (j5 + 1) & ( right_cell (f,i1)) = ( cell (( GoB f),(i4 -' 1),j5)) by A8, A9, A11, A15, A16, A22, A23, GOBOARD5:def 6;

          ( |.(i4 - i5).| + |.(j4 - j5).|) = 1 by A4, A14, A15, A16, A21, A22, A23, GOBOARD1:def 9;

          then

           A26: |.(i4 - i5).| = 1 & j4 = j5 or |.(j4 - j5).| = 1 & i4 = i5 by SEQM_3: 42;

          

           A27: j5 <= ( width ( Gauge (C,j))) by A22, MATRIX_0: 32;

          

           A28: i5 <= ( len ( Gauge (C,j))) by A22, MATRIX_0: 32;

          

           A29: 1 <= j5 by A22, MATRIX_0: 32;

          per cases by A26, SEQM_3: 41;

            suppose

             A30: i4 = i5 & (j4 + 1) = j5;

            then i4 < ( len ( Gauge (C,j))) by A1, A8, A9, A15, A16, A22, A23, JORDAN10: 1;

            then (i4 + 1) <= ( len ( Gauge (C,j))) by NAT_1: 13;

            hence thesis by A2, A11, A17, A19, A27, A25, A30, Th38;

          end;

            suppose

             A31: (i4 + 1) = i5 & j4 = j5;

            then 1 < j4 by A1, A8, A9, A15, A16, A22, A23, JORDAN10: 3;

            then (1 + 1) <= j4 by NAT_1: 13;

            then

             A32: 1 <= (j4 -' 1) by JORDAN5B: 2;

            ((j4 -' 1) + 1) = j4 by A19, XREAL_1: 235;

            hence thesis by A2, A11, A17, A18, A28, A25, A31, A32, Th38;

          end;

            suppose

             A33: i4 = (i5 + 1) & j4 = j5;

            then j5 < ( width ( Gauge (C,j))) by A1, A8, A9, A15, A16, A22, A23, JORDAN10: 4;

            then (j5 + 1) <= ( width ( Gauge (C,j))) by NAT_1: 13;

            hence thesis by A2, A11, A20, A24, A29, A25, A33, Th38;

          end;

            suppose

             A34: i4 = i5 & j4 = (j5 + 1);

            then 1 < i4 by A1, A8, A9, A15, A16, A22, A23, JORDAN10: 2;

            then (1 + 1) <= i4 by NAT_1: 13;

            then

             A35: 1 <= (i4 -' 1) by JORDAN5B: 2;

            ((i4 -' 1) + 1) = i4 by A17, XREAL_1: 235;

            hence thesis by A2, A11, A20, A18, A29, A25, A34, A35, Th38;

          end;

        end;

        then

        consider i2,j2 be Nat such that 1 <= i2 and

         A36: (i2 + 1) <= ( len ( Gauge (C,i))) and 1 <= j2 and

         A37: (j2 + 1) <= ( width ( Gauge (C,i))) and

         A38: ( right_cell (( Cage (C,j)),i1)) c= ( cell (( Gauge (C,i)),i2,j2));

        

         A39: ( Int ( right_cell (( Cage (C,j)),i1))) c= ( Int ( cell (( Gauge (C,i)),i2,j2))) by A38, TOPS_1: 19;

        

         A40: ( RightComp ( Cage (C,i))) is_a_component_of (( L~ ( Cage (C,i))) ` ) by GOBOARD9:def 2;

        

         A41: (( Cl ( LeftComp ( Cage (C,i)))) \/ ( RightComp ( Cage (C,i)))) = ((( L~ ( Cage (C,i))) \/ ( LeftComp ( Cage (C,i)))) \/ ( RightComp ( Cage (C,i)))) by GOBRD14: 22

        .= ((( L~ ( Cage (C,i))) \/ ( RightComp ( Cage (C,i)))) \/ ( LeftComp ( Cage (C,i)))) by XBOOLE_1: 4

        .= the carrier of ( TOP-REAL 2) by GOBRD14: 15;

        assume not ( right_cell (( Cage (C,j)),i1)) c= ( Cl ( LeftComp ( Cage (C,i))));

        then not ( cell (( Gauge (C,i)),i2,j2)) c= ( Cl ( LeftComp ( Cage (C,i)))) by A38;

        then

         A42: ( cell (( Gauge (C,i)),i2,j2)) meets ( RightComp ( Cage (C,i))) by A41, XBOOLE_1: 73;

        

         A43: i2 < ( len ( Gauge (C,i))) & j2 < ( width ( Gauge (C,i))) by A36, A37, NAT_1: 13;

        then ( cell (( Gauge (C,i)),i2,j2)) = ( Cl ( Int ( cell (( Gauge (C,i)),i2,j2)))) by GOBRD11: 35;

        then

         A44: ( Int ( cell (( Gauge (C,i)),i2,j2))) meets ( RightComp ( Cage (C,i))) by A42, TSEP_1: 36;

        

         A45: ( Int ( cell (( Gauge (C,i)),i2,j2))) is convex by A43, GOBOARD9: 17;

        ( Int ( cell (( Gauge (C,i)),i2,j2))) c= (( L~ ( Cage (C,i))) ` ) by A5, A43, GOBRD12: 1;

        then ( Int ( cell (( Gauge (C,i)),i2,j2))) c= ( RightComp ( Cage (C,i))) by A44, A40, A45, GOBOARD9: 4;

        then ( Int ( right_cell (( Cage (C,j)),i1))) c= ( RightComp ( Cage (C,i))) by A39;

        then ( Cl ( Int ( right_cell (( Cage (C,j)),i1)))) c= ( Cl ( RightComp ( Cage (C,i)))) by PRE_TOPC: 19;

        then

         A46: ( right_cell (( Cage (C,j)),i1)) c= ( Cl ( RightComp ( Cage (C,i)))) by A4, A8, A9, A12, JORDAN9: 11;

        ( LSeg (( Cage (C,j)),i1)) c= ( right_cell (( Cage (C,j)),i1,( Gauge (C,j)))) & ( right_cell (( Cage (C,j)),i1,( Gauge (C,j)))) c= ( right_cell (( Cage (C,j)),i1)) by A4, A8, A9, Th22, GOBRD13: 33;

        then ( LSeg (( Cage (C,j)),i1)) c= ( right_cell (( Cage (C,j)),i1));

        then ( LSeg (( Cage (C,j)),i1)) c= ( Cl ( RightComp ( Cage (C,i)))) by A46;

        hence contradiction by A7, A10;

      end;

      then

       A47: C meets ( Cl ( LeftComp ( Cage (C,i)))) by A1, A8, A9, A12, JORDAN9: 31, XBOOLE_1: 63;

      ( Cl ( LeftComp ( Cage (C,i)))) = (( LeftComp ( Cage (C,i))) \/ ( L~ ( Cage (C,i)))) & C misses ( L~ ( Cage (C,i))) by A1, GOBRD14: 22, JORDAN10: 5;

      then

       A48: C meets ( LeftComp ( Cage (C,i))) by A47, XBOOLE_1: 70;

      reconsider D = (( L~ ( Cage (C,i))) ` ) as Subset of ( TOP-REAL 2);

      D = (( LeftComp ( Cage (C,i))) \/ ( RightComp ( Cage (C,i)))) by GOBRD12: 10;

      then

       A49: ( RightComp ( Cage (C,i))) c= D by XBOOLE_1: 7;

      C c= ( RightComp ( Cage (C,i))) by A1, JORDAN10: 11;

      then

       A50: C c= D by A49;

      C meets C;

      then

       A51: C meets ( RightComp ( Cage (C,i))) by A1, JORDAN10: 11, XBOOLE_1: 63;

      ( LeftComp ( Cage (C,i))) is_a_component_of D & ( RightComp ( Cage (C,i))) is_a_component_of D by GOBOARD9:def 1, GOBOARD9:def 2;

      hence contradiction by A1, A48, A50, A51, JORDAN9: 1, SPRECT_4: 6;

    end;

    theorem :: JORDAN1H:47

    

     Th47: C is connected & i <= j implies ( LeftComp ( Cage (C,i))) c= ( LeftComp ( Cage (C,j)))

    proof

      assume that

       A1: C is connected and

       A2: i <= j;

      

       A3: (( Cage (C,j)) /. 1) = ( N-min ( L~ ( Cage (C,j)))) by A1, JORDAN9: 32;

      i < j or i = j by A2, XXREAL_0: 1;

      then

       A4: ( E-bound ( L~ ( Cage (C,i)))) > ( E-bound ( L~ ( Cage (C,j)))) or ( E-bound ( L~ ( Cage (C,i)))) = ( E-bound ( L~ ( Cage (C,j)))) by A1, JORDAN1A: 67;

      set p = |[(( E-bound ( L~ ( Cage (C,i)))) + 1), 0 ]|;

      

       A5: ( LeftComp ( Cage (C,i))) misses ( RightComp ( Cage (C,i))) by GOBRD14: 14;

      

       A6: (p `1 ) = (( E-bound ( L~ ( Cage (C,i)))) + 1) by EUCLID: 52;

      then (p `1 ) > ( E-bound ( L~ ( Cage (C,i)))) by XREAL_1: 29;

      then (p `1 ) > ( E-bound ( L~ ( Cage (C,j)))) by A4, XXREAL_0: 2;

      then

       A7: p in ( LeftComp ( Cage (C,j))) by A3, JORDAN2C: 111;

      (( Cage (C,i)) /. 1) = ( N-min ( L~ ( Cage (C,i)))) by A1, JORDAN9: 32;

      then p in ( LeftComp ( Cage (C,i))) by A6, JORDAN2C: 111, XREAL_1: 29;

      then

       A8: ( LeftComp ( Cage (C,i))) meets ( LeftComp ( Cage (C,j))) by A7, XBOOLE_0: 3;

      ( Cl ( RightComp ( Cage (C,i)))) = (( RightComp ( Cage (C,i))) \/ ( L~ ( Cage (C,i)))) & ( L~ ( Cage (C,i))) misses ( LeftComp ( Cage (C,i))) by GOBRD14: 21, SPRECT_3: 26;

      then ( Cl ( RightComp ( Cage (C,i)))) misses ( LeftComp ( Cage (C,i))) by A5, XBOOLE_1: 70;

      then ( L~ ( Cage (C,j))) misses ( LeftComp ( Cage (C,i))) by A1, A2, Th46, XBOOLE_1: 63;

      then ( LeftComp ( Cage (C,j))) is_a_component_of (( L~ ( Cage (C,j))) ` ) & ( LeftComp ( Cage (C,i))) c= (( L~ ( Cage (C,j))) ` ) by GOBOARD9:def 1, SUBSET_1: 23;

      hence thesis by A8, GOBOARD9: 4;

    end;

    theorem :: JORDAN1H:48

    C is connected & i <= j implies ( RightComp ( Cage (C,j))) c= ( RightComp ( Cage (C,i)))

    proof

      assume C is connected & i <= j;

      then

       A1: ( Cl ( LeftComp ( Cage (C,i)))) c= ( Cl ( LeftComp ( Cage (C,j)))) by Th47, PRE_TOPC: 19;

      (( Cl ( LeftComp ( Cage (C,i)))) ` ) = ( RightComp ( Cage (C,i))) & (( Cl ( LeftComp ( Cage (C,j)))) ` ) = ( RightComp ( Cage (C,j))) by Th42;

      hence thesis by A1, SUBSET_1: 12;

    end;

    begin

    definition

      let C, n;

      :: JORDAN1H:def2

      func X-SpanStart (C,n) -> Nat equals ((2 |^ (n -' 1)) + 2);

      correctness ;

    end

    theorem :: JORDAN1H:49

    

     Th49: 2 < ( X-SpanStart (C,n)) & ( X-SpanStart (C,n)) < ( len ( Gauge (C,n)))

    proof

      (2 |^ (n -' 1)) > 0 by NEWTON: 83;

      then ((2 |^ (n -' 1)) + 2) > ( 0 qua Nat + 2) by XREAL_1: 6;

      hence 2 < ( X-SpanStart (C,n));

      (n -' 1) <= n by NAT_D: 44;

      then ( len ( Gauge (C,n))) = ((2 |^ n) + 3) & (2 |^ (n -' 1)) <= (2 |^ n) by JORDAN8:def 1, PREPOWER: 93;

      hence thesis by XREAL_1: 8;

    end;

    theorem :: JORDAN1H:50

    

     Th50: 1 <= (( X-SpanStart (C,n)) -' 1) & (( X-SpanStart (C,n)) -' 1) < ( len ( Gauge (C,n)))

    proof

      2 < ( X-SpanStart (C,n)) by Th49;

      then

       A1: ((( X-SpanStart (C,n)) -' 1) + 1) = ( X-SpanStart (C,n)) by XREAL_1: 235, XXREAL_0: 2;

      1 < ( X-SpanStart (C,n)) by Th49, XXREAL_0: 2;

      hence 1 <= (( X-SpanStart (C,n)) -' 1) by A1, NAT_1: 13;

      ( X-SpanStart (C,n)) < ( len ( Gauge (C,n))) & (( X-SpanStart (C,n)) -' 1) <= ( X-SpanStart (C,n)) by Th49, NAT_D: 44;

      hence thesis by XXREAL_0: 2;

    end;

    definition

      let C, n;

      :: JORDAN1H:def3

      pred n is_sufficiently_large_for C means ex j st j < ( width ( Gauge (C,n))) & ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),j)) c= ( BDD C);

    end

    theorem :: JORDAN1H:51

    n is_sufficiently_large_for C implies n >= 1

    proof

      

       A1: (2 |^ 0 ) = 1 by NEWTON: 4;

      assume n is_sufficiently_large_for C;

      then

      consider j such that

       A2: j < ( width ( Gauge (C,n))) and

       A3: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),j)) c= ( BDD C);

      assume n < 1;

      then

       A4: n = 0 by NAT_1: 14;

      

       A5: j > 1

      proof

        

         A6: (( X-SpanStart (C,n)) -' 1) <= ( len ( Gauge (C,n))) by Th50;

        assume

         A7: j <= 1;

        per cases by A7, NAT_1: 25;

          suppose

           A8: j = 0 ;

           0 <= ( width ( Gauge (C,n)));

          then

           A9: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1), 0 )) is non empty by A6, JORDAN1A: 24;

          ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1), 0 )) c= ( UBD C) by A6, JORDAN1A: 49;

          hence contradiction by A3, A8, A9, JORDAN2C: 24, XBOOLE_1: 68;

        end;

          suppose

           A10: j = 1;

          set i1 = ( X-SpanStart (C,n));

          ( UBD C) is_outside_component_of C by JORDAN2C: 68;

          then

           A11: ( UBD C) is_a_component_of (C ` ) by JORDAN2C:def 3;

          i1 < ( len ( Gauge (C,n))) & (i1 -' 1) <= i1 by Th49, NAT_D: 44;

          then

           A12: (i1 -' 1) < ( len ( Gauge (C,n))) by XXREAL_0: 2;

          ( BDD C) c= (C ` ) by JORDAN2C: 25;

          then

           A13: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),1)) c= (C ` ) by A3, A10;

          

           A14: ( width ( Gauge (C,n))) <> 0 by MATRIX_0:def 10;

          then

           A15: ( 0 qua Nat + 1) <= ( width ( Gauge (C,n))) by NAT_1: 14;

          then

           A16: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),1)) is non empty by A6, JORDAN1A: 24;

          1 <= (i1 -' 1) by Th50;

          then (( cell (( Gauge (C,n)),(i1 -' 1), 0 )) /\ ( cell (( Gauge (C,n)),(i1 -' 1),( 0 qua Nat + 1)))) = ( LSeg ((( Gauge (C,n)) * ((i1 -' 1),( 0 qua Nat + 1))),(( Gauge (C,n)) * (((i1 -' 1) + 1),( 0 qua Nat + 1))))) by A14, A12, GOBOARD5: 26;

          then

           A17: ( cell (( Gauge (C,n)),(i1 -' 1), 0 )) meets ( cell (( Gauge (C,n)),(i1 -' 1),( 0 qua Nat + 1)));

          ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1), 0 )) c= ( UBD C) by A6, JORDAN1A: 49;

          then ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),1)) c= ( UBD C) by A15, A12, A17, A11, A13, GOBOARD9: 4, JORDAN1A: 25;

          hence contradiction by A3, A10, A16, JORDAN2C: 24, XBOOLE_1: 68;

        end;

      end;

      

       A18: ( width ( Gauge (C,n))) = ((2 |^ n) + 3) by JORDAN1A: 28;

      then

       A19: j <= (3 + 1) by A2, A4, NEWTON: 4;

      

       A20: (j + 1) < ( width ( Gauge (C,n)))

      proof

        assume (j + 1) >= ( width ( Gauge (C,n)));

        then

         A21: (j + 1) > ( width ( Gauge (C,n))) or (j + 1) = ( width ( Gauge (C,n))) by XXREAL_0: 1;

        

         A22: (( X-SpanStart (C,n)) -' 1) <= ( len ( Gauge (C,n))) by Th50;

        per cases by A2, A21, NAT_1: 13;

          suppose

           A23: j = ( width ( Gauge (C,n)));

          ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),( width ( Gauge (C,n))))) is non empty & ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),( width ( Gauge (C,n))))) c= ( UBD C) by A22, JORDAN1A: 24, JORDAN1A: 50;

          hence contradiction by A3, A23, JORDAN2C: 24, XBOOLE_1: 68;

        end;

          suppose (j + 1) = ( width ( Gauge (C,n)));

          then

           A24: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),(( width ( Gauge (C,n))) -' 1))) c= ( BDD C) by A3, NAT_D: 34;

          ( BDD C) c= (C ` ) by JORDAN2C: 25;

          then

           A25: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),(( width ( Gauge (C,n))) -' 1))) c= (C ` ) by A24;

          set i1 = ( X-SpanStart (C,n));

          

           A26: (( width ( Gauge (C,n))) - 1) < ( width ( Gauge (C,n))) by XREAL_1: 146;

          ( UBD C) is_outside_component_of C by JORDAN2C: 68;

          then

           A27: ( UBD C) is_a_component_of (C ` ) by JORDAN2C:def 3;

          (( width ( Gauge (C,n))) -' 1) <= ( width ( Gauge (C,n))) by NAT_D: 44;

          then

           A28: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),(( width ( Gauge (C,n))) -' 1))) is non empty by A22, JORDAN1A: 24;

          

           A29: ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),( width ( Gauge (C,n))))) c= ( UBD C) by A22, JORDAN1A: 50;

          

           A30: 1 <= (i1 -' 1) by Th50;

          i1 < ( len ( Gauge (C,n))) & (i1 -' 1) <= i1 by Th49, NAT_D: 44;

          then

           A31: (i1 -' 1) < ( len ( Gauge (C,n))) by XXREAL_0: 2;

          

           A32: ( width ( Gauge (C,n))) <> 0 by MATRIX_0:def 10;

          then ((( width ( Gauge (C,n))) -' 1) + 1) = ( width ( Gauge (C,n))) by NAT_1: 14, XREAL_1: 235;

          then (( cell (( Gauge (C,n)),(i1 -' 1),( width ( Gauge (C,n))))) /\ ( cell (( Gauge (C,n)),(i1 -' 1),(( width ( Gauge (C,n))) -' 1)))) = ( LSeg ((( Gauge (C,n)) * ((i1 -' 1),( width ( Gauge (C,n))))),(( Gauge (C,n)) * (((i1 -' 1) + 1),( width ( Gauge (C,n))))))) by A31, A26, A30, GOBOARD5: 26;

          then

           A33: ( cell (( Gauge (C,n)),(i1 -' 1),( width ( Gauge (C,n))))) meets ( cell (( Gauge (C,n)),(i1 -' 1),(( width ( Gauge (C,n))) -' 1)));

          (( width ( Gauge (C,n))) -' 1) < ( width ( Gauge (C,n))) by A32, A26, NAT_1: 14, XREAL_1: 233;

          then ( cell (( Gauge (C,n)),(( X-SpanStart (C,n)) -' 1),(( width ( Gauge (C,n))) -' 1))) c= ( UBD C) by A29, A31, A33, A27, A25, GOBOARD9: 4, JORDAN1A: 25;

          hence contradiction by A24, A28, JORDAN2C: 24, XBOOLE_1: 68;

        end;

      end;

      j = 0 or ... or j = 4 by A19;

      per cases ;

        suppose j = 0 or j = 1;

        hence thesis by A5;

      end;

        suppose

         A34: j = 2;

        

         A35: ( X-SpanStart (C, 0 )) = (1 + 2) by A1, NAT_2: 8;

        

        then (( X-SpanStart (C, 0 )) -' 1) = (( X-SpanStart (C, 0 )) - 1) by NAT_D: 39

        .= 2 by A35;

        hence contradiction by A3, A4, A34, JORDAN1B: 18;

      end;

        suppose j = 3 or j = 4;

        hence thesis by A18, A20, A1, A4;

      end;

    end;

    theorem :: JORDAN1H:52

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on ( Gauge (C,n)) & ( len f) > 1 holds for i1,j1 be Nat st ( left_cell (f,(( len f) -' 1),( Gauge (C,n)))) meets C & [i1, j1] in ( Indices ( Gauge (C,n))) & (f /. (( len f) -' 1)) = (( Gauge (C,n)) * (i1,j1)) & [i1, (j1 + 1)] in ( Indices ( Gauge (C,n))) & (f /. ( len f)) = (( Gauge (C,n)) * (i1,(j1 + 1))) holds [(i1 -' 1), (j1 + 1)] in ( Indices ( Gauge (C,n)))

    proof

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

      let n;

      set G = ( Gauge (C,n));

      let f be FinSequence of ( TOP-REAL 2) such that

       A1: f is_sequence_on G and

       A2: ( len f) > 1;

      

       A3: 1 <= (( len f) -' 1) & ((( len f) -' 1) + 1) = ( len f) by A2, NAT_D: 49, XREAL_1: 235;

      let i1,j1 be Nat such that

       A4: ( left_cell (f,(( len f) -' 1),G)) meets C and

       A5: [i1, j1] in ( Indices G) and

       A6: (f /. (( len f) -' 1)) = (G * (i1,j1)) and

       A7: [i1, (j1 + 1)] in ( Indices G) and

       A8: (f /. ( len f)) = (G * (i1,(j1 + 1)));

      

       A9: 1 <= i1 by A7, MATRIX_0: 32;

      

       A10: ( len G) = ( width G) & j1 <= ( width G) by A5, JORDAN8:def 1, MATRIX_0: 32;

       A11:

      now

        assume (i1 -' 1) < 1;

        then i1 <= 1 by NAT_1: 14, NAT_D: 36;

        then i1 = 1 by A9, XXREAL_0: 1;

        then ( cell (G,(1 -' 1),j1)) meets C by A1, A4, A5, A6, A7, A8, A3, GOBRD13: 21;

        then ( cell (G, 0 ,j1)) meets C by XREAL_1: 232;

        hence contradiction by A10, JORDAN8: 18;

      end;

      

       A12: (i1 -' 1) <= i1 by NAT_D: 35;

      i1 <= ( len G) by A5, MATRIX_0: 32;

      then

       A13: (i1 -' 1) <= ( len G) by A12, XXREAL_0: 2;

      1 <= (j1 + 1) & (j1 + 1) <= ( width G) by A7, MATRIX_0: 32;

      hence thesis by A13, A11, MATRIX_0: 30;

    end;

    theorem :: JORDAN1H:53

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on ( Gauge (C,n)) & ( len f) > 1 holds for i1,j1 be Nat st ( left_cell (f,(( len f) -' 1),( Gauge (C,n)))) meets C & [i1, j1] in ( Indices ( Gauge (C,n))) & (f /. (( len f) -' 1)) = (( Gauge (C,n)) * (i1,j1)) & [(i1 + 1), j1] in ( Indices ( Gauge (C,n))) & (f /. ( len f)) = (( Gauge (C,n)) * ((i1 + 1),j1)) holds [(i1 + 1), (j1 + 1)] in ( Indices ( Gauge (C,n)))

    proof

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

      let n;

      set G = ( Gauge (C,n));

      let f be FinSequence of ( TOP-REAL 2) such that

       A1: f is_sequence_on G and

       A2: ( len f) > 1;

      

       A3: 1 <= (( len f) -' 1) & ((( len f) -' 1) + 1) = ( len f) by A2, NAT_D: 49, XREAL_1: 235;

      

       A4: ( len G) = ( width G) by JORDAN8:def 1;

      let i1,j1 be Nat such that

       A5: ( left_cell (f,(( len f) -' 1),G)) meets C and

       A6: [i1, j1] in ( Indices G) and

       A7: (f /. (( len f) -' 1)) = (G * (i1,j1)) and

       A8: [(i1 + 1), j1] in ( Indices G) and

       A9: (f /. ( len f)) = (G * ((i1 + 1),j1));

      

       A10: j1 <= ( width G) by A8, MATRIX_0: 32;

      

       A11: i1 <= ( len G) by A6, MATRIX_0: 32;

       A12:

      now

        assume (j1 + 1) > ( len G);

        then

         A13: (( len G) + 1) <= (j1 + 1) by NAT_1: 13;

        (j1 + 1) <= (( len G) + 1) by A4, A10, XREAL_1: 6;

        then (j1 + 1) = (( len G) + 1) by A13, XXREAL_0: 1;

        then ( cell (G,i1,( len G))) meets C by A1, A5, A6, A7, A8, A9, A3, GOBRD13: 23;

        hence contradiction by A11, JORDAN8: 15;

      end;

      

       A14: 1 <= (j1 + 1) by NAT_1: 11;

      1 <= (i1 + 1) & (i1 + 1) <= ( len G) by A8, MATRIX_0: 32;

      hence thesis by A4, A14, A12, MATRIX_0: 30;

    end;

    theorem :: JORDAN1H:54

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on ( Gauge (C,n)) & ( len f) > 1 holds for j1,i2 be Nat st ( left_cell (f,(( len f) -' 1),( Gauge (C,n)))) meets C & [(i2 + 1), j1] in ( Indices ( Gauge (C,n))) & (f /. (( len f) -' 1)) = (( Gauge (C,n)) * ((i2 + 1),j1)) & [i2, j1] in ( Indices ( Gauge (C,n))) & (f /. ( len f)) = (( Gauge (C,n)) * (i2,j1)) holds [i2, (j1 -' 1)] in ( Indices ( Gauge (C,n)))

    proof

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

      let n;

      set G = ( Gauge (C,n));

      let f be FinSequence of ( TOP-REAL 2) such that

       A1: f is_sequence_on G and

       A2: ( len f) > 1;

      

       A3: 1 <= (( len f) -' 1) & ((( len f) -' 1) + 1) = ( len f) by A2, NAT_D: 49, XREAL_1: 235;

      let j1,i2 be Nat such that

       A4: ( left_cell (f,(( len f) -' 1),G)) meets C & [(i2 + 1), j1] in ( Indices G) & (f /. (( len f) -' 1)) = (G * ((i2 + 1),j1)) and

       A5: [i2, j1] in ( Indices G) and

       A6: (f /. ( len f)) = (G * (i2,j1));

      

       A7: i2 <= ( len G) by A5, MATRIX_0: 32;

      

       A8: 1 <= j1 by A5, MATRIX_0: 32;

       A9:

      now

        assume (j1 -' 1) < 1;

        then j1 <= 1 by NAT_1: 14, NAT_D: 36;

        then j1 = 1 by A8, XXREAL_0: 1;

        then ( cell (G,i2,(1 -' 1))) meets C by A1, A4, A5, A6, A3, GOBRD13: 25;

        then ( cell (G,i2, 0 )) meets C by XREAL_1: 232;

        hence contradiction by A7, JORDAN8: 17;

      end;

      

       A10: (j1 -' 1) <= j1 by NAT_D: 35;

      j1 <= ( width G) by A5, MATRIX_0: 32;

      then

       A11: (j1 -' 1) <= ( width G) by A10, XXREAL_0: 2;

      1 <= i2 by A5, MATRIX_0: 32;

      hence thesis by A7, A11, A9, MATRIX_0: 30;

    end;

    theorem :: JORDAN1H:55

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on ( Gauge (C,n)) & ( len f) > 1 holds for i1,j2 be Nat st ( left_cell (f,(( len f) -' 1),( Gauge (C,n)))) meets C & [i1, (j2 + 1)] in ( Indices ( Gauge (C,n))) & (f /. (( len f) -' 1)) = (( Gauge (C,n)) * (i1,(j2 + 1))) & [i1, j2] in ( Indices ( Gauge (C,n))) & (f /. ( len f)) = (( Gauge (C,n)) * (i1,j2)) holds [(i1 + 1), j2] in ( Indices ( Gauge (C,n)))

    proof

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

      let n;

      set G = ( Gauge (C,n));

      

       A1: ( len G) = ( width G) by JORDAN8:def 1;

      let f be FinSequence of ( TOP-REAL 2) such that

       A2: f is_sequence_on G and

       A3: ( len f) > 1;

      

       A4: 1 <= (( len f) -' 1) & ((( len f) -' 1) + 1) = ( len f) by A3, NAT_D: 49, XREAL_1: 235;

      let i1,j2 be Nat such that

       A5: ( left_cell (f,(( len f) -' 1),G)) meets C & [i1, (j2 + 1)] in ( Indices G) & (f /. (( len f) -' 1)) = (G * (i1,(j2 + 1))) and

       A6: [i1, j2] in ( Indices G) and

       A7: (f /. ( len f)) = (G * (i1,j2));

      

       A8: j2 <= ( width G) by A6, MATRIX_0: 32;

      

       A9: i1 <= ( len G) by A6, MATRIX_0: 32;

       A10:

      now

        assume (i1 + 1) > ( len G);

        then

         A11: (( len G) + 1) <= (i1 + 1) by NAT_1: 13;

        (i1 + 1) <= (( len G) + 1) by A9, XREAL_1: 6;

        then (i1 + 1) = (( len G) + 1) by A11, XXREAL_0: 1;

        then ( cell (G,( len G),j2)) meets C by A2, A5, A6, A7, A4, GOBRD13: 27;

        hence contradiction by A1, A8, JORDAN8: 16;

      end;

      

       A12: 1 <= (i1 + 1) by NAT_1: 11;

      1 <= j2 by A6, MATRIX_0: 32;

      hence thesis by A8, A12, A10, MATRIX_0: 30;

    end;

    theorem :: JORDAN1H:56

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on ( Gauge (C,n)) & ( len f) > 1 holds for i1,j1 be Nat st ( front_left_cell (f,(( len f) -' 1),( Gauge (C,n)))) meets C & [i1, j1] in ( Indices ( Gauge (C,n))) & (f /. (( len f) -' 1)) = (( Gauge (C,n)) * (i1,j1)) & [i1, (j1 + 1)] in ( Indices ( Gauge (C,n))) & (f /. ( len f)) = (( Gauge (C,n)) * (i1,(j1 + 1))) holds [i1, (j1 + 2)] in ( Indices ( Gauge (C,n)))

    proof

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

      let n;

      set G = ( Gauge (C,n));

      

       A1: ( len G) = ( width G) by JORDAN8:def 1;

      let f be FinSequence of ( TOP-REAL 2) such that

       A2: f is_sequence_on G and

       A3: ( len f) > 1;

      

       A4: 1 <= (( len f) -' 1) & ((( len f) -' 1) + 1) = ( len f) by A3, NAT_D: 49, XREAL_1: 235;

      let i1,j1 be Nat such that

       A5: ( front_left_cell (f,(( len f) -' 1),G)) meets C & [i1, j1] in ( Indices G) & (f /. (( len f) -' 1)) = (G * (i1,j1)) and

       A6: [i1, (j1 + 1)] in ( Indices G) and

       A7: (f /. ( len f)) = (G * (i1,(j1 + 1)));

      

       A8: i1 <= ( len G) by A6, MATRIX_0: 32;

      

       A9: (i1 -' 1) <= i1 by NAT_D: 35;

      

       A10: (j1 + 1) <= ( width G) by A6, MATRIX_0: 32;

       A11:

      now

        assume ((j1 + 1) + 1) > ( len G);

        then

         A12: (( len G) + 1) <= ((j1 + 1) + 1) by NAT_1: 13;

        ((j1 + 1) + 1) <= (( len G) + 1) by A1, A10, XREAL_1: 6;

        then ((j1 + 1) + 1) = (( len G) + 1) by A12, XXREAL_0: 1;

        then ( cell (G,(i1 -' 1),( len G))) meets C by A2, A5, A6, A7, A4, GOBRD13: 34;

        hence contradiction by A8, A9, JORDAN8: 15, XXREAL_0: 2;

      end;

      

       A13: 1 <= ((j1 + 1) + 1) by NAT_1: 12;

      1 <= i1 by A6, MATRIX_0: 32;

      hence thesis by A1, A8, A13, A11, MATRIX_0: 30;

    end;

    theorem :: JORDAN1H:57

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on ( Gauge (C,n)) & ( len f) > 1 holds for i1,j1 be Nat st ( front_left_cell (f,(( len f) -' 1),( Gauge (C,n)))) meets C & [i1, j1] in ( Indices ( Gauge (C,n))) & (f /. (( len f) -' 1)) = (( Gauge (C,n)) * (i1,j1)) & [(i1 + 1), j1] in ( Indices ( Gauge (C,n))) & (f /. ( len f)) = (( Gauge (C,n)) * ((i1 + 1),j1)) holds [(i1 + 2), j1] in ( Indices ( Gauge (C,n)))

    proof

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

      let n;

      set G = ( Gauge (C,n));

      

       A1: ( len G) = ( width G) by JORDAN8:def 1;

      let f be FinSequence of ( TOP-REAL 2) such that

       A2: f is_sequence_on G and

       A3: ( len f) > 1;

      

       A4: 1 <= (( len f) -' 1) & ((( len f) -' 1) + 1) = ( len f) by A3, NAT_D: 49, XREAL_1: 235;

      let i1,j1 be Nat such that

       A5: ( front_left_cell (f,(( len f) -' 1),G)) meets C & [i1, j1] in ( Indices G) & (f /. (( len f) -' 1)) = (G * (i1,j1)) and

       A6: [(i1 + 1), j1] in ( Indices G) and

       A7: (f /. ( len f)) = (G * ((i1 + 1),j1));

      

       A8: j1 <= ( width G) by A6, MATRIX_0: 32;

      

       A9: (i1 + 1) <= ( len G) by A6, MATRIX_0: 32;

       A10:

      now

        assume ((i1 + 1) + 1) > ( len G);

        then

         A11: (( len G) + 1) <= ((i1 + 1) + 1) by NAT_1: 13;

        ((i1 + 1) + 1) <= (( len G) + 1) by A9, XREAL_1: 6;

        then ((i1 + 1) + 1) = (( len G) + 1) by A11, XXREAL_0: 1;

        then ( cell (G,( len G),j1)) meets C by A2, A5, A6, A7, A4, GOBRD13: 36;

        hence contradiction by A1, A8, JORDAN8: 16;

      end;

      

       A12: 1 <= ((i1 + 1) + 1) by NAT_1: 12;

      1 <= j1 by A6, MATRIX_0: 32;

      hence thesis by A8, A12, A10, MATRIX_0: 30;

    end;

    theorem :: JORDAN1H:58

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on ( Gauge (C,n)) & ( len f) > 1 holds for j1,i2 be Nat st ( front_left_cell (f,(( len f) -' 1),( Gauge (C,n)))) meets C & [(i2 + 1), j1] in ( Indices ( Gauge (C,n))) & (f /. (( len f) -' 1)) = (( Gauge (C,n)) * ((i2 + 1),j1)) & [i2, j1] in ( Indices ( Gauge (C,n))) & (f /. ( len f)) = (( Gauge (C,n)) * (i2,j1)) holds [(i2 -' 1), j1] in ( Indices ( Gauge (C,n)))

    proof

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

      let n;

      set G = ( Gauge (C,n));

      

       A1: ( len G) = ( width G) by JORDAN8:def 1;

      let f be FinSequence of ( TOP-REAL 2) such that

       A2: f is_sequence_on G and

       A3: ( len f) > 1;

      

       A4: 1 <= (( len f) -' 1) & ((( len f) -' 1) + 1) = ( len f) by A3, NAT_D: 49, XREAL_1: 235;

      let j1,i2 be Nat such that

       A5: ( front_left_cell (f,(( len f) -' 1),G)) meets C & [(i2 + 1), j1] in ( Indices G) & (f /. (( len f) -' 1)) = (G * ((i2 + 1),j1)) and

       A6: [i2, j1] in ( Indices G) and

       A7: (f /. ( len f)) = (G * (i2,j1));

      

       A8: j1 <= ( width G) by A6, MATRIX_0: 32;

      

       A9: 1 <= i2 by A6, MATRIX_0: 32;

       A10:

      now

        assume (i2 -' 1) < 1;

        then i2 <= 1 by NAT_1: 14, NAT_D: 36;

        then i2 = 1 by A9, XXREAL_0: 1;

        then ( cell (G,(1 -' 1),(j1 -' 1))) meets C by A2, A5, A6, A7, A4, GOBRD13: 38;

        then ( cell (G, 0 ,(j1 -' 1))) meets C by XREAL_1: 232;

        hence contradiction by A1, A8, JORDAN8: 18, NAT_D: 44;

      end;

      i2 <= ( len G) by A6, MATRIX_0: 32;

      then

       A11: (i2 -' 1) <= ( len G) by NAT_D: 44;

      1 <= j1 by A6, MATRIX_0: 32;

      hence thesis by A8, A11, A10, MATRIX_0: 30;

    end;

    theorem :: JORDAN1H:59

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on ( Gauge (C,n)) & ( len f) > 1 holds for i1,j2 be Nat st ( front_left_cell (f,(( len f) -' 1),( Gauge (C,n)))) meets C & [i1, (j2 + 1)] in ( Indices ( Gauge (C,n))) & (f /. (( len f) -' 1)) = (( Gauge (C,n)) * (i1,(j2 + 1))) & [i1, j2] in ( Indices ( Gauge (C,n))) & (f /. ( len f)) = (( Gauge (C,n)) * (i1,j2)) holds [i1, (j2 -' 1)] in ( Indices ( Gauge (C,n)))

    proof

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

      let n;

      set G = ( Gauge (C,n));

      let f be FinSequence of ( TOP-REAL 2) such that

       A1: f is_sequence_on G and

       A2: ( len f) > 1;

      

       A3: 1 <= (( len f) -' 1) & ((( len f) -' 1) + 1) = ( len f) by A2, NAT_D: 49, XREAL_1: 235;

      let i1,j2 be Nat such that

       A4: ( front_left_cell (f,(( len f) -' 1),G)) meets C and

       A5: [i1, (j2 + 1)] in ( Indices G) and

       A6: (f /. (( len f) -' 1)) = (G * (i1,(j2 + 1))) and

       A7: [i1, j2] in ( Indices G) and

       A8: (f /. ( len f)) = (G * (i1,j2));

      

       A9: 1 <= j2 by A7, MATRIX_0: 32;

      

       A10: i1 <= ( len G) by A5, MATRIX_0: 32;

       A11:

      now

        assume (j2 -' 1) < 1;

        then j2 <= 1 by NAT_1: 14, NAT_D: 36;

        then j2 = 1 by A9, XXREAL_0: 1;

        then ( cell (G,i1,(1 -' 1))) meets C by A1, A4, A5, A6, A7, A8, A3, GOBRD13: 40;

        then ( cell (G,i1, 0 )) meets C by XREAL_1: 232;

        hence contradiction by A10, JORDAN8: 17;

      end;

      j2 <= ( width G) by A7, MATRIX_0: 32;

      then

       A12: (j2 -' 1) <= ( width G) by NAT_D: 44;

      1 <= i1 & i1 <= ( len G) by A7, MATRIX_0: 32;

      hence thesis by A12, A11, MATRIX_0: 30;

    end;

    theorem :: JORDAN1H:60

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on ( Gauge (C,n)) & ( len f) > 1 holds for i1,j1 be Nat st ( front_right_cell (f,(( len f) -' 1),( Gauge (C,n)))) meets C & [i1, j1] in ( Indices ( Gauge (C,n))) & (f /. (( len f) -' 1)) = (( Gauge (C,n)) * (i1,j1)) & [i1, (j1 + 1)] in ( Indices ( Gauge (C,n))) & (f /. ( len f)) = (( Gauge (C,n)) * (i1,(j1 + 1))) holds [(i1 + 1), (j1 + 1)] in ( Indices ( Gauge (C,n)))

    proof

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

      let n;

      set G = ( Gauge (C,n));

      

       A1: ( len G) = ( width G) by JORDAN8:def 1;

      let f be FinSequence of ( TOP-REAL 2) such that

       A2: f is_sequence_on G and

       A3: ( len f) > 1;

      

       A4: 1 <= (( len f) -' 1) & ((( len f) -' 1) + 1) = ( len f) by A3, NAT_D: 49, XREAL_1: 235;

      let i1,j1 be Nat such that

       A5: ( front_right_cell (f,(( len f) -' 1),G)) meets C & [i1, j1] in ( Indices G) & (f /. (( len f) -' 1)) = (G * (i1,j1)) and

       A6: [i1, (j1 + 1)] in ( Indices G) and

       A7: (f /. ( len f)) = (G * (i1,(j1 + 1)));

      

       A8: (j1 + 1) <= ( width G) by A6, MATRIX_0: 32;

      

       A9: i1 <= ( len G) by A6, MATRIX_0: 32;

       A10:

      now

        assume (i1 + 1) > ( len G);

        then

         A11: (( len G) + 1) <= (i1 + 1) by NAT_1: 13;

        (i1 + 1) <= (( len G) + 1) by A9, XREAL_1: 6;

        then (i1 + 1) = (( len G) + 1) by A11, XXREAL_0: 1;

        then ( cell (G,( len G),(j1 + 1))) meets C by A2, A5, A6, A7, A4, GOBRD13: 35;

        hence contradiction by A1, A8, JORDAN8: 16;

      end;

      

       A12: 1 <= (i1 + 1) by NAT_1: 11;

      1 <= (j1 + 1) by A6, MATRIX_0: 32;

      hence thesis by A8, A12, A10, MATRIX_0: 30;

    end;

    theorem :: JORDAN1H:61

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on ( Gauge (C,n)) & ( len f) > 1 holds for i1,j1 be Nat st ( front_right_cell (f,(( len f) -' 1),( Gauge (C,n)))) meets C & [i1, j1] in ( Indices ( Gauge (C,n))) & (f /. (( len f) -' 1)) = (( Gauge (C,n)) * (i1,j1)) & [(i1 + 1), j1] in ( Indices ( Gauge (C,n))) & (f /. ( len f)) = (( Gauge (C,n)) * ((i1 + 1),j1)) holds [(i1 + 1), (j1 -' 1)] in ( Indices ( Gauge (C,n)))

    proof

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

      let n;

      set G = ( Gauge (C,n));

      let f be FinSequence of ( TOP-REAL 2) such that

       A1: f is_sequence_on G and

       A2: ( len f) > 1;

      

       A3: 1 <= (( len f) -' 1) & ((( len f) -' 1) + 1) = ( len f) by A2, NAT_D: 49, XREAL_1: 235;

      let i1,j1 be Nat such that

       A4: ( front_right_cell (f,(( len f) -' 1),G)) meets C & [i1, j1] in ( Indices G) & (f /. (( len f) -' 1)) = (G * (i1,j1)) and

       A5: [(i1 + 1), j1] in ( Indices G) and

       A6: (f /. ( len f)) = (G * ((i1 + 1),j1));

      

       A7: (i1 + 1) <= ( len G) by A5, MATRIX_0: 32;

      

       A8: 1 <= j1 by A5, MATRIX_0: 32;

       A9:

      now

        assume (j1 -' 1) < 1;

        then j1 <= 1 by NAT_1: 14, NAT_D: 36;

        then j1 = 1 by A8, XXREAL_0: 1;

        then ( cell (G,(i1 + 1),(1 -' 1))) meets C by A1, A4, A5, A6, A3, GOBRD13: 37;

        then ( cell (G,(i1 + 1), 0 )) meets C by XREAL_1: 232;

        hence contradiction by A7, JORDAN8: 17;

      end;

      

       A10: (j1 -' 1) <= j1 by NAT_D: 35;

      j1 <= ( width G) by A5, MATRIX_0: 32;

      then

       A11: (j1 -' 1) <= ( width G) by A10, XXREAL_0: 2;

      1 <= (i1 + 1) by A5, MATRIX_0: 32;

      hence thesis by A7, A11, A9, MATRIX_0: 30;

    end;

    theorem :: JORDAN1H:62

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on ( Gauge (C,n)) & ( len f) > 1 holds for j1,i2 be Nat st ( front_right_cell (f,(( len f) -' 1),( Gauge (C,n)))) meets C & [(i2 + 1), j1] in ( Indices ( Gauge (C,n))) & (f /. (( len f) -' 1)) = (( Gauge (C,n)) * ((i2 + 1),j1)) & [i2, j1] in ( Indices ( Gauge (C,n))) & (f /. ( len f)) = (( Gauge (C,n)) * (i2,j1)) holds [i2, (j1 + 1)] in ( Indices ( Gauge (C,n)))

    proof

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

      let n;

      set G = ( Gauge (C,n));

      let f be FinSequence of ( TOP-REAL 2) such that

       A1: f is_sequence_on G and

       A2: ( len f) > 1;

      

       A3: 1 <= (( len f) -' 1) & ((( len f) -' 1) + 1) = ( len f) by A2, NAT_D: 49, XREAL_1: 235;

      

       A4: ( len G) = ( width G) by JORDAN8:def 1;

      let j1,i2 be Nat such that

       A5: ( front_right_cell (f,(( len f) -' 1),G)) meets C & [(i2 + 1), j1] in ( Indices G) & (f /. (( len f) -' 1)) = (G * ((i2 + 1),j1)) and

       A6: [i2, j1] in ( Indices G) and

       A7: (f /. ( len f)) = (G * (i2,j1));

      

       A8: i2 <= ( len G) by A6, MATRIX_0: 32;

      

       A9: j1 <= ( width G) by A6, MATRIX_0: 32;

       A10:

      now

        assume (j1 + 1) > ( len G);

        then

         A11: (( len G) + 1) <= (j1 + 1) by NAT_1: 13;

        (j1 + 1) <= (( len G) + 1) by A9, A4, XREAL_1: 6;

        then (j1 + 1) = (( len G) + 1) by A11, XXREAL_0: 1;

        then ( cell (G,(i2 -' 1),( len G))) meets C by A1, A5, A6, A7, A3, GOBRD13: 39;

        hence contradiction by A8, JORDAN8: 15, NAT_D: 44;

      end;

      

       A12: 1 <= (j1 + 1) by NAT_1: 11;

      1 <= i2 by A6, MATRIX_0: 32;

      hence thesis by A8, A12, A4, A10, MATRIX_0: 30;

    end;

    theorem :: JORDAN1H:63

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on ( Gauge (C,n)) & ( len f) > 1 holds for i1,j2 be Nat st ( front_right_cell (f,(( len f) -' 1),( Gauge (C,n)))) meets C & [i1, (j2 + 1)] in ( Indices ( Gauge (C,n))) & (f /. (( len f) -' 1)) = (( Gauge (C,n)) * (i1,(j2 + 1))) & [i1, j2] in ( Indices ( Gauge (C,n))) & (f /. ( len f)) = (( Gauge (C,n)) * (i1,j2)) holds [(i1 -' 1), j2] in ( Indices ( Gauge (C,n)))

    proof

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

      let n;

      set G = ( Gauge (C,n));

      

       A1: ( len G) = ( width G) by JORDAN8:def 1;

      let f be FinSequence of ( TOP-REAL 2) such that

       A2: f is_sequence_on G and

       A3: ( len f) > 1;

      

       A4: 1 <= (( len f) -' 1) & ((( len f) -' 1) + 1) = ( len f) by A3, NAT_D: 49, XREAL_1: 235;

      let i1,j2 be Nat such that

       A5: ( front_right_cell (f,(( len f) -' 1),G)) meets C & [i1, (j2 + 1)] in ( Indices G) & (f /. (( len f) -' 1)) = (G * (i1,(j2 + 1))) and

       A6: [i1, j2] in ( Indices G) and

       A7: (f /. ( len f)) = (G * (i1,j2));

      

       A8: j2 <= ( width G) by A6, MATRIX_0: 32;

      

       A9: 1 <= i1 by A6, MATRIX_0: 32;

       A10:

      now

        assume (i1 -' 1) < 1;

        then i1 <= 1 by NAT_1: 14, NAT_D: 36;

        then i1 = 1 by A9, XXREAL_0: 1;

        then ( cell (G,(1 -' 1),(j2 -' 1))) meets C by A2, A5, A6, A7, A4, GOBRD13: 41;

        then ( cell (G, 0 ,(j2 -' 1))) meets C by XREAL_1: 232;

        hence contradiction by A1, A8, JORDAN8: 18, NAT_D: 44;

      end;

      i1 <= ( len G) by A6, MATRIX_0: 32;

      then

       A11: (i1 -' 1) <= ( len G) by NAT_D: 44;

      1 <= j2 by A6, MATRIX_0: 32;

      hence thesis by A8, A11, A10, MATRIX_0: 30;

    end;