jordan1a.miz



    begin

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

D for non empty Subset of ( TOP-REAL 2),

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

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

G for Go-board,

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

r,s for Real;

    3 = ((2 * 1) + 1);

    then

     Lm1: (3 div 2) = 1 by NAT_D:def 1;

    1 = ((2 * 0 ) + 1);

    then

     Lm2: (1 div 2) = 0 by NAT_D:def 1;

    definition

      let f be FinSequence;

      :: JORDAN1A:def1

      func Center f -> Nat equals ((( len f) div 2) + 1);

      coherence ;

    end

    theorem :: JORDAN1A:1

    for f be FinSequence st ( len f) is odd holds ( len f) = ((2 * ( Center f)) - 1)

    proof

      let f be FinSequence;

      assume ( len f) is odd;

      then

      consider k be Nat such that

       A1: ( len f) = ((2 * k) + 1) by ABIAN: 9;

      

       A2: ((2 * k) mod 2) = 0 by NAT_D: 13;

      

      thus ( len f) = ((2 * (((2 * k) div 2) + (1 div 2))) + 1) by A1, Lm2, NAT_D: 18

      .= ((2 * (( len f) div 2)) + ((2 * 1) - 1)) by A1, A2, NAT_D: 19

      .= ((2 * ( Center f)) - 1);

    end;

    theorem :: JORDAN1A:2

    for f be FinSequence st ( len f) is even holds ( len f) = ((2 * ( Center f)) - 2)

    proof

      let f be FinSequence;

      assume ex k be Nat st ( len f) = (2 * k);

      

      hence ( len f) = (((2 * (( len f) div 2)) + (2 * 1)) - 2) by NAT_D: 18

      .= ((2 * ( Center f)) - 2);

    end;

    begin

    registration

      cluster compact non vertical non horizontal being_simple_closed_curve non empty for Subset of ( TOP-REAL 2);

      existence

      proof

        set f = the non constant standard special_circular_sequence;

        take ( L~ f);

        thus thesis;

      end;

    end

    theorem :: JORDAN1A:3

    

     Th3: p in ( N-most D) implies (p `2 ) = ( N-bound D)

    proof

      assume p in ( N-most D);

      then

       A1: p in ( LSeg (( NW-corner D),( NE-corner D))) by XBOOLE_0:def 4;

      (( NE-corner D) `2 ) = ( N-bound D) by EUCLID: 52

      .= (( NW-corner D) `2 ) by EUCLID: 52;

      

      hence (p `2 ) = (( NW-corner D) `2 ) by A1, GOBOARD7: 6

      .= ( N-bound D) by EUCLID: 52;

    end;

    theorem :: JORDAN1A:4

    

     Th4: p in ( E-most D) implies (p `1 ) = ( E-bound D)

    proof

      assume p in ( E-most D);

      then

       A1: p in ( LSeg (( SE-corner D),( NE-corner D))) by XBOOLE_0:def 4;

      (( SE-corner D) `1 ) = ( E-bound D) by EUCLID: 52

      .= (( NE-corner D) `1 ) by EUCLID: 52;

      

      hence (p `1 ) = (( SE-corner D) `1 ) by A1, GOBOARD7: 5

      .= ( E-bound D) by EUCLID: 52;

    end;

    theorem :: JORDAN1A:5

    

     Th5: p in ( S-most D) implies (p `2 ) = ( S-bound D)

    proof

      assume p in ( S-most D);

      then

       A1: p in ( LSeg (( SW-corner D),( SE-corner D))) by XBOOLE_0:def 4;

      (( SE-corner D) `2 ) = ( S-bound D) by EUCLID: 52

      .= (( SW-corner D) `2 ) by EUCLID: 52;

      

      hence (p `2 ) = (( SW-corner D) `2 ) by A1, GOBOARD7: 6

      .= ( S-bound D) by EUCLID: 52;

    end;

    theorem :: JORDAN1A:6

    

     Th6: p in ( W-most D) implies (p `1 ) = ( W-bound D)

    proof

      assume p in ( W-most D);

      then

       A1: p in ( LSeg (( SW-corner D),( NW-corner D))) by XBOOLE_0:def 4;

      (( SW-corner D) `1 ) = ( W-bound D) by EUCLID: 52

      .= (( NW-corner D) `1 ) by EUCLID: 52;

      

      hence (p `1 ) = (( SW-corner D) `1 ) by A1, GOBOARD7: 5

      .= ( W-bound D) by EUCLID: 52;

    end;

    theorem :: JORDAN1A:7

    for D be Subset of ( TOP-REAL 2) holds ( BDD D) misses D

    proof

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

      D misses (D ` ) by SUBSET_1: 24;

      hence thesis by JORDAN2C: 25, XBOOLE_1: 63;

    end;

    theorem :: JORDAN1A:8

    

     Th8: p in ( Vertical_Line (p `1 ))

    proof

      p in { q where q be Point of ( TOP-REAL 2) : (p `1 ) = (q `1 ) };

      hence thesis by JORDAN6:def 6;

    end;

    theorem :: JORDAN1A:9

     |[r, s]| in ( Vertical_Line r)

    proof

      ( |[r, s]| `1 ) = r by EUCLID: 52;

      hence thesis by Th8;

    end;

    theorem :: JORDAN1A:10

    for A be Subset of ( TOP-REAL 2) st A c= ( Vertical_Line s) holds A is vertical

    proof

      

       A1: ( Vertical_Line s) = { p where p be Point of ( TOP-REAL 2) : (p `1 ) = s } by JORDAN6:def 6;

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

       A2: A c= ( Vertical_Line s);

      for p,q be Point of ( TOP-REAL 2) st p in A & q in A holds (p `1 ) = (q `1 )

      proof

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

        assume p in A;

        then p in ( Vertical_Line s) by A2;

        then

         A3: ex p1 be Point of ( TOP-REAL 2) st p1 = p & (p1 `1 ) = s by A1;

        assume q in A;

        then q in ( Vertical_Line s) by A2;

        then ex p1 be Point of ( TOP-REAL 2) st p1 = q & (p1 `1 ) = s by A1;

        hence thesis by A3;

      end;

      hence thesis by SPPOL_1:def 3;

    end;

    theorem :: JORDAN1A:11

    (p `1 ) = (q `1 ) & r in [.( proj2 . p), ( proj2 . q).] implies |[(p `1 ), r]| in ( LSeg (p,q))

    proof

      assume

       A1: (p `1 ) = (q `1 );

      assume

       A2: r in [.( proj2 . p), ( proj2 . q).];

      

       A3: ( |[(p `1 ), r]| `2 ) = r by EUCLID: 52;

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

      then

       A4: ( |[(p `1 ), r]| `2 ) <= (q `2 ) by A2, A3, XXREAL_1: 1;

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

      then (p `1 ) = ( |[(p `1 ), r]| `1 ) & (p `2 ) <= ( |[(p `1 ), r]| `2 ) by A2, A3, EUCLID: 52, XXREAL_1: 1;

      hence thesis by A1, A4, GOBOARD7: 7;

    end;

    theorem :: JORDAN1A:12

    (p `2 ) = (q `2 ) & r in [.( proj1 . p), ( proj1 . q).] implies |[r, (p `2 )]| in ( LSeg (p,q))

    proof

      assume

       A1: (p `2 ) = (q `2 );

      assume

       A2: r in [.( proj1 . p), ( proj1 . q).];

      

       A3: ( |[r, (p `2 )]| `1 ) = r by EUCLID: 52;

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

      then

       A4: ( |[r, (p `2 )]| `1 ) <= (q `1 ) by A2, A3, XXREAL_1: 1;

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

      then (p `2 ) = ( |[r, (p `2 )]| `2 ) & (p `1 ) <= ( |[r, (p `2 )]| `1 ) by A2, A3, EUCLID: 52, XXREAL_1: 1;

      hence thesis by A1, A4, GOBOARD7: 8;

    end;

    theorem :: JORDAN1A:13

    p in ( Vertical_Line s) & q in ( Vertical_Line s) implies ( LSeg (p,q)) c= ( Vertical_Line s)

    proof

      

       A1: ( Vertical_Line s) = { p1 where p1 be Point of ( TOP-REAL 2) : (p1 `1 ) = s } by JORDAN6:def 6;

      assume p in ( Vertical_Line s) & q in ( Vertical_Line s);

      then

       A2: (p `1 ) = s & (q `1 ) = s by JORDAN6: 31;

      let u be object;

      assume

       A3: u in ( LSeg (p,q));

      then

      reconsider p1 = u as Point of ( TOP-REAL 2);

      (p1 `1 ) = s by A2, A3, GOBOARD7: 5;

      hence thesis by A1;

    end;

    theorem :: JORDAN1A:14

    for A,B be Subset of ( TOP-REAL 2) st A meets B holds ( proj2 .: A) meets ( proj2 .: B)

    proof

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

      assume A meets B;

      then

      consider e be object such that

       A1: e in A and

       A2: e in B by XBOOLE_0: 3;

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

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

      then (e `2 ) in ( proj2 .: A) & (e `2 ) in ( proj2 .: B) by A1, A2, FUNCT_2: 35;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: JORDAN1A:15

    for A,B be Subset of ( TOP-REAL 2) st A misses B & A c= ( Vertical_Line s) & B c= ( Vertical_Line s) holds ( proj2 .: A) misses ( proj2 .: B)

    proof

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

       A1: A misses B and

       A2: A c= ( Vertical_Line s) and

       A3: B c= ( Vertical_Line s);

      assume ( proj2 .: A) meets ( proj2 .: B);

      then

      consider e be object such that

       A4: e in ( proj2 .: A) and

       A5: e in ( proj2 .: B) by XBOOLE_0: 3;

      reconsider e as Real by A4;

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

       A6: d in B and

       A7: e = ( proj2 . d) by A5, FUNCT_2: 65;

      

       A8: (d `1 ) = s by A3, A6, JORDAN6: 31;

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

       A9: c in A and

       A10: e = ( proj2 . c) by A4, FUNCT_2: 65;

      (c `1 ) = s by A2, A9, JORDAN6: 31;

      

      then c = |[(d `1 ), (c `2 )]| by A8, EUCLID: 53

      .= |[(d `1 ), e]| by A10, PSCOMP_1:def 6

      .= |[(d `1 ), (d `2 )]| by A7, PSCOMP_1:def 6

      .= d by EUCLID: 53;

      hence contradiction by A1, A9, A6, XBOOLE_0: 3;

    end;

    begin

    theorem :: JORDAN1A:16

    1 <= i & i <= ( len G) & 1 <= j & j <= ( width G) implies (G * (i,j)) in ( LSeg ((G * (i,1)),(G * (i,( width G)))))

    proof

      assume that

       A1: 1 <= i & i <= ( len G) and

       A2: 1 <= j & j <= ( width G);

      

       A3: ((G * (i,j)) `2 ) <= ((G * (i,( width G))) `2 ) by A1, A2, SPRECT_3: 12;

      1 <= ( width G) by A2, XXREAL_0: 2;

      then

       A4: ((G * (i,1)) `1 ) = ((G * (i,( width G))) `1 ) by A1, GOBOARD5: 2;

      ((G * (i,1)) `1 ) = ((G * (i,j)) `1 ) & ((G * (i,1)) `2 ) <= ((G * (i,j)) `2 ) by A1, A2, GOBOARD5: 2, SPRECT_3: 12;

      hence thesis by A4, A3, GOBOARD7: 7;

    end;

    theorem :: JORDAN1A:17

    1 <= i & i <= ( len G) & 1 <= j & j <= ( width G) implies (G * (i,j)) in ( LSeg ((G * (1,j)),(G * (( len G),j))))

    proof

      assume that

       A1: 1 <= i & i <= ( len G) and

       A2: 1 <= j & j <= ( width G);

      

       A3: ((G * (i,j)) `1 ) <= ((G * (( len G),j)) `1 ) by A1, A2, SPRECT_3: 13;

      1 <= ( len G) by A1, XXREAL_0: 2;

      then

       A4: ((G * (1,j)) `2 ) = ((G * (( len G),j)) `2 ) by A2, GOBOARD5: 1;

      ((G * (1,j)) `2 ) = ((G * (i,j)) `2 ) & ((G * (1,j)) `1 ) <= ((G * (i,j)) `1 ) by A1, A2, GOBOARD5: 1, SPRECT_3: 13;

      hence thesis by A4, A3, GOBOARD7: 8;

    end;

    theorem :: JORDAN1A:18

    

     Th18: 1 <= j1 & j1 <= ( width G) & 1 <= j2 & j2 <= ( width G) & 1 <= i1 & i1 <= i2 & i2 <= ( len G) implies ((G * (i1,j1)) `1 ) <= ((G * (i2,j2)) `1 )

    proof

      assume that

       A1: 1 <= j1 & j1 <= ( width G) and

       A2: 1 <= j2 & j2 <= ( width G) and

       A3: 1 <= i1 & i1 <= i2 and

       A4: i2 <= ( len G);

      

       A5: 1 <= i2 by A3, XXREAL_0: 2;

      

      then ((G * (i2,j1)) `1 ) = ((G * (i2,1)) `1 ) by A1, A4, GOBOARD5: 2

      .= ((G * (i2,j2)) `1 ) by A2, A4, A5, GOBOARD5: 2;

      hence thesis by A1, A3, A4, SPRECT_3: 13;

    end;

    theorem :: JORDAN1A:19

    

     Th19: 1 <= i1 & i1 <= ( len G) & 1 <= i2 & i2 <= ( len G) & 1 <= j1 & j1 <= j2 & j2 <= ( width G) implies ((G * (i1,j1)) `2 ) <= ((G * (i2,j2)) `2 )

    proof

      assume that

       A1: 1 <= i1 & i1 <= ( len G) and

       A2: 1 <= i2 & i2 <= ( len G) and

       A3: 1 <= j1 & j1 <= j2 and

       A4: j2 <= ( width G);

      

       A5: 1 <= j2 by A3, XXREAL_0: 2;

      

      then ((G * (i1,j2)) `2 ) = ((G * (1,j2)) `2 ) by A1, A4, GOBOARD5: 1

      .= ((G * (i2,j2)) `2 ) by A2, A4, A5, GOBOARD5: 1;

      hence thesis by A1, A3, A4, SPRECT_3: 12;

    end;

    theorem :: JORDAN1A:20

    

     Th20: for f be non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= ( len G) holds ((G * (t,( width G))) `2 ) >= ( N-bound ( L~ f))

    proof

      let f be non constant standard special_circular_sequence;

      ( N-min ( L~ f)) in ( rng f) by SPRECT_2: 39;

      then

      consider x be object such that

       A1: x in ( dom f) and

       A2: (f . x) = ( N-min ( L~ f)) by FUNCT_1:def 3;

      reconsider x as Nat by A1;

      assume f is_sequence_on G;

      then

      consider i, j such that

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

       A4: (f /. x) = (G * (i,j)) by A1, GOBOARD1:def 9;

      

       A5: 1 <= i & i <= ( len G) by A3, MATRIX_0: 32;

      assume

       A6: 1 <= t & t <= ( len G);

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

      then ( N-bound ( L~ f)) = (( N-min ( L~ f)) `2 ) & ((G * (t,( width G))) `2 ) >= ((G * (i,j)) `2 ) by A6, A5, Th19, EUCLID: 52;

      hence thesis by A1, A2, A4, PARTFUN1:def 6;

    end;

    theorem :: JORDAN1A:21

    

     Th21: for f be non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= ( width G) holds ((G * (1,t)) `1 ) <= ( W-bound ( L~ f))

    proof

      let f be non constant standard special_circular_sequence;

      ( W-min ( L~ f)) in ( rng f) by SPRECT_2: 43;

      then

      consider x be object such that

       A1: x in ( dom f) and

       A2: (f . x) = ( W-min ( L~ f)) by FUNCT_1:def 3;

      reconsider x as Nat by A1;

      assume f is_sequence_on G;

      then

      consider i, j such that

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

       A4: (f /. x) = (G * (i,j)) by A1, GOBOARD1:def 9;

      

       A5: 1 <= i & i <= ( len G) by A3, MATRIX_0: 32;

      assume

       A6: 1 <= t & t <= ( width G);

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

      then ( W-bound ( L~ f)) = (( W-min ( L~ f)) `1 ) & ((G * (1,t)) `1 ) <= ((G * (i,j)) `1 ) by A6, A5, Th18, EUCLID: 52;

      hence thesis by A1, A2, A4, PARTFUN1:def 6;

    end;

    theorem :: JORDAN1A:22

    

     Th22: for f be non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= ( len G) holds ((G * (t,1)) `2 ) <= ( S-bound ( L~ f))

    proof

      let f be non constant standard special_circular_sequence;

      ( S-min ( L~ f)) in ( rng f) by SPRECT_2: 41;

      then

      consider x be object such that

       A1: x in ( dom f) and

       A2: (f . x) = ( S-min ( L~ f)) by FUNCT_1:def 3;

      reconsider x as Nat by A1;

      assume f is_sequence_on G;

      then

      consider i, j such that

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

       A4: (f /. x) = (G * (i,j)) by A1, GOBOARD1:def 9;

      

       A5: 1 <= i & i <= ( len G) by A3, MATRIX_0: 32;

      assume

       A6: 1 <= t & t <= ( len G);

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

      then ( S-bound ( L~ f)) = (( S-min ( L~ f)) `2 ) & ((G * (t,1)) `2 ) <= ((G * (i,j)) `2 ) by A6, A5, Th19, EUCLID: 52;

      hence thesis by A1, A2, A4, PARTFUN1:def 6;

    end;

    theorem :: JORDAN1A:23

    

     Th23: for f be non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= ( width G) holds ((G * (( len G),t)) `1 ) >= ( E-bound ( L~ f))

    proof

      let f be non constant standard special_circular_sequence;

      ( E-min ( L~ f)) in ( rng f) by SPRECT_2: 45;

      then

      consider x be object such that

       A1: x in ( dom f) and

       A2: (f . x) = ( E-min ( L~ f)) by FUNCT_1:def 3;

      reconsider x as Nat by A1;

      assume f is_sequence_on G;

      then

      consider i, j such that

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

       A4: (f /. x) = (G * (i,j)) by A1, GOBOARD1:def 9;

      

       A5: 1 <= i & i <= ( len G) by A3, MATRIX_0: 32;

      assume

       A6: 1 <= t & t <= ( width G);

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

      then ( E-bound ( L~ f)) = (( E-min ( L~ f)) `1 ) & ((G * (( len G),t)) `1 ) >= ((G * (i,j)) `1 ) by A6, A5, Th18, EUCLID: 52;

      hence thesis by A1, A2, A4, PARTFUN1:def 6;

    end;

    theorem :: JORDAN1A:24

    

     Th24: i <= ( len G) & j <= ( width G) implies ( cell (G,i,j)) is non empty

    proof

      assume i <= ( len G) & j <= ( width G);

      then ( Int ( cell (G,i,j))) is non empty by GOBOARD9: 14;

      hence thesis by TOPS_1: 16, XBOOLE_1: 3;

    end;

    theorem :: JORDAN1A:25

    

     Th25: i <= ( len G) & j <= ( width G) implies ( cell (G,i,j)) is connected

    proof

      assume

       A1: i <= ( len G) & j <= ( width G);

      then ( Int ( cell (G,i,j))) is convex by GOBOARD9: 17;

      then ( Cl ( Int ( cell (G,i,j)))) is connected by CONNSP_1: 19;

      hence thesis by A1, GOBRD11: 35;

    end;

    theorem :: JORDAN1A:26

    

     Th26: i <= ( len G) implies not ( cell (G,i, 0 )) is bounded

    proof

      assume

       A1: i <= ( len G);

      per cases by A1, NAT_1: 14, XXREAL_0: 1;

        suppose i = 0 ;

        then

         A2: ( cell (G,i, 0 )) = { |[r, s]| where r,s be Real : r <= ((G * (1,1)) `1 ) & s <= ((G * (1,1)) `2 ) } by GOBRD11: 24;

         not ex r be Real st for q be Point of ( TOP-REAL 2) st q in ( cell (G,i, 0 )) holds |.q.| < r

        proof

          let r be Real;

          take q = |[( min (( - r),((G * (1,1)) `1 ))), ( min (( - r),((G * (1,1)) `2 )))]|;

          

           A3: |.(q `1 ).| <= |.q.| by JGRAPH_1: 33;

          ( min (( - r),((G * (1,1)) `1 ))) <= ((G * (1,1)) `1 ) & ( min (( - r),((G * (1,1)) `2 ))) <= ((G * (1,1)) `2 ) by XXREAL_0: 17;

          hence q in ( cell (G,i, 0 )) by A2;

          per cases ;

            suppose r <= 0 ;

            hence thesis;

          end;

            suppose

             A4: r > 0 ;

            (q `1 ) = ( min (( - r),((G * (1,1)) `1 ))) by EUCLID: 52;

            then

             A5: |.( - r).| <= |.(q `1 ).| by A4, TOPREAL6: 3, XXREAL_0: 17;

            ( - ( - r)) > 0 by A4;

            then ( - r) < 0 ;

            then ( - ( - r)) <= |.(q `1 ).| by A5, ABSVALUE:def 1;

            hence thesis by A3, XXREAL_0: 2;

          end;

        end;

        hence thesis by JORDAN2C: 34;

      end;

        suppose

         A6: i >= 1 & i < ( len G);

        then

         A7: ( cell (G,i, 0 )) = { |[r, s]| where r be Real, s be Real : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) & s <= ((G * (1,1)) `2 ) } by GOBRD11: 30;

         not ex r be Real st for q be Point of ( TOP-REAL 2) st q in ( cell (G,i, 0 )) holds |.q.| < r

        proof

          let r be Real;

          take q = |[((G * (i,1)) `1 ), ( min (( - r),((G * (1,1)) `2 )))]|;

          

           A8: ( min (( - r),((G * (1,1)) `2 ))) <= ((G * (1,1)) `2 ) by XXREAL_0: 17;

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

          then

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

          i < (i + 1) & (i + 1) <= ( len G) by A6, NAT_1: 13;

          then ((G * (i,1)) `1 ) <= ((G * ((i + 1),1)) `1 ) by A6, A9, GOBOARD5: 3;

          hence q in ( cell (G,i, 0 )) by A7, A8;

          

           A10: |.(q `2 ).| <= |.q.| by JGRAPH_1: 33;

          per cases ;

            suppose r <= 0 ;

            hence thesis;

          end;

            suppose

             A11: r > 0 ;

            (q `2 ) = ( min (( - r),((G * (1,1)) `2 ))) by EUCLID: 52;

            then

             A12: |.( - r).| <= |.(q `2 ).| by A11, TOPREAL6: 3, XXREAL_0: 17;

            ( - ( - r)) > 0 by A11;

            then ( - r) < 0 ;

            then ( - ( - r)) <= |.(q `2 ).| by A12, ABSVALUE:def 1;

            hence thesis by A10, XXREAL_0: 2;

          end;

        end;

        hence thesis by JORDAN2C: 34;

      end;

        suppose i = ( len G);

        then

         A13: ( cell (G,i, 0 )) = { |[r, s]| where r be Real, s be Real : ((G * (( len G),1)) `1 ) <= r & s <= ((G * (1,1)) `2 ) } by GOBRD11: 27;

         not ex r be Real st for q be Point of ( TOP-REAL 2) st q in ( cell (G,i, 0 )) holds |.q.| < r

        proof

          let r be Real;

          take q = |[( max (r,((G * (( len G),1)) `1 ))), ((G * (1,1)) `2 )]|;

          

           A14: |.(q `1 ).| <= |.q.| by JGRAPH_1: 33;

          ((G * (( len G),1)) `1 ) <= ( max (r,((G * (( len G),1)) `1 ))) by XXREAL_0: 25;

          hence q in ( cell (G,i, 0 )) by A13;

          per cases ;

            suppose r <= 0 ;

            hence thesis;

          end;

            suppose

             A15: r > 0 ;

            (q `1 ) = ( max (r,((G * (( len G),1)) `1 ))) by EUCLID: 52;

            then r <= (q `1 ) by XXREAL_0: 25;

            then r <= |.(q `1 ).| by A15, ABSVALUE:def 1;

            hence thesis by A14, XXREAL_0: 2;

          end;

        end;

        hence thesis by JORDAN2C: 34;

      end;

    end;

    theorem :: JORDAN1A:27

    

     Th27: i <= ( len G) implies not ( cell (G,i,( width G))) is bounded

    proof

      assume

       A1: i <= ( len G);

      per cases by A1, NAT_1: 14, XXREAL_0: 1;

        suppose

         A2: i = 0 ;

        

         A3: ( cell (G, 0 ,( width G))) = { |[r, s]| where r be Real, s be Real : r <= ((G * (1,1)) `1 ) & ((G * (1,( width G))) `2 ) <= s } by GOBRD11: 25;

         not ex r be Real st for q be Point of ( TOP-REAL 2) st q in ( cell (G, 0 ,( width G))) holds |.q.| < r

        proof

          let r be Real;

          take q = |[( min (( - r),((G * (1,1)) `1 ))), ((G * (1,( width G))) `2 )]|;

          

           A4: |.(q `1 ).| <= |.q.| by JGRAPH_1: 33;

          ( min (( - r),((G * (1,1)) `1 ))) <= ((G * (1,1)) `1 ) by XXREAL_0: 17;

          hence q in ( cell (G, 0 ,( width G))) by A3;

          per cases ;

            suppose r <= 0 ;

            hence thesis;

          end;

            suppose

             A5: r > 0 ;

            (q `1 ) = ( min (( - r),((G * (1,1)) `1 ))) by EUCLID: 52;

            then

             A6: |.( - r).| <= |.(q `1 ).| by A5, TOPREAL6: 3, XXREAL_0: 17;

            ( - ( - r)) > 0 by A5;

            then ( - r) < 0 ;

            then ( - ( - r)) <= |.(q `1 ).| by A6, ABSVALUE:def 1;

            hence thesis by A4, XXREAL_0: 2;

          end;

        end;

        hence thesis by A2, JORDAN2C: 34;

      end;

        suppose

         A7: i >= 1 & i < ( len G);

        then

         A8: ( cell (G,i,( width G))) = { |[r, s]| where r be Real, s be Real : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) & ((G * (1,( width G))) `2 ) <= s } by GOBRD11: 31;

         not ex r be Real st for q be Point of ( TOP-REAL 2) st q in ( cell (G,i,( width G))) holds |.q.| < r

        proof

          let r be Real;

          take q = |[((G * (i,1)) `1 ), ( max (r,((G * (1,( width G))) `2 )))]|;

          

           A9: ( max (r,((G * (1,( width G))) `2 ))) >= ((G * (1,( width G))) `2 ) by XXREAL_0: 25;

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

          then

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

          i < (i + 1) & (i + 1) <= ( len G) by A7, NAT_1: 13;

          then ((G * (i,1)) `1 ) <= ((G * ((i + 1),1)) `1 ) by A7, A10, GOBOARD5: 3;

          hence q in ( cell (G,i,( width G))) by A8, A9;

          

           A11: |.(q `2 ).| <= |.q.| by JGRAPH_1: 33;

          per cases ;

            suppose r <= 0 ;

            hence thesis;

          end;

            suppose

             A12: r > 0 ;

            (q `2 ) = ( max (r,((G * (1,( width G))) `2 ))) by EUCLID: 52;

            then (q `2 ) >= r by XXREAL_0: 25;

            then r <= |.(q `2 ).| by A12, ABSVALUE:def 1;

            hence thesis by A11, XXREAL_0: 2;

          end;

        end;

        hence thesis by JORDAN2C: 34;

      end;

        suppose

         A13: i = ( len G);

        

         A14: ( cell (G,( len G),( width G))) = { |[r, s]| where r,s be Real : ((G * (( len G),1)) `1 ) <= r & ((G * (1,( width G))) `2 ) <= s } by GOBRD11: 28;

         not ex r be Real st for q be Point of ( TOP-REAL 2) st q in ( cell (G,i,( width G))) holds |.q.| < r

        proof

          let r be Real;

          take q = |[( max (r,((G * (( len G),1)) `1 ))), ((G * (1,( width G))) `2 )]|;

          

           A15: |.(q `1 ).| <= |.q.| by JGRAPH_1: 33;

          ((G * (( len G),1)) `1 ) <= ( max (r,((G * (( len G),1)) `1 ))) by XXREAL_0: 25;

          hence q in ( cell (G,i,( width G))) by A13, A14;

          per cases ;

            suppose r <= 0 ;

            hence thesis;

          end;

            suppose

             A16: r > 0 ;

            (q `1 ) = ( max (r,((G * (( len G),1)) `1 ))) by EUCLID: 52;

            then r <= (q `1 ) by XXREAL_0: 25;

            then r <= |.(q `1 ).| by A16, ABSVALUE:def 1;

            hence thesis by A15, XXREAL_0: 2;

          end;

        end;

        hence thesis by JORDAN2C: 34;

      end;

    end;

    begin

    theorem :: JORDAN1A:28

    ( width ( Gauge (D,n))) = ((2 |^ n) + 3)

    proof

      

      thus ( width ( Gauge (D,n))) = ( len ( Gauge (D,n))) by JORDAN8:def 1

      .= ((2 |^ n) + 3) by JORDAN8:def 1;

    end;

    theorem :: JORDAN1A:29

    i < j implies ( len ( Gauge (D,i))) < ( len ( Gauge (D,j)))

    proof

      assume i < j;

      then

       A1: (2 |^ i) < (2 |^ j) by PEPIN: 66;

      ( len ( Gauge (D,i))) = ((2 |^ i) + 3) & ( len ( Gauge (D,j))) = ((2 |^ j) + 3) by JORDAN8:def 1;

      hence thesis by A1, XREAL_1: 6;

    end;

    theorem :: JORDAN1A:30

    i <= j implies ( len ( Gauge (D,i))) <= ( len ( Gauge (D,j)))

    proof

      assume i <= j;

      then

       A1: (2 |^ i) <= (2 |^ j) by PREPOWER: 93;

      ( len ( Gauge (D,i))) = ((2 |^ i) + 3) & ( len ( Gauge (D,j))) = ((2 |^ j) + 3) by JORDAN8:def 1;

      hence thesis by A1, XREAL_1: 6;

    end;

    theorem :: JORDAN1A:31

    

     Th31: m <= n & 1 < i & i < ( len ( Gauge (D,m))) implies 1 < (((2 |^ (n -' m)) * (i - 2)) + 2) & (((2 |^ (n -' m)) * (i - 2)) + 2) < ( len ( Gauge (D,n)))

    proof

      assume that

       A1: m <= n and

       A2: 1 < i and

       A3: i < ( len ( Gauge (D,m)));

      (1 + 1) <= i by A2, NAT_1: 13;

      then

      reconsider i2 = (i - 2) as Element of NAT by INT_1: 5;

       0 < (((2 |^ (n -' m)) * i2) + 1);

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

      hence 1 < (((2 |^ (n -' m)) * (i - 2)) + 2);

      ( len ( Gauge (D,m))) = ((2 |^ m) + (2 + 1)) by JORDAN8:def 1

      .= (((2 |^ m) + 2) + 1);

      then i <= ((2 |^ m) + 2) by A3, NAT_1: 13;

      then i2 <= (2 |^ m) by XREAL_1: 20;

      then ((2 |^ (n -' m)) * i2) <= ((2 |^ (n -' m)) * (2 |^ m)) by XREAL_1: 64;

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

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

      then ((2 |^ (n -' m)) * i2) < ((2 |^ n) + 1) by NAT_1: 13;

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

      then (((2 |^ (n -' m)) * (i - 2)) + 2) < ((2 |^ n) + (1 + 2));

      hence thesis by JORDAN8:def 1;

    end;

    theorem :: JORDAN1A:32

    

     Th32: m <= n & 1 < i & i < ( width ( Gauge (D,m))) implies 1 < (((2 |^ (n -' m)) * (i - 2)) + 2) & (((2 |^ (n -' m)) * (i - 2)) + 2) < ( width ( Gauge (D,n)))

    proof

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

      hence thesis by Th31;

    end;

    theorem :: JORDAN1A:33

    

     Th33: m <= n & 1 < i & i < ( len ( Gauge (D,m))) & 1 < j & j < ( width ( Gauge (D,m))) implies for i1,j1 be Nat st i1 = (((2 |^ (n -' m)) * (i - 2)) + 2) & j1 = (((2 |^ (n -' m)) * (j - 2)) + 2) holds (( Gauge (D,m)) * (i,j)) = (( Gauge (D,n)) * (i1,j1))

    proof

      assume that

       A1: m <= n and

       A2: 1 < i & i < ( len ( Gauge (D,m))) and

       A3: 1 < j & j < ( width ( Gauge (D,m)));

      let i1,j1 be Nat such that

       A4: i1 = (((2 |^ (n -' m)) * (i - 2)) + 2) and

       A5: j1 = (((2 |^ (n -' m)) * (j - 2)) + 2);

      

       A6: 1 < i1 & i1 < ( len ( Gauge (D,n))) by A1, A2, A4, Th31;

      ((j - 2) / (2 |^ m)) = ((j - 2) / (2 |^ (n -' (n -' m)))) by A1, NAT_D: 58

      .= ((j - 2) / ((2 |^ n) / (2 |^ (n -' m)))) by NAT_D: 50, TOPREAL6: 10

      .= ((j1 - 2) / (2 |^ n)) by A5, XCMPLX_1: 77;

      

      then

       A7: (((( N-bound D) - ( S-bound D)) / (2 |^ m)) * (j - 2)) = ((( N-bound D) - ( S-bound D)) * ((j1 - 2) / (2 |^ n))) by XCMPLX_1: 75

      .= (((( N-bound D) - ( S-bound D)) / (2 |^ n)) * (j1 - 2)) by XCMPLX_1: 75;

      ((i - 2) / (2 |^ m)) = ((i - 2) / (2 |^ (n -' (n -' m)))) by A1, NAT_D: 58

      .= ((i - 2) / ((2 |^ n) / (2 |^ (n -' m)))) by NAT_D: 50, TOPREAL6: 10

      .= ((i1 - 2) / (2 |^ n)) by A4, XCMPLX_1: 77;

      

      then

       A8: (((( E-bound D) - ( W-bound D)) / (2 |^ m)) * (i - 2)) = ((( E-bound D) - ( W-bound D)) * ((i1 - 2) / (2 |^ n))) by XCMPLX_1: 75

      .= (((( E-bound D) - ( W-bound D)) / (2 |^ n)) * (i1 - 2)) by XCMPLX_1: 75;

      1 < j1 & j1 < ( width ( Gauge (D,n))) by A1, A3, A5, Th32;

      then

       A9: [i1, j1] in ( Indices ( Gauge (D,n))) by A6, MATRIX_0: 30;

       [i, j] in ( Indices ( Gauge (D,m))) by A2, A3, MATRIX_0: 30;

      

      hence (( Gauge (D,m)) * (i,j)) = |[(( W-bound D) + (((( E-bound D) - ( W-bound D)) / (2 |^ m)) * (i - 2))), (( S-bound D) + (((( N-bound D) - ( S-bound D)) / (2 |^ m)) * (j - 2)))]| by JORDAN8:def 1

      .= (( Gauge (D,n)) * (i1,j1)) by A9, A8, A7, JORDAN8:def 1;

    end;

    theorem :: JORDAN1A:34

    

     Th34: m <= n & 1 < i & (i + 1) < ( len ( Gauge (D,m))) implies 1 < (((2 |^ (n -' m)) * (i - 1)) + 2) & (((2 |^ (n -' m)) * (i - 1)) + 2) <= ( len ( Gauge (D,n)))

    proof

      assume that

       A1: m <= n and

       A2: 1 < i and

       A3: (i + 1) < ( len ( Gauge (D,m)));

      reconsider i2 = (i - 1) as Element of NAT by A2, INT_1: 5;

       0 < (((2 |^ (n -' m)) * i2) + 1);

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

      hence 1 < (((2 |^ (n -' m)) * (i - 1)) + 2);

      ( len ( Gauge (D,m))) = ((2 |^ m) + (2 + 1)) by JORDAN8:def 1

      .= (((2 |^ m) + 2) + 1);

      then (i + 1) <= (((2 |^ m) + 1) + 1) by A3, NAT_1: 13;

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

      then i2 <= (2 |^ m) by XREAL_1: 20;

      then ((2 |^ (n -' m)) * i2) <= ((2 |^ (n -' m)) * (2 |^ m)) by XREAL_1: 64;

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

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

      then ((2 |^ (n -' m)) * i2) <= ((2 |^ n) + 1) by NAT_1: 13;

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

      then (((2 |^ (n -' m)) * (i - 1)) + 2) <= ((2 |^ n) + (1 + 2));

      hence thesis by JORDAN8:def 1;

    end;

    theorem :: JORDAN1A:35

    

     Th35: m <= n & 1 < i & (i + 1) < ( width ( Gauge (D,m))) implies 1 < (((2 |^ (n -' m)) * (i - 1)) + 2) & (((2 |^ (n -' m)) * (i - 1)) + 2) <= ( width ( Gauge (D,n)))

    proof

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

      hence thesis by Th34;

    end;

     Lm3:

    now

      let D, n;

      set G = ( Gauge (D,n));

      ( 0 + 1) <= ((( len G) div 2) + 1) by XREAL_1: 6;

      hence 1 <= ( Center G);

       0 < ( len G) by JORDAN8: 10;

      then (( len G) div 2) < ( len G) by INT_1: 56;

      hence ( Center G) <= ( len G) by NAT_1: 13;

    end;

     Lm4:

    now

      let D, n, j;

      set G = ( Gauge (D,n));

      assume

       A1: 1 <= j & j <= ( len G);

      

       A2: ( len G) = ( width G) & ( 0 + 1) <= ((( len G) div 2) + 1) by JORDAN8:def 1, XREAL_1: 6;

      ( Center G) <= ( len G) by Lm3;

      hence [( Center G), j] in ( Indices G) by A1, A2, MATRIX_0: 30;

    end;

     Lm5:

    now

      let D, n, j;

      set G = ( Gauge (D,n));

      assume

       A1: 1 <= j & j <= ( len G);

      

       A2: ( len G) = ( width G) & ( 0 + 1) <= ((( len G) div 2) + 1) by JORDAN8:def 1, XREAL_1: 6;

      ( Center G) <= ( len G) by Lm3;

      hence [j, ( Center G)] in ( Indices G) by A1, A2, MATRIX_0: 30;

    end;

    

     Lm6: for w be Real holds n > 0 implies ((w / (2 |^ n)) * (( Center ( Gauge (D,n))) - 2)) = (w / 2)

    proof

      let w be Real;

      set G = ( Gauge (D,n));

      

       A1: (2 |^ n) <> 0 by NEWTON: 83;

      assume

       A2: n > 0 ;

      then

       A3: ((2 |^ n) mod 2) = 0 by PEPIN: 36;

      

      thus ((w / (2 |^ n)) * (( Center G) - 2)) = ((w / (2 |^ n)) * (((((2 |^ n) + 3) div 2) + 1) - 2)) by JORDAN8:def 1

      .= ((w / (2 |^ n)) * ((((2 |^ n) + 3) div 2) + (1 - 2)))

      .= ((w / (2 |^ n)) * ((((2 |^ n) div 2) + 1) + ( - 1))) by A3, Lm1, NAT_D: 19

      .= ((w / (2 |^ n)) * ((2 |^ n) / 2)) by A2, PEPIN: 64

      .= (w / 2) by A1, XCMPLX_1: 98;

    end;

     Lm7:

    now

      let m, n;

      let c,d be Real;

      assume

       A1: 0 <= c;

      assume m <= n;

      then 0 < (2 |^ m) & (2 |^ m) <= (2 |^ n) by NEWTON: 83, PREPOWER: 93;

      hence (c / (2 |^ n)) <= (c / (2 |^ m)) by A1, XREAL_1: 118;

    end;

    

     Lm8: for m, n holds for c,d be Real st 0 <= c & m <= n holds (d + (c / (2 |^ n))) <= (d + (c / (2 |^ m))) by XREAL_1: 6, Lm7;

     Lm9:

    now

      let m, n;

      let c,d be Real;

      assume 0 <= c & m <= n;

      then (c / (2 |^ n)) <= (c / (2 |^ m)) by Lm7;

      hence (d - (c / (2 |^ m))) <= (d - (c / (2 |^ n))) by XREAL_1: 13;

    end;

    theorem :: JORDAN1A:36

    

     Th36: 1 <= i & i <= ( len ( Gauge (D,n))) & 1 <= j & j <= ( len ( Gauge (D,m))) & (n > 0 & m > 0 or n = 0 & m = 0 ) implies ((( Gauge (D,n)) * (( Center ( Gauge (D,n))),i)) `1 ) = ((( Gauge (D,m)) * (( Center ( Gauge (D,m))),j)) `1 )

    proof

      set a = ( N-bound D), s = ( S-bound D), w = ( W-bound D), e = ( E-bound D), G = ( Gauge (D,n)), M = ( Gauge (D,m));

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

      then

       A1: [( Center G), i] in ( Indices G) by Lm4;

      assume 1 <= j & j <= ( len M);

      then

       A2: [( Center M), j] in ( Indices M) by Lm4;

      assume

       A3: n > 0 & m > 0 or n = 0 & m = 0 ;

      per cases by A3;

        suppose that

         A4: n > 0 and

         A5: m > 0 ;

        

        thus ((G * (( Center G),i)) `1 ) = ( |[(w + (((e - w) / (2 |^ n)) * (( Center G) - 2))), (s + (((a - s) / (2 |^ n)) * (i - 2)))]| `1 ) by A1, JORDAN8:def 1

        .= (w + (((e - w) / (2 |^ n)) * (( Center G) - 2))) by EUCLID: 52

        .= (w + ((e - w) / 2)) by A4, Lm6

        .= (w + (((e - w) / (2 |^ m)) * (( Center M) - 2))) by A5, Lm6

        .= ( |[(w + (((e - w) / (2 |^ m)) * (( Center M) - 2))), (s + (((a - s) / (2 |^ m)) * (j - 2)))]| `1 ) by EUCLID: 52

        .= ((M * (( Center M),j)) `1 ) by A2, JORDAN8:def 1;

      end;

        suppose

         A6: n = 0 & m = 0 ;

        

        thus ((G * (( Center G),i)) `1 ) = ( |[(w + (((e - w) / (2 |^ n)) * (( Center G) - 2))), (s + (((a - s) / (2 |^ n)) * (i - 2)))]| `1 ) by A1, JORDAN8:def 1

        .= (w + (((e - w) / (2 |^ m)) * (( Center M) - 2))) by A6, EUCLID: 52

        .= ( |[(w + (((e - w) / (2 |^ m)) * (( Center M) - 2))), (s + (((a - s) / (2 |^ m)) * (j - 2)))]| `1 ) by EUCLID: 52

        .= ((M * (( Center M),j)) `1 ) by A2, JORDAN8:def 1;

      end;

    end;

    theorem :: JORDAN1A:37

    1 <= i & i <= ( len ( Gauge (D,n))) & 1 <= j & j <= ( len ( Gauge (D,m))) & (n > 0 & m > 0 or n = 0 & m = 0 ) implies ((( Gauge (D,n)) * (i,( Center ( Gauge (D,n))))) `2 ) = ((( Gauge (D,m)) * (j,( Center ( Gauge (D,m))))) `2 )

    proof

      set a = ( N-bound D), s = ( S-bound D), w = ( W-bound D), e = ( E-bound D), G = ( Gauge (D,n)), M = ( Gauge (D,m));

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

      then

       A1: [i, ( Center G)] in ( Indices G) by Lm5;

      assume 1 <= j & j <= ( len M);

      then

       A2: [j, ( Center M)] in ( Indices M) by Lm5;

      assume

       A3: n > 0 & m > 0 or n = 0 & m = 0 ;

      per cases by A3;

        suppose that

         A4: n > 0 and

         A5: m > 0 ;

        

        thus ((G * (i,( Center G))) `2 ) = ( |[(w + (((e - w) / (2 |^ n)) * (i - 2))), (s + (((a - s) / (2 |^ n)) * (( Center G) - 2)))]| `2 ) by A1, JORDAN8:def 1

        .= (s + (((a - s) / (2 |^ n)) * (( Center G) - 2))) by EUCLID: 52

        .= (s + ((a - s) / 2)) by A4, Lm6

        .= (s + (((a - s) / (2 |^ m)) * (( Center M) - 2))) by A5, Lm6

        .= ( |[(w + (((e - w) / (2 |^ m)) * (j - 2))), (s + (((a - s) / (2 |^ m)) * (( Center M) - 2)))]| `2 ) by EUCLID: 52

        .= ((M * (j,( Center M))) `2 ) by A2, JORDAN8:def 1;

      end;

        suppose

         A6: n = 0 & m = 0 ;

        

        thus ((G * (i,( Center G))) `2 ) = ( |[(w + (((e - w) / (2 |^ n)) * (i - 2))), (s + (((a - s) / (2 |^ n)) * (( Center G) - 2)))]| `2 ) by A1, JORDAN8:def 1

        .= (s + (((a - s) / (2 |^ m)) * (( Center M) - 2))) by A6, EUCLID: 52

        .= ( |[(w + (((e - w) / (2 |^ m)) * (j - 2))), (s + (((a - s) / (2 |^ m)) * (( Center M) - 2)))]| `2 ) by EUCLID: 52

        .= ((M * (j,( Center M))) `2 ) by A2, JORDAN8:def 1;

      end;

    end;

     Lm10:

    now

      let D, n;

      let e,w be Real;

      

       A1: (2 |^ n) <> 0 by NEWTON: 83;

      

      thus (w + (((e - w) / (2 |^ n)) * (( len ( Gauge (D,n))) - 2))) = (w + (((e - w) / (2 |^ n)) * (((2 |^ n) + 3) - 2))) by JORDAN8:def 1

      .= ((w + (((e - w) / (2 |^ n)) * (2 |^ n))) + ((e - w) / (2 |^ n)))

      .= ((w + (e - w)) + ((e - w) / (2 |^ n))) by A1, XCMPLX_1: 87

      .= (e + ((e - w) / (2 |^ n)));

    end;

     Lm11:

    now

      let D, n, i;

      set a = ( N-bound D), s = ( S-bound D), w = ( W-bound D), e = ( E-bound D), G = ( Gauge (D,n));

      assume [i, 1] in ( Indices G);

      

      hence ((G * (i,1)) `2 ) = ( |[(w + (((e - w) / (2 |^ n)) * (i - 2))), (s + (((a - s) / (2 |^ n)) * (1 - 2)))]| `2 ) by JORDAN8:def 1

      .= (s - ((a - s) / (2 |^ n))) by EUCLID: 52;

    end;

     Lm12:

    now

      let D, n, i;

      set a = ( N-bound D), s = ( S-bound D), w = ( W-bound D), e = ( E-bound D), G = ( Gauge (D,n));

      assume [1, i] in ( Indices G);

      

      hence ((G * (1,i)) `1 ) = ( |[(w + (((e - w) / (2 |^ n)) * (1 - 2))), (s + (((a - s) / (2 |^ n)) * (i - 2)))]| `1 ) by JORDAN8:def 1

      .= (w - ((e - w) / (2 |^ n))) by EUCLID: 52;

    end;

     Lm13:

    now

      let D, n, i;

      set a = ( N-bound D), s = ( S-bound D), w = ( W-bound D), e = ( E-bound D), G = ( Gauge (D,n));

      assume [i, ( len G)] in ( Indices G);

      

      hence ((G * (i,( len G))) `2 ) = ( |[(w + (((e - w) / (2 |^ n)) * (i - 2))), (s + (((a - s) / (2 |^ n)) * (( len G) - 2)))]| `2 ) by JORDAN8:def 1

      .= (s + (((a - s) / (2 |^ n)) * (( len G) - 2))) by EUCLID: 52

      .= (a + ((a - s) / (2 |^ n))) by Lm10;

    end;

     Lm14:

    now

      let D, n, i;

      set a = ( N-bound D), s = ( S-bound D), w = ( W-bound D), e = ( E-bound D), G = ( Gauge (D,n));

      assume [( len G), i] in ( Indices G);

      

      hence ((G * (( len G),i)) `1 ) = ( |[(w + (((e - w) / (2 |^ n)) * (( len G) - 2))), (s + (((a - s) / (2 |^ n)) * (i - 2)))]| `1 ) by JORDAN8:def 1

      .= (w + (((e - w) / (2 |^ n)) * (( len G) - 2))) by EUCLID: 52

      .= (e + ((e - w) / (2 |^ n))) by Lm10;

    end;

    theorem :: JORDAN1A:38

    1 <= i & i <= ( len ( Gauge (C,1))) implies ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),i)) `1 ) = ((( W-bound C) + ( E-bound C)) / 2)

    proof

      set a = ( N-bound C), s = ( S-bound C), w = ( W-bound C), e = ( E-bound C), G = ( Gauge (C,1));

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

      then [( Center G), i] in ( Indices G) by Lm4;

      

      hence ((G * (( Center G),i)) `1 ) = ( |[(w + (((e - w) / (2 |^ 1)) * (( Center G) - 2))), (s + (((a - s) / (2 |^ 1)) * (i - 2)))]| `1 ) by JORDAN8:def 1

      .= (w + (((e - w) / (2 |^ 1)) * (( Center G) - 2))) by EUCLID: 52

      .= (w + ((e - w) / 2)) by Lm6

      .= ((w + e) / 2);

    end;

    theorem :: JORDAN1A:39

    1 <= i & i <= ( len ( Gauge (C,1))) implies ((( Gauge (C,1)) * (i,( Center ( Gauge (C,1))))) `2 ) = ((( S-bound C) + ( N-bound C)) / 2)

    proof

      set a = ( N-bound C), s = ( S-bound C), w = ( W-bound C), e = ( E-bound C), G = ( Gauge (C,1));

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

      then [i, ( Center G)] in ( Indices G) by Lm5;

      

      hence ((G * (i,( Center G))) `2 ) = ( |[(w + (((e - w) / (2 |^ 1)) * (i - 2))), (s + (((a - s) / (2 |^ 1)) * (( Center G) - 2)))]| `2 ) by JORDAN8:def 1

      .= (s + (((a - s) / (2 |^ 1)) * (( Center G) - 2))) by EUCLID: 52

      .= (s + ((a - s) / 2)) by Lm6

      .= ((s + a) / 2);

    end;

    theorem :: JORDAN1A:40

    

     Th40: 1 <= i & i <= ( len ( Gauge (E,n))) & 1 <= j & j <= ( len ( Gauge (E,m))) & m <= n implies ((( Gauge (E,n)) * (i,( len ( Gauge (E,n))))) `2 ) <= ((( Gauge (E,m)) * (j,( len ( Gauge (E,m))))) `2 )

    proof

      set a = ( N-bound E), s = ( S-bound E), G = ( Gauge (E,n)), M = ( Gauge (E,m));

      assume that

       A1: 1 <= i & i <= ( len G) and

       A2: 1 <= j & j <= ( len M) and

       A3: m <= n;

      

       A4: ( len M) = ( width M) by JORDAN8:def 1;

      1 <= ( len M) by A2, XXREAL_0: 2;

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

      then

       A5: ((M * (j,( len M))) `2 ) = (a + ((a - s) / (2 |^ m))) by Lm13;

      

       A6: ( len G) = ( width G) by JORDAN8:def 1;

      1 <= ( len G) by A1, XXREAL_0: 2;

      then [i, ( len G)] in ( Indices G) by A1, A6, MATRIX_0: 30;

      then 0 < (a - s) & ((G * (i,( len G))) `2 ) = (a + ((a - s) / (2 |^ n))) by Lm13, SPRECT_1: 32, XREAL_1: 50;

      hence thesis by A3, A5, Lm8;

    end;

    theorem :: JORDAN1A:41

    1 <= i & i <= ( len ( Gauge (E,n))) & 1 <= j & j <= ( len ( Gauge (E,m))) & m <= n implies ((( Gauge (E,n)) * (( len ( Gauge (E,n))),i)) `1 ) <= ((( Gauge (E,m)) * (( len ( Gauge (E,m))),j)) `1 )

    proof

      set w = ( W-bound E), e = ( E-bound E), G = ( Gauge (E,n)), M = ( Gauge (E,m));

      assume that

       A1: 1 <= i & i <= ( len G) and

       A2: 1 <= j & j <= ( len M) and

       A3: m <= n;

      

       A4: ( len M) = ( width M) by JORDAN8:def 1;

      1 <= ( len M) by A2, XXREAL_0: 2;

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

      then

       A5: ((M * (( len M),j)) `1 ) = (e + ((e - w) / (2 |^ m))) by Lm14;

      

       A6: ( len G) = ( width G) by JORDAN8:def 1;

      1 <= ( len G) by A1, XXREAL_0: 2;

      then [( len G), i] in ( Indices G) by A1, A6, MATRIX_0: 30;

      then 0 < (e - w) & ((G * (( len G),i)) `1 ) = (e + ((e - w) / (2 |^ n))) by Lm14, SPRECT_1: 31, XREAL_1: 50;

      hence thesis by A3, A5, Lm8;

    end;

    theorem :: JORDAN1A:42

    1 <= i & i <= ( len ( Gauge (E,n))) & 1 <= j & j <= ( len ( Gauge (E,m))) & m <= n implies ((( Gauge (E,m)) * (1,j)) `1 ) <= ((( Gauge (E,n)) * (1,i)) `1 )

    proof

      set w = ( W-bound E), e = ( E-bound E), G = ( Gauge (E,n)), M = ( Gauge (E,m));

      assume that

       A1: 1 <= i & i <= ( len G) and

       A2: 1 <= j & j <= ( len M) and

       A3: m <= n;

      

       A4: ( len M) = ( width M) by JORDAN8:def 1;

      1 <= ( len M) by A2, XXREAL_0: 2;

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

      then

       A5: ((M * (1,j)) `1 ) = (w - ((e - w) / (2 |^ m))) by Lm12;

      

       A6: ( len G) = ( width G) by JORDAN8:def 1;

      1 <= ( len G) by A1, XXREAL_0: 2;

      then [1, i] in ( Indices G) by A1, A6, MATRIX_0: 30;

      then 0 < (e - w) & ((G * (1,i)) `1 ) = (w - ((e - w) / (2 |^ n))) by Lm12, SPRECT_1: 31, XREAL_1: 50;

      hence thesis by A3, A5, Lm9;

    end;

    theorem :: JORDAN1A:43

    1 <= i & i <= ( len ( Gauge (E,n))) & 1 <= j & j <= ( len ( Gauge (E,m))) & m <= n implies ((( Gauge (E,m)) * (j,1)) `2 ) <= ((( Gauge (E,n)) * (i,1)) `2 )

    proof

      set a = ( N-bound E), s = ( S-bound E), G = ( Gauge (E,n)), M = ( Gauge (E,m));

      assume that

       A1: 1 <= i & i <= ( len G) and

       A2: 1 <= j & j <= ( len M) and

       A3: m <= n;

      

       A4: ( len M) = ( width M) by JORDAN8:def 1;

      1 <= ( len M) by A2, XXREAL_0: 2;

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

      then

       A5: ((M * (j,1)) `2 ) = (s - ((a - s) / (2 |^ m))) by Lm11;

      

       A6: ( len G) = ( width G) by JORDAN8:def 1;

      1 <= ( len G) by A1, XXREAL_0: 2;

      then [i, 1] in ( Indices G) by A1, A6, MATRIX_0: 30;

      then 0 < (a - s) & ((G * (i,1)) `2 ) = (s - ((a - s) / (2 |^ n))) by Lm11, SPRECT_1: 32, XREAL_1: 50;

      hence thesis by A3, A5, Lm9;

    end;

    theorem :: JORDAN1A:44

    1 <= m & m <= n implies ( LSeg ((( Gauge (E,n)) * (( Center ( Gauge (E,n))),1)),(( Gauge (E,n)) * (( Center ( Gauge (E,n))),( len ( Gauge (E,n))))))) c= ( LSeg ((( Gauge (E,m)) * (( Center ( Gauge (E,m))),1)),(( Gauge (E,m)) * (( Center ( Gauge (E,m))),( len ( Gauge (E,m)))))))

    proof

      set a = ( N-bound E), s = ( S-bound E), G = ( Gauge (E,n)), M = ( Gauge (E,m)), sn = ( Center G), sm = ( Center M);

      assume

       A1: 1 <= m;

      

       A2: 1 <= ( len M) by GOBRD11: 34;

      then [sm, 1] in ( Indices M) by Lm4;

      then

       A3: ((M * (sm,1)) `2 ) = (s - ((a - s) / (2 |^ m))) by Lm11;

       [sm, ( len M)] in ( Indices M) by A2, Lm4;

      then

       A4: ((M * (sm,( len M))) `2 ) = (a + ((a - s) / (2 |^ m))) by Lm13;

      

       A5: sn <= ( len G) by Lm3;

      

       A6: 1 <= ( len G) by GOBRD11: 34;

      assume

       A7: m <= n;

      then

       A8: ((M * (sm,1)) `1 ) = ((G * (sn,( len G))) `1 ) & ((G * (sn,( len G))) `1 ) = ((M * (sm,( len M))) `1 ) by A1, A6, A2, Th36;

       0 < (a - s) by SPRECT_1: 32, XREAL_1: 50;

      then

       A9: ((a - s) / (2 |^ n)) <= ((a - s) / (2 |^ m)) by A7, Lm7;

      ( len G) = ( width G) & 1 <= sn by Lm3, JORDAN8:def 1;

      then

       A10: ((G * (sn,1)) `2 ) <= ((G * (sn,( len G))) `2 ) by A6, A5, SPRECT_3: 12;

       [sn, ( len G)] in ( Indices G) by A6, Lm4;

      then ((G * (sn,( len G))) `2 ) = (a + ((a - s) / (2 |^ n))) by Lm13;

      then

       A11: ((G * (sn,( len G))) `2 ) <= ((M * (sm,( len M))) `2 ) by A9, A4, XREAL_1: 7;

      then

       A12: ((G * (sn,1)) `2 ) <= ((M * (sm,( len M))) `2 ) by A10, XXREAL_0: 2;

       [sn, 1] in ( Indices G) by A6, Lm4;

      then ((G * (sn,1)) `2 ) = (s - ((a - s) / (2 |^ n))) by Lm11;

      then

       A13: ((M * (sm,1)) `2 ) <= ((G * (sn,1)) `2 ) by A9, A3, XREAL_1: 13;

      then ((M * (sm,1)) `2 ) <= ((G * (sn,( len G))) `2 ) by A10, XXREAL_0: 2;

      then

       A14: (G * (sn,( len G))) in ( LSeg ((M * (sm,1)),(M * (sm,( len M))))) by A11, A8, GOBOARD7: 7;

      ((M * (sm,1)) `1 ) = ((G * (sn,1)) `1 ) & ((G * (sn,1)) `1 ) = ((M * (sm,( len M))) `1 ) by A1, A7, A6, A2, Th36;

      then (G * (sn,1)) in ( LSeg ((M * (sm,1)),(M * (sm,( len M))))) by A13, A12, GOBOARD7: 7;

      hence thesis by A14, TOPREAL1: 6;

    end;

    theorem :: JORDAN1A:45

    1 <= m & m <= n & 1 <= j & j <= ( width ( Gauge (E,n))) implies ( LSeg ((( Gauge (E,n)) * (( Center ( Gauge (E,n))),1)),(( Gauge (E,n)) * (( Center ( Gauge (E,n))),j)))) c= ( LSeg ((( Gauge (E,m)) * (( Center ( Gauge (E,m))),1)),(( Gauge (E,n)) * (( Center ( Gauge (E,n))),j))))

    proof

      set a = ( N-bound E), s = ( S-bound E), w = ( W-bound E), e = ( E-bound E), G = ( Gauge (E,n)), M = ( Gauge (E,m)), sn = ( Center G), sm = ( Center M);

      assume that

       A1: 1 <= m and

       A2: m <= n and

       A3: 1 <= j and

       A4: j <= ( width G);

      now

        

         A5: 0 < (a - s) by SPRECT_1: 32, XREAL_1: 50;

        then

         A6: (s - ((a - s) / (2 |^ m))) <= (s - 0 ) by XREAL_1: 13;

        

         A7: ((a - s) / (2 |^ n)) <= ((a - s) / (2 |^ m)) by A2, A5, Lm7;

        

         A8: 1 <= ( len M) by GOBRD11: 34;

        then [sm, 1] in ( Indices M) by Lm4;

        then

         A9: ((M * (sm,1)) `2 ) = (s - ((a - s) / (2 |^ m))) by Lm11;

        let t be Nat;

        assume that

         A10: 1 <= t and

         A11: t <= j;

        1 <= sn & sn <= ( len G) by Lm3;

        then

         A12: ((G * (sn,t)) `2 ) <= ((G * (sn,j)) `2 ) by A4, A10, A11, SPRECT_3: 12;

        

         A13: ( len G) = ( width G) by JORDAN8:def 1;

        then

         A14: t <= ( len G) by A4, A11, XXREAL_0: 2;

        then

         A15: ((M * (sm,1)) `1 ) = ((G * (sn,t)) `1 ) by A1, A2, A10, A8, Th36;

        

         A16: [sn, t] in ( Indices G) by A10, A14, Lm4;

        

        then

         A17: ((G * (sn,t)) `2 ) = ( |[(w + (((e - w) / (2 |^ n)) * (sn - 2))), (s + (((a - s) / (2 |^ n)) * (t - 2)))]| `2 ) by JORDAN8:def 1

        .= (s + (((a - s) / (2 |^ n)) * (t - 2))) by EUCLID: 52;

         A18:

        now

          per cases by A10, XXREAL_0: 1;

            suppose t = 1;

            then ((G * (sn,t)) `2 ) = (s - ((a - s) / (2 |^ n))) by A16, Lm11;

            hence ((M * (sm,1)) `2 ) <= ((G * (sn,t)) `2 ) by A7, A9, XREAL_1: 13;

          end;

            suppose t > 1;

            then t >= (1 + 1) by NAT_1: 13;

            then (t - 2) >= (2 - 2) by XREAL_1: 9;

            then (s + 0 ) <= (s + (((a - s) / (2 |^ n)) * (t - 2))) by A5, XREAL_1: 6;

            hence ((M * (sm,1)) `2 ) <= ((G * (sn,t)) `2 ) by A17, A6, A9, XXREAL_0: 2;

          end;

        end;

        ((G * (sn,t)) `1 ) = ((G * (sn,j)) `1 ) by A1, A2, A3, A4, A10, A13, A14, Th36;

        hence (G * (sn,t)) in ( LSeg ((M * (sm,1)),(G * (sn,j)))) by A15, A18, A12, GOBOARD7: 7;

      end;

      then (G * (sn,1)) in ( LSeg ((M * (sm,1)),(G * (sn,j)))) & (G * (sn,j)) in ( LSeg ((M * (sm,1)),(G * (sn,j)))) by A3;

      hence thesis by TOPREAL1: 6;

    end;

    theorem :: JORDAN1A:46

    1 <= m & m <= n & 1 <= j & j <= ( width ( Gauge (E,n))) implies ( LSeg ((( Gauge (E,m)) * (( Center ( Gauge (E,m))),1)),(( Gauge (E,n)) * (( Center ( Gauge (E,n))),j)))) c= ( LSeg ((( Gauge (E,m)) * (( Center ( Gauge (E,m))),1)),(( Gauge (E,m)) * (( Center ( Gauge (E,m))),( len ( Gauge (E,m)))))))

    proof

      set a = ( N-bound E), s = ( S-bound E), w = ( W-bound E), e = ( E-bound E), G = ( Gauge (E,n)), M = ( Gauge (E,m)), sn = ( Center G), sm = ( Center M);

      assume that

       A1: 1 <= m and

       A2: m <= n and

       A3: 1 <= j and

       A4: j <= ( width G);

      

       A5: 1 <= sm & sm <= ( len M) by Lm3;

      

       A6: 1 <= sn & sn <= ( len G) by Lm3;

      then

       A7: ((G * (sn,( len G))) `2 ) <= ((M * (sm,( len M))) `2 ) by A2, A5, Th40;

      ( len G) = ( width G) by JORDAN8:def 1;

      then ((G * (sn,j)) `2 ) <= ((G * (sn,( len G))) `2 ) by A3, A4, A6, SPRECT_3: 12;

      then

       A8: ((G * (sn,j)) `2 ) <= ((M * (sm,( len M))) `2 ) by A7, XXREAL_0: 2;

      

       A9: 0 < (a - s) by SPRECT_1: 32, XREAL_1: 50;

      then

       A10: (s - ((a - s) / (2 |^ m))) <= (s - 0 ) by XREAL_1: 13;

      

       A11: 1 <= ( len M) by GOBRD11: 34;

      then [sm, 1] in ( Indices M) by Lm4;

      then

       A12: ((M * (sm,1)) `2 ) = (s - ((a - s) / (2 |^ m))) by Lm11;

      

       A13: ((a - s) / (2 |^ n)) <= ((a - s) / (2 |^ m)) by A2, A9, Lm7;

      

       A14: ( len G) = ( width G) by JORDAN8:def 1;

      then

       A15: [sn, j] in ( Indices G) by A3, A4, Lm4;

      

      then

       A16: ((G * (sn,j)) `2 ) = ( |[(w + (((e - w) / (2 |^ n)) * (sn - 2))), (s + (((a - s) / (2 |^ n)) * (j - 2)))]| `2 ) by JORDAN8:def 1

      .= (s + (((a - s) / (2 |^ n)) * (j - 2))) by EUCLID: 52;

       A17:

      now

        per cases by A3, XXREAL_0: 1;

          suppose j = 1;

          then ((G * (sn,j)) `2 ) = (s - ((a - s) / (2 |^ n))) by A15, Lm11;

          hence ((M * (sm,1)) `2 ) <= ((G * (sn,j)) `2 ) by A13, A12, XREAL_1: 13;

        end;

          suppose j > 1;

          then j >= (1 + 1) by NAT_1: 13;

          then (j - 2) >= (2 - 2) by XREAL_1: 9;

          then (s + 0 ) <= (s + (((a - s) / (2 |^ n)) * (j - 2))) by A9, XREAL_1: 6;

          hence ((M * (sm,1)) `2 ) <= ((G * (sn,j)) `2 ) by A12, A16, A10, XXREAL_0: 2;

        end;

      end;

      ( len M) = ( width M) by JORDAN8:def 1;

      then

       A18: ((M * (sm,1)) `2 ) <= ((M * (sm,( len M))) `2 ) by A11, A5, SPRECT_3: 12;

      ((M * (sm,1)) `1 ) = ((M * (sm,( len M))) `1 ) by A1, A11, Th36;

      then

       A19: (M * (sm,1)) in ( LSeg ((M * (sm,1)),(M * (sm,( len M))))) by A18, GOBOARD7: 7;

      ((M * (sm,1)) `1 ) = ((G * (sn,j)) `1 ) & ((G * (sn,j)) `1 ) = ((M * (sm,( len M))) `1 ) by A1, A2, A3, A4, A11, A14, Th36;

      then (G * (sn,j)) in ( LSeg ((M * (sm,1)),(M * (sm,( len M))))) by A17, A8, GOBOARD7: 7;

      hence thesis by A19, TOPREAL1: 6;

    end;

    theorem :: JORDAN1A:47

    

     Th47: m <= n & 1 < i & (i + 1) < ( len ( Gauge (E,m))) & 1 < j & (j + 1) < ( width ( Gauge (E,m))) implies for i1,j1 be Nat st (((2 |^ (n -' m)) * (i - 2)) + 2) <= i1 & i1 < (((2 |^ (n -' m)) * (i - 1)) + 2) & (((2 |^ (n -' m)) * (j - 2)) + 2) <= j1 & j1 < (((2 |^ (n -' m)) * (j - 1)) + 2) holds ( cell (( Gauge (E,n)),i1,j1)) c= ( cell (( Gauge (E,m)),i,j))

    proof

      set G = ( Gauge (E,m)), G1 = ( Gauge (E,n));

      assume that

       A1: m <= n and

       A2: 1 < i and

       A3: (i + 1) < ( len G) and

       A4: 1 < j and

       A5: (j + 1) < ( width G);

      set i2 = (((2 |^ (n -' m)) * (i -' 2)) + 2), j2 = (((2 |^ (n -' m)) * (j -' 2)) + 2), i3 = (((2 |^ (n -' m)) * (i -' 1)) + 2), j3 = (((2 |^ (n -' m)) * (j -' 1)) + 2);

      let i1,j1 be Nat such that

       A6: (((2 |^ (n -' m)) * (i - 2)) + 2) <= i1 and

       A7: i1 < (((2 |^ (n -' m)) * (i - 1)) + 2) and

       A8: (((2 |^ (n -' m)) * (j - 2)) + 2) <= j1 and

       A9: j1 < (((2 |^ (n -' m)) * (j - 1)) + 2);

      

       A10: (j - 1) = (j -' 1) by A4, XREAL_1: 233;

      then

       A11: j3 <= ( width G1) by A1, A4, A5, Th35;

      

       A12: (1 + 1) <= i by A2, NAT_1: 13;

      then

       A13: i2 = (((2 |^ (n -' m)) * (i - 2)) + 2) by XREAL_1: 233;

      i < (i + 1) by XREAL_1: 29;

      then

       A14: i < ( len G) by A3, XXREAL_0: 2;

      then

       A15: 1 <= (((2 |^ (n -' m)) * (i - 2)) + 2) by A1, A2, Th31;

      then

       A16: 1 <= i1 by A6, XXREAL_0: 2;

      (j1 + 1) <= (((2 |^ (n -' m)) * (j -' 1)) + 2) by A9, A10, NAT_1: 13;

      then

       A17: (j1 + 1) < j3 or (j1 + 1) = j3 by XXREAL_0: 1;

      let e be object;

      assume

       A18: e in ( cell (G1,i1,j1));

      then

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

      (((2 |^ (n -' m)) * (i - 1)) + 2) <= ( len G1) by A1, A2, A3, Th34;

      then

       A19: i1 < ( len G1) by A7, XXREAL_0: 2;

      then

       A20: (i1 + 1) <= ( len G1) by NAT_1: 13;

      

       A21: ((j + 1) - (1 + 1)) = (j - 1)

      .= (j -' 1) by A4, XREAL_1: 233;

      1 < (j + 1) by A4, XREAL_1: 29;

      then

       A22: (G * (i,(j + 1))) = (G1 * (i2,j3)) by A1, A2, A5, A14, A21, A13, Th33;

      

       A23: (i - 1) = (i -' 1) by A2, XREAL_1: 233;

      then

       A24: i3 <= ( len G1) by A1, A2, A3, Th34;

      (i1 + 1) <= (((2 |^ (n -' m)) * (i -' 1)) + 2) by A7, A23, NAT_1: 13;

      then

       A25: (i1 + 1) < i3 or (i1 + 1) = i3 by XXREAL_0: 1;

      

       A26: i2 = (((2 |^ (n -' m)) * (i - 2)) + 2) by A12, XREAL_1: 233;

      

       A27: ((i + 1) - (1 + 1)) = (i - 1)

      .= (i -' 1) by A2, XREAL_1: 233;

      

       A28: i2 = (((2 |^ (n -' m)) * (i - 2)) + 2) by A12, XREAL_1: 233;

      then

       A29: i2 <= ( len G1) by A6, A19, XXREAL_0: 2;

      j < (j + 1) by XREAL_1: 29;

      then

       A30: j < ( width G) by A5, XXREAL_0: 2;

      then

       A31: 1 <= (((2 |^ (n -' m)) * (j - 2)) + 2) by A1, A4, Th32;

      then

       A32: 1 <= j1 by A8, XXREAL_0: 2;

      then 1 < (j1 + 1) by NAT_1: 13;

      then

       A33: ((G1 * (i1,(j1 + 1))) `2 ) <= ((G1 * (i1,j3)) `2 ) by A19, A16, A11, A17, GOBOARD5: 4;

      (((2 |^ (n -' m)) * (j - 1)) + 2) <= ( width G1) by A1, A4, A5, Th35;

      then

       A34: j1 < ( width G1) by A9, XXREAL_0: 2;

      then

       A35: (j1 + 1) <= ( width G1) by NAT_1: 13;

      then

       A36: ((G1 * (i1,j1)) `1 ) <= (p `1 ) by A18, A20, A16, A32, JORDAN9: 17;

      

       A37: (1 + 1) <= j by A4, NAT_1: 13;

      then

       A38: j2 = (((2 |^ (n -' m)) * (j - 2)) + 2) by XREAL_1: 233;

      then j2 < j1 or j2 = j1 by A8, XXREAL_0: 1;

      then

       A39: ((G1 * (i1,j2)) `2 ) <= ((G1 * (i1,j1)) `2 ) by A19, A34, A16, A31, A38, GOBOARD5: 4;

      

       A40: j2 = (((2 |^ (n -' m)) * (j - 2)) + 2) by A37, XREAL_1: 233;

      then

       A41: (G * (i,j)) = (( Gauge (E,n)) * (i2,j2)) by A1, A2, A4, A14, A30, A28, Th33;

      1 < (i + 1) by A2, XREAL_1: 29;

      then

       A42: (G * ((i + 1),j)) = (G1 * (i3,j2)) by A1, A3, A4, A30, A27, A38, Th33;

      

       A43: (p `1 ) <= ((G1 * ((i1 + 1),j1)) `1 ) by A18, A20, A35, A16, A32, JORDAN9: 17;

      1 < (i1 + 1) by A16, NAT_1: 13;

      then

       A44: ((G1 * ((i1 + 1),j1)) `1 ) <= ((G1 * (i3,j1)) `1 ) by A34, A32, A24, A25, GOBOARD5: 3;

      

       A45: ((G1 * (i1,j1)) `2 ) <= (p `2 ) by A18, A20, A35, A16, A32, JORDAN9: 17;

      

       A46: j2 <= ( width G1) by A8, A34, A40, XXREAL_0: 2;

      

      then ((G1 * (i1,j2)) `2 ) = ((G1 * (1,j2)) `2 ) by A19, A16, A31, A38, GOBOARD5: 1

      .= ((G1 * (i2,j2)) `2 ) by A15, A31, A29, A46, A26, A38, GOBOARD5: 1;

      then

       A47: ((G * (i,j)) `2 ) <= (p `2 ) by A45, A41, A39, XXREAL_0: 2;

      

       A48: (p `2 ) <= ((G1 * (i1,(j1 + 1))) `2 ) by A18, A20, A35, A16, A32, JORDAN9: 17;

      

       A49: 1 < j3 by A9, A32, A10, XXREAL_0: 2;

      

      then ((G1 * (i1,j3)) `2 ) = ((G1 * (1,j3)) `2 ) by A19, A16, A11, GOBOARD5: 1

      .= ((G1 * (i2,j3)) `2 ) by A15, A29, A13, A11, A49, GOBOARD5: 1;

      then

       A50: (p `2 ) <= ((G * (i,(j + 1))) `2 ) by A48, A22, A33, XXREAL_0: 2;

      i2 < i1 or i2 = i1 by A6, A28, XXREAL_0: 1;

      then

       A51: ((G1 * (i2,j1)) `1 ) <= ((G1 * (i1,j1)) `1 ) by A19, A34, A15, A32, A28, GOBOARD5: 3;

      

       A52: 1 < i3 by A7, A16, A23, XXREAL_0: 2;

      

      then ((G1 * (i3,j1)) `1 ) = ((G1 * (i3,1)) `1 ) by A34, A32, A24, GOBOARD5: 2

      .= ((G1 * (i3,j2)) `1 ) by A31, A46, A38, A24, A52, GOBOARD5: 2;

      then

       A53: (p `1 ) <= ((G * ((i + 1),j)) `1 ) by A43, A42, A44, XXREAL_0: 2;

      ((G1 * (i2,j1)) `1 ) = ((G1 * (i2,1)) `1 ) by A34, A15, A32, A28, A29, GOBOARD5: 2

      .= ((G1 * (i2,j2)) `1 ) by A15, A31, A28, A40, A29, A46, GOBOARD5: 2;

      then ((G * (i,j)) `1 ) <= (p `1 ) by A36, A41, A51, XXREAL_0: 2;

      hence thesis by A2, A3, A4, A5, A53, A47, A50, JORDAN9: 17;

    end;

    theorem :: JORDAN1A:48

    m <= n & 3 <= i & i < ( len ( Gauge (E,m))) & 1 < j & (j + 1) < ( width ( Gauge (E,m))) implies for i1,j1 be Nat st i1 = (((2 |^ (n -' m)) * (i - 2)) + 2) & j1 = (((2 |^ (n -' m)) * (j - 2)) + 2) holds ( cell (( Gauge (E,n)),(i1 -' 1),j1)) c= ( cell (( Gauge (E,m)),(i -' 1),j))

    proof

      assume that

       A1: m <= n and

       A2: 3 <= i and

       A3: i < ( len ( Gauge (E,m))) and

       A4: 1 < j & (j + 1) < ( width ( Gauge (E,m)));

      

       A5: (i - 2) = (i -' 2) by A2, XREAL_1: 233, XXREAL_0: 2;

      

       A6: (2 + 1) <= i by A2;

      then (1 + 1) < i by NAT_1: 13;

      then

       A7: 1 < (i - 1) by XREAL_1: 20;

      

       A8: (2 |^ (n -' m)) > 0 by NEWTON: 83;

      

       A9: (i - 3) = (i -' 3) by A2, XREAL_1: 233;

      then (i -' 3) < (i -' 2) by A5, XREAL_1: 10;

      then ((2 |^ (n -' m)) * (i -' 3)) < ((2 |^ (n -' m)) * (i -' 2)) by A8, XREAL_1: 68;

      then (((2 |^ (n -' m)) * (i -' 3)) + 1) <= ((2 |^ (n -' m)) * (i -' 2)) by NAT_1: 13;

      then ((2 |^ (n -' m)) * (i -' 3)) <= (((2 |^ (n -' m)) * (i -' 2)) -' 1) by NAT_D: 55;

      then

       A10: (((2 |^ (n -' m)) * (i -' 3)) + 2) <= ((((2 |^ (n -' m)) * (i -' 2)) -' 1) + 2) by XREAL_1: 6;

      

       A11: (i -' 1) = (i - 1) by A2, XREAL_1: 233, XXREAL_0: 2;

      then

       A12: ((i -' 1) - 1) = (i - (1 + 1));

      i > (2 + 0 ) by A6, NAT_1: 13;

      then (i - 2) > 0 by XREAL_1: 20;

      then

       A13: ((2 |^ (n -' m)) * (i -' 2)) > 0 by A8, A5, XREAL_1: 129;

      then ((2 |^ (n -' m)) * (i -' 2)) >= ( 0 + 1) by NAT_1: 13;

      then

       A14: (((2 |^ (n -' m)) * ((i -' 1) - 2)) + 2) <= ((((2 |^ (n -' m)) * (i -' 2)) + 2) -' 1) by A9, A11, A10, NAT_D: 38;

      

       A15: ((i -' 1) + 1) < ( len ( Gauge (E,m))) by A2, A3, XREAL_1: 235, XXREAL_0: 2;

      let i1,j1 be Nat such that

       A16: i1 = (((2 |^ (n -' m)) * (i - 2)) + 2) and

       A17: j1 = (((2 |^ (n -' m)) * (j - 2)) + 2);

      i1 < (i1 + 1) by XREAL_1: 29;

      then

       A18: (i1 - 1) < i1 by XREAL_1: 19;

      i1 > ( 0 + 2) by A16, A5, A13, XREAL_1: 6;

      then

       A19: (i1 -' 1) < i1 by A18, XREAL_1: 233, XXREAL_0: 2;

      (j - 2) < (j - 1) by XREAL_1: 10;

      then ((2 |^ (n -' m)) * (j - 2)) < ((2 |^ (n -' m)) * (j - 1)) by A8, XREAL_1: 68;

      then j1 < (((2 |^ (n -' m)) * (j - 1)) + 2) by A17, XREAL_1: 6;

      hence thesis by A1, A4, A16, A17, A7, A15, A5, A14, A12, A19, Th47;

    end;

    theorem :: JORDAN1A:49

    for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds i <= ( len ( Gauge (C,n))) implies ( cell (( Gauge (C,n)),i, 0 )) c= ( UBD C)

    proof

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

      assume

       A1: i <= ( len ( Gauge (C,n)));

      then ( cell (( Gauge (C,n)),i, 0 )) misses C by JORDAN8: 17;

      then

       A2: ( cell (( Gauge (C,n)),i, 0 )) c= (C ` ) by SUBSET_1: 23;

       0 <= ( width ( Gauge (C,n)));

      then ( cell (( Gauge (C,n)),i, 0 )) is connected & ( cell (( Gauge (C,n)),i, 0 )) is non empty by A1, Th24, Th25;

      then

      consider W be Subset of ( TOP-REAL 2) such that

       A3: W is_a_component_of (C ` ) and

       A4: ( cell (( Gauge (C,n)),i, 0 )) c= W by A2, GOBOARD9: 3;

       not W is bounded by A1, A4, Th26, RLTOPSP1: 42;

      then W is_outside_component_of C by A3, JORDAN2C:def 3;

      then W c= ( UBD C) by JORDAN2C: 23;

      hence thesis by A4;

    end;

    theorem :: JORDAN1A:50

    for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds i <= ( len ( Gauge (E,n))) implies ( cell (( Gauge (E,n)),i,( width ( Gauge (E,n))))) c= ( UBD E)

    proof

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

      assume

       A1: i <= ( len ( Gauge (E,n)));

      ( width ( Gauge (E,n))) = ( len ( Gauge (E,n))) by JORDAN8:def 1;

      then ( cell (( Gauge (E,n)),i,( width ( Gauge (E,n))))) misses E by A1, JORDAN8: 15;

      then

       A2: ( cell (( Gauge (E,n)),i,( width ( Gauge (E,n))))) c= (E ` ) by SUBSET_1: 23;

      ( cell (( Gauge (E,n)),i,( width ( Gauge (E,n))))) is connected & ( cell (( Gauge (E,n)),i,( width ( Gauge (E,n))))) is non empty by A1, Th24, Th25;

      then

      consider W be Subset of ( TOP-REAL 2) such that

       A3: W is_a_component_of (E ` ) and

       A4: ( cell (( Gauge (E,n)),i,( width ( Gauge (E,n))))) c= W by A2, GOBOARD9: 3;

       not W is bounded by A1, A4, Th27, RLTOPSP1: 42;

      then W is_outside_component_of E by A3, JORDAN2C:def 3;

      then W c= ( UBD E) by JORDAN2C: 23;

      hence thesis by A4;

    end;

    begin

    theorem :: JORDAN1A:51

    

     Th51: p in C implies ( north_halfline p) meets ( L~ ( Cage (C,n)))

    proof

      set f = ( Cage (C,n));

      assume

       A1: p in C;

      set X = { q where q be Point of ( TOP-REAL 2) : (q `1 ) = (p `1 ) & (q `2 ) >= (p `2 ) };

      

       A2: X = ( north_halfline p) by TOPREAL1: 30;

      (( max (( N-bound ( L~ f)),(p `2 ))) + 1) > (( N-bound ( L~ f)) + 0 ) by XREAL_1: 8, XXREAL_0: 25;

      then (f /. 1) = ( N-min ( L~ f)) & ( |[(p `1 ), (( max (( N-bound ( L~ f)),(p `2 ))) + 1)]| `2 ) > ( N-bound ( L~ f)) by EUCLID: 52, JORDAN9: 32;

      then |[(p `1 ), (( max (( N-bound ( L~ f)),(p `2 ))) + 1)]| in ( LeftComp f) by JORDAN2C: 113;

      then

       A3: |[(p `1 ), (( max (( N-bound ( L~ f)),(p `2 ))) + 1)]| in ( UBD ( L~ f)) by GOBRD14: 36;

      ( LeftComp f) is_outside_component_of ( L~ f) by GOBRD14: 34;

      then ( LeftComp f) is_a_component_of (( L~ f) ` ) by JORDAN2C:def 3;

      then

       A4: ( UBD ( L~ f)) is_a_component_of (( L~ f) ` ) by GOBRD14: 36;

      reconsider X as connected Subset of ( TOP-REAL 2) by A2;

      

       A5: C c= ( BDD ( L~ f)) & p in X by JORDAN10: 12;

      ( max (( N-bound ( L~ f)),(p `2 ))) >= (p `2 ) by XXREAL_0: 25;

      then (( max (( N-bound ( L~ f)),(p `2 ))) + 1) >= ((p `2 ) + 0 ) by XREAL_1: 7;

      then

       A6: ( |[(p `1 ), (( max (( N-bound ( L~ f)),(p `2 ))) + 1)]| `2 ) >= (p `2 ) by EUCLID: 52;

      ( |[(p `1 ), (( max (( N-bound ( L~ f)),(p `2 ))) + 1)]| `1 ) = (p `1 ) by EUCLID: 52;

      then |[(p `1 ), (( max (( N-bound ( L~ f)),(p `2 ))) + 1)]| in X by A6;

      then

       A7: X meets ( UBD ( L~ f)) by A3, XBOOLE_0: 3;

      assume not thesis;

      then X c= (( L~ f) ` ) by A2, SUBSET_1: 23;

      then X c= ( UBD ( L~ f)) by A7, A4, GOBOARD9: 4;

      then p in (( BDD ( L~ f)) /\ ( UBD ( L~ f))) by A1, A5, XBOOLE_0:def 4;

      then ( BDD ( L~ f)) meets ( UBD ( L~ f));

      hence contradiction by JORDAN2C: 24;

    end;

    theorem :: JORDAN1A:52

    

     Th52: p in C implies ( east_halfline p) meets ( L~ ( Cage (C,n)))

    proof

      set f = ( Cage (C,n));

      assume

       A1: p in C;

      set X = { q where q be Point of ( TOP-REAL 2) : (q `1 ) >= (p `1 ) & (q `2 ) = (p `2 ) };

      

       A2: X = ( east_halfline p) by TOPREAL1: 32;

      (( max (( E-bound ( L~ f)),(p `1 ))) + 1) > (( E-bound ( L~ f)) + 0 ) by XREAL_1: 8, XXREAL_0: 25;

      then (f /. 1) = ( N-min ( L~ f)) & ( |[(( max (( E-bound ( L~ f)),(p `1 ))) + 1), (p `2 )]| `1 ) > ( E-bound ( L~ f)) by EUCLID: 52, JORDAN9: 32;

      then |[(( max (( E-bound ( L~ f)),(p `1 ))) + 1), (p `2 )]| in ( LeftComp f) by JORDAN2C: 111;

      then

       A3: |[(( max (( E-bound ( L~ f)),(p `1 ))) + 1), (p `2 )]| in ( UBD ( L~ f)) by GOBRD14: 36;

      ( LeftComp f) is_outside_component_of ( L~ f) by GOBRD14: 34;

      then ( LeftComp f) is_a_component_of (( L~ f) ` ) by JORDAN2C:def 3;

      then

       A4: ( UBD ( L~ f)) is_a_component_of (( L~ f) ` ) by GOBRD14: 36;

      reconsider X as connected Subset of ( TOP-REAL 2) by A2;

      

       A5: C c= ( BDD ( L~ f)) & p in X by JORDAN10: 12;

      ( max (( E-bound ( L~ f)),(p `1 ))) >= (p `1 ) by XXREAL_0: 25;

      then (( max (( E-bound ( L~ f)),(p `1 ))) + 1) >= ((p `1 ) + 0 ) by XREAL_1: 7;

      then

       A6: ( |[(( max (( E-bound ( L~ f)),(p `1 ))) + 1), (p `2 )]| `1 ) >= (p `1 ) by EUCLID: 52;

      ( |[(( max (( E-bound ( L~ f)),(p `1 ))) + 1), (p `2 )]| `2 ) = (p `2 ) by EUCLID: 52;

      then |[(( max (( E-bound ( L~ f)),(p `1 ))) + 1), (p `2 )]| in X by A6;

      then

       A7: X meets ( UBD ( L~ f)) by A3, XBOOLE_0: 3;

      assume not thesis;

      then X c= (( L~ f) ` ) by A2, SUBSET_1: 23;

      then X c= ( UBD ( L~ f)) by A7, A4, GOBOARD9: 4;

      then p in (( BDD ( L~ f)) /\ ( UBD ( L~ f))) by A1, A5, XBOOLE_0:def 4;

      then ( BDD ( L~ f)) meets ( UBD ( L~ f));

      hence contradiction by JORDAN2C: 24;

    end;

    theorem :: JORDAN1A:53

    

     Th53: p in C implies ( south_halfline p) meets ( L~ ( Cage (C,n)))

    proof

      set f = ( Cage (C,n));

      assume

       A1: p in C;

      set X = { q where q be Point of ( TOP-REAL 2) : (q `1 ) = (p `1 ) & (q `2 ) <= (p `2 ) };

      

       A2: X = ( south_halfline p) by TOPREAL1: 34;

      (( min (( S-bound ( L~ f)),(p `2 ))) - 1) < (( S-bound ( L~ f)) - 0 ) by XREAL_1: 15, XXREAL_0: 17;

      then (f /. 1) = ( N-min ( L~ f)) & ( |[(p `1 ), (( min (( S-bound ( L~ f)),(p `2 ))) - 1)]| `2 ) < ( S-bound ( L~ f)) by EUCLID: 52, JORDAN9: 32;

      then |[(p `1 ), (( min (( S-bound ( L~ f)),(p `2 ))) - 1)]| in ( LeftComp f) by JORDAN2C: 112;

      then

       A3: |[(p `1 ), (( min (( S-bound ( L~ f)),(p `2 ))) - 1)]| in ( UBD ( L~ f)) by GOBRD14: 36;

      ( LeftComp f) is_outside_component_of ( L~ f) by GOBRD14: 34;

      then ( LeftComp f) is_a_component_of (( L~ f) ` ) by JORDAN2C:def 3;

      then

       A4: ( UBD ( L~ f)) is_a_component_of (( L~ f) ` ) by GOBRD14: 36;

      reconsider X as connected Subset of ( TOP-REAL 2) by A2;

      

       A5: C c= ( BDD ( L~ f)) & p in X by JORDAN10: 12;

      ( min (( S-bound ( L~ f)),(p `2 ))) <= (p `2 ) by XXREAL_0: 17;

      then (( min (( S-bound ( L~ f)),(p `2 ))) - 1) <= ((p `2 ) - 0 ) by XREAL_1: 13;

      then

       A6: ( |[(p `1 ), (( min (( S-bound ( L~ f)),(p `2 ))) - 1)]| `2 ) <= (p `2 ) by EUCLID: 52;

      ( |[(p `1 ), (( min (( S-bound ( L~ f)),(p `2 ))) - 1)]| `1 ) = (p `1 ) by EUCLID: 52;

      then |[(p `1 ), (( min (( S-bound ( L~ f)),(p `2 ))) - 1)]| in X by A6;

      then

       A7: X meets ( UBD ( L~ f)) by A3, XBOOLE_0: 3;

      assume not thesis;

      then X c= (( L~ f) ` ) by A2, SUBSET_1: 23;

      then X c= ( UBD ( L~ f)) by A7, A4, GOBOARD9: 4;

      then p in (( BDD ( L~ f)) /\ ( UBD ( L~ f))) by A1, A5, XBOOLE_0:def 4;

      then ( BDD ( L~ f)) meets ( UBD ( L~ f));

      hence contradiction by JORDAN2C: 24;

    end;

    theorem :: JORDAN1A:54

    

     Th54: p in C implies ( west_halfline p) meets ( L~ ( Cage (C,n)))

    proof

      set f = ( Cage (C,n));

      assume

       A1: p in C;

      set X = { q where q be Point of ( TOP-REAL 2) : (q `1 ) <= (p `1 ) & (q `2 ) = (p `2 ) };

      

       A2: X = ( west_halfline p) by TOPREAL1: 36;

      (( min (( W-bound ( L~ f)),(p `1 ))) - 1) < (( W-bound ( L~ f)) - 0 ) by XREAL_1: 15, XXREAL_0: 17;

      then (f /. 1) = ( N-min ( L~ f)) & ( |[(( min (( W-bound ( L~ f)),(p `1 ))) - 1), (p `2 )]| `1 ) < ( W-bound ( L~ f)) by EUCLID: 52, JORDAN9: 32;

      then |[(( min (( W-bound ( L~ f)),(p `1 ))) - 1), (p `2 )]| in ( LeftComp f) by JORDAN2C: 110;

      then

       A3: |[(( min (( W-bound ( L~ f)),(p `1 ))) - 1), (p `2 )]| in ( UBD ( L~ f)) by GOBRD14: 36;

      ( LeftComp f) is_outside_component_of ( L~ f) by GOBRD14: 34;

      then ( LeftComp f) is_a_component_of (( L~ f) ` ) by JORDAN2C:def 3;

      then

       A4: ( UBD ( L~ f)) is_a_component_of (( L~ f) ` ) by GOBRD14: 36;

      reconsider X as connected Subset of ( TOP-REAL 2) by A2;

      

       A5: C c= ( BDD ( L~ f)) & p in X by JORDAN10: 12;

      ( min (( W-bound ( L~ f)),(p `1 ))) <= (p `1 ) by XXREAL_0: 17;

      then (( min (( W-bound ( L~ f)),(p `1 ))) - 1) <= ((p `1 ) - 0 ) by XREAL_1: 13;

      then

       A6: ( |[(( min (( W-bound ( L~ f)),(p `1 ))) - 1), (p `2 )]| `1 ) <= (p `1 ) by EUCLID: 52;

      ( |[(( min (( W-bound ( L~ f)),(p `1 ))) - 1), (p `2 )]| `2 ) = (p `2 ) by EUCLID: 52;

      then |[(( min (( W-bound ( L~ f)),(p `1 ))) - 1), (p `2 )]| in X by A6;

      then

       A7: X meets ( UBD ( L~ f)) by A3, XBOOLE_0: 3;

      assume not thesis;

      then X c= (( L~ f) ` ) by A2, SUBSET_1: 23;

      then X c= ( UBD ( L~ f)) by A7, A4, GOBOARD9: 4;

      then p in (( BDD ( L~ f)) /\ ( UBD ( L~ f))) by A1, A5, XBOOLE_0:def 4;

      then ( BDD ( L~ f)) meets ( UBD ( L~ f));

      hence contradiction by JORDAN2C: 24;

    end;

    

     Lm15: ex k, t st 1 <= k & k <= ( len ( Cage (C,n))) & 1 <= t & t <= ( width ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (1,t))

    proof

      consider x be object such that

       A1: x in ( W-most C) by XBOOLE_0:def 1;

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

      

       A2: x in C by A1, XBOOLE_0:def 4;

      set X = { q where q be Point of ( TOP-REAL 2) : (q `1 ) <= (x `1 ) & (q `2 ) = (x `2 ) };

      

       A3: X = ( west_halfline x) by TOPREAL1: 36;

      then

      reconsider X as connected Subset of ( TOP-REAL 2);

      assume

       A4: for k,t be Nat st 1 <= k & k <= ( len ( Cage (C,n))) & 1 <= t & t <= ( width ( Gauge (C,n))) holds (( Cage (C,n)) /. k) <> (( Gauge (C,n)) * (1,t));

       A5:

      now

        ( west_halfline x) meets ( L~ ( Cage (C,n))) by A2, Th54;

        then

        consider y be object such that

         A6: y in X and

         A7: y in ( L~ ( Cage (C,n))) by A3, XBOOLE_0: 3;

        reconsider y as Point of ( TOP-REAL 2) by A6;

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

         A8: y = q and

         A9: (q `1 ) <= (x `1 ) and

         A10: (q `2 ) = (x `2 ) by A6;

        consider i be Nat such that

         A11: 1 <= i and

         A12: (i + 1) <= ( len ( Cage (C,n))) and

         A13: y in ( LSeg (( Cage (C,n)),i)) by A7, SPPOL_2: 13;

        

         A14: (q `1 ) < (x `1 )

        proof

          assume (q `1 ) >= (x `1 );

          then (q `1 ) = (x `1 ) by A9, XXREAL_0: 1;

          then q = x by A10, TOPREAL3: 6;

          then x in (C /\ ( L~ ( Cage (C,n)))) by A2, A7, A8, XBOOLE_0:def 4;

          then C meets ( L~ ( Cage (C,n)));

          hence contradiction by JORDAN10: 5;

        end;

        

         A15: y in ( LSeg ((( Cage (C,n)) /. i),(( Cage (C,n)) /. (i + 1)))) by A11, A12, A13, TOPREAL1:def 3;

        now

          per cases ;

            suppose ((( Cage (C,n)) /. i) `1 ) <= ((( Cage (C,n)) /. (i + 1)) `1 );

            then ((( Cage (C,n)) /. i) `1 ) <= (q `1 ) by A8, A15, TOPREAL1: 3;

            then

             A16: ((( Cage (C,n)) /. i) `1 ) < (x `1 ) by A14, XXREAL_0: 2;

            

             A17: ( Cage (C,n)) is_sequence_on ( Gauge (C,n)) by JORDAN9:def 1;

            

             A18: i < ( len ( Cage (C,n))) by A12, NAT_1: 13;

            then i in ( Seg ( len ( Cage (C,n)))) by A11, FINSEQ_1: 1;

            then i in ( dom ( Cage (C,n))) by FINSEQ_1:def 3;

            then

            consider i1,i2 be Nat such that

             A19: [i1, i2] in ( Indices ( Gauge (C,n))) and

             A20: (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (i1,i2)) by A17, GOBOARD1:def 9;

            

             A21: 1 <= i2 by A19, MATRIX_0: 32;

            

             A22: i1 <= ( len ( Gauge (C,n))) by A19, MATRIX_0: 32;

            

             A23: 1 <= i1 by A19, MATRIX_0: 32;

            

             A24: i2 <= ( width ( Gauge (C,n))) by A19, MATRIX_0: 32;

            then

             A25: i2 <= ( len ( Gauge (C,n))) by JORDAN8:def 1;

            (x `1 ) = (( W-min C) `1 ) by A1, PSCOMP_1: 31

            .= ( W-bound C) by EUCLID: 52

            .= ((( Gauge (C,n)) * (2,i2)) `1 ) by A21, A25, JORDAN8: 11;

            then i1 < (1 + 1) by A16, A20, A21, A24, A22, SPRECT_3: 13;

            then i1 <= 1 by NAT_1: 13;

            then (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (1,i2)) by A20, A23, XXREAL_0: 1;

            hence x in ( UBD ( L~ ( Cage (C,n)))) by A4, A11, A18, A21, A24;

          end;

            suppose ((( Cage (C,n)) /. i) `1 ) >= ((( Cage (C,n)) /. (i + 1)) `1 );

            then (q `1 ) >= ((( Cage (C,n)) /. (i + 1)) `1 ) by A8, A15, TOPREAL1: 3;

            then

             A26: ((( Cage (C,n)) /. (i + 1)) `1 ) < (x `1 ) by A14, XXREAL_0: 2;

            

             A27: ( Cage (C,n)) is_sequence_on ( Gauge (C,n)) by JORDAN9:def 1;

            

             A28: (i + 1) >= 1 by NAT_1: 11;

            then (i + 1) in ( Seg ( len ( Cage (C,n)))) by A12, FINSEQ_1: 1;

            then (i + 1) in ( dom ( Cage (C,n))) by FINSEQ_1:def 3;

            then

            consider i1,i2 be Nat such that

             A29: [i1, i2] in ( Indices ( Gauge (C,n))) and

             A30: (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (i1,i2)) by A27, GOBOARD1:def 9;

            

             A31: 1 <= i2 by A29, MATRIX_0: 32;

            

             A32: i1 <= ( len ( Gauge (C,n))) by A29, MATRIX_0: 32;

            

             A33: 1 <= i1 by A29, MATRIX_0: 32;

            

             A34: i2 <= ( width ( Gauge (C,n))) by A29, MATRIX_0: 32;

            then

             A35: i2 <= ( len ( Gauge (C,n))) by JORDAN8:def 1;

            (x `1 ) = (( W-min C) `1 ) by A1, PSCOMP_1: 31

            .= ( W-bound C) by EUCLID: 52

            .= ((( Gauge (C,n)) * (2,i2)) `1 ) by A31, A35, JORDAN8: 11;

            then i1 < (1 + 1) by A26, A30, A31, A34, A32, SPRECT_3: 13;

            then i1 <= 1 by NAT_1: 13;

            then (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (1,i2)) by A30, A33, XXREAL_0: 1;

            hence x in ( UBD ( L~ ( Cage (C,n)))) by A4, A12, A28, A31, A34;

          end;

        end;

        hence x in ( UBD ( L~ ( Cage (C,n))));

      end;

      C c= ( BDD ( L~ ( Cage (C,n)))) by JORDAN10: 12;

      then x in (( BDD ( L~ ( Cage (C,n)))) /\ ( UBD ( L~ ( Cage (C,n))))) by A2, A5, XBOOLE_0:def 4;

      then ( BDD ( L~ ( Cage (C,n)))) meets ( UBD ( L~ ( Cage (C,n))));

      hence contradiction by JORDAN2C: 24;

    end;

    

     Lm16: ex k, t st 1 <= k & k <= ( len ( Cage (C,n))) & 1 <= t & t <= ( len ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (t,1))

    proof

      consider x be object such that

       A1: x in ( S-most C) by XBOOLE_0:def 1;

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

      

       A2: x in C by A1, XBOOLE_0:def 4;

      set X = { q where q be Point of ( TOP-REAL 2) : (q `1 ) = (x `1 ) & (q `2 ) <= (x `2 ) };

      

       A3: X = ( south_halfline x) by TOPREAL1: 34;

      then

      reconsider X as connected Subset of ( TOP-REAL 2);

      assume

       A4: for k,t be Nat st 1 <= k & k <= ( len ( Cage (C,n))) & 1 <= t & t <= ( len ( Gauge (C,n))) holds (( Cage (C,n)) /. k) <> (( Gauge (C,n)) * (t,1));

       A5:

      now

        ( south_halfline x) meets ( L~ ( Cage (C,n))) by A2, Th53;

        then

        consider y be object such that

         A6: y in X and

         A7: y in ( L~ ( Cage (C,n))) by A3, XBOOLE_0: 3;

        reconsider y as Point of ( TOP-REAL 2) by A6;

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

         A8: y = q and

         A9: (q `1 ) = (x `1 ) and

         A10: (q `2 ) <= (x `2 ) by A6;

        consider i be Nat such that

         A11: 1 <= i and

         A12: (i + 1) <= ( len ( Cage (C,n))) and

         A13: y in ( LSeg (( Cage (C,n)),i)) by A7, SPPOL_2: 13;

        

         A14: (q `2 ) < (x `2 )

        proof

          assume (q `2 ) >= (x `2 );

          then (q `2 ) = (x `2 ) by A10, XXREAL_0: 1;

          then q = x by A9, TOPREAL3: 6;

          then x in (C /\ ( L~ ( Cage (C,n)))) by A2, A7, A8, XBOOLE_0:def 4;

          then C meets ( L~ ( Cage (C,n)));

          hence contradiction by JORDAN10: 5;

        end;

        

         A15: y in ( LSeg ((( Cage (C,n)) /. i),(( Cage (C,n)) /. (i + 1)))) by A11, A12, A13, TOPREAL1:def 3;

        now

          per cases ;

            suppose ((( Cage (C,n)) /. i) `2 ) <= ((( Cage (C,n)) /. (i + 1)) `2 );

            then ((( Cage (C,n)) /. i) `2 ) <= (q `2 ) by A8, A15, TOPREAL1: 4;

            then

             A16: ((( Cage (C,n)) /. i) `2 ) < (x `2 ) by A14, XXREAL_0: 2;

            

             A17: ( Cage (C,n)) is_sequence_on ( Gauge (C,n)) by JORDAN9:def 1;

            

             A18: i < ( len ( Cage (C,n))) by A12, NAT_1: 13;

            then i in ( Seg ( len ( Cage (C,n)))) by A11, FINSEQ_1: 1;

            then i in ( dom ( Cage (C,n))) by FINSEQ_1:def 3;

            then

            consider i1,i2 be Nat such that

             A19: [i1, i2] in ( Indices ( Gauge (C,n))) and

             A20: (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (i1,i2)) by A17, GOBOARD1:def 9;

            

             A21: 1 <= i2 by A19, MATRIX_0: 32;

            

             A22: i2 <= ( width ( Gauge (C,n))) by A19, MATRIX_0: 32;

            

             A23: 1 <= i1 & i1 <= ( len ( Gauge (C,n))) by A19, MATRIX_0: 32;

            (x `2 ) = (( S-min C) `2 ) by A1, PSCOMP_1: 55

            .= ( S-bound C) by EUCLID: 52

            .= ((( Gauge (C,n)) * (i1,2)) `2 ) by A23, JORDAN8: 13;

            then i2 < (1 + 1) by A16, A20, A22, A23, SPRECT_3: 12;

            then i2 <= 1 by NAT_1: 13;

            then (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (i1,1)) by A20, A21, XXREAL_0: 1;

            hence x in ( UBD ( L~ ( Cage (C,n)))) by A4, A11, A18, A23;

          end;

            suppose ((( Cage (C,n)) /. i) `2 ) >= ((( Cage (C,n)) /. (i + 1)) `2 );

            then (q `2 ) >= ((( Cage (C,n)) /. (i + 1)) `2 ) by A8, A15, TOPREAL1: 4;

            then

             A24: ((( Cage (C,n)) /. (i + 1)) `2 ) < (x `2 ) by A14, XXREAL_0: 2;

            

             A25: ( Cage (C,n)) is_sequence_on ( Gauge (C,n)) by JORDAN9:def 1;

            

             A26: (i + 1) >= 1 by NAT_1: 11;

            then (i + 1) in ( Seg ( len ( Cage (C,n)))) by A12, FINSEQ_1: 1;

            then (i + 1) in ( dom ( Cage (C,n))) by FINSEQ_1:def 3;

            then

            consider i1,i2 be Nat such that

             A27: [i1, i2] in ( Indices ( Gauge (C,n))) and

             A28: (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (i1,i2)) by A25, GOBOARD1:def 9;

            

             A29: 1 <= i2 by A27, MATRIX_0: 32;

            

             A30: i2 <= ( width ( Gauge (C,n))) by A27, MATRIX_0: 32;

            

             A31: 1 <= i1 & i1 <= ( len ( Gauge (C,n))) by A27, MATRIX_0: 32;

            (x `2 ) = (( S-min C) `2 ) by A1, PSCOMP_1: 55

            .= ( S-bound C) by EUCLID: 52

            .= ((( Gauge (C,n)) * (i1,2)) `2 ) by A31, JORDAN8: 13;

            then i2 < (1 + 1) by A24, A28, A30, A31, SPRECT_3: 12;

            then i2 <= 1 by NAT_1: 13;

            then (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (i1,1)) by A28, A29, XXREAL_0: 1;

            hence x in ( UBD ( L~ ( Cage (C,n)))) by A4, A12, A26, A31;

          end;

        end;

        hence x in ( UBD ( L~ ( Cage (C,n))));

      end;

      C c= ( BDD ( L~ ( Cage (C,n)))) by JORDAN10: 12;

      then x in (( BDD ( L~ ( Cage (C,n)))) /\ ( UBD ( L~ ( Cage (C,n))))) by A2, A5, XBOOLE_0:def 4;

      then ( BDD ( L~ ( Cage (C,n)))) meets ( UBD ( L~ ( Cage (C,n))));

      hence contradiction by JORDAN2C: 24;

    end;

    

     Lm17: ex k, t st 1 <= k & k <= ( len ( Cage (C,n))) & 1 <= t & t <= ( width ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (( len ( Gauge (C,n))),t))

    proof

      consider x be object such that

       A1: x in ( E-most C) by XBOOLE_0:def 1;

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

      

       A2: x in C by A1, XBOOLE_0:def 4;

      set X = { q where q be Point of ( TOP-REAL 2) : (q `1 ) >= (x `1 ) & (q `2 ) = (x `2 ) };

      

       A3: X = ( east_halfline x) by TOPREAL1: 32;

      then

      reconsider X as connected Subset of ( TOP-REAL 2);

      assume

       A4: for k,t be Nat st 1 <= k & k <= ( len ( Cage (C,n))) & 1 <= t & t <= ( width ( Gauge (C,n))) holds (( Cage (C,n)) /. k) <> (( Gauge (C,n)) * (( len ( Gauge (C,n))),t));

       A5:

      now

        ( east_halfline x) meets ( L~ ( Cage (C,n))) by A2, Th52;

        then

        consider y be object such that

         A6: y in X and

         A7: y in ( L~ ( Cage (C,n))) by A3, XBOOLE_0: 3;

        reconsider y as Point of ( TOP-REAL 2) by A6;

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

         A8: y = q and

         A9: (q `1 ) >= (x `1 ) and

         A10: (q `2 ) = (x `2 ) by A6;

        consider i be Nat such that

         A11: 1 <= i and

         A12: (i + 1) <= ( len ( Cage (C,n))) and

         A13: y in ( LSeg (( Cage (C,n)),i)) by A7, SPPOL_2: 13;

        

         A14: y in ( LSeg ((( Cage (C,n)) /. i),(( Cage (C,n)) /. (i + 1)))) by A11, A12, A13, TOPREAL1:def 3;

        

         A15: (q `1 ) > (x `1 )

        proof

          assume (q `1 ) <= (x `1 );

          then (q `1 ) = (x `1 ) by A9, XXREAL_0: 1;

          then q = x by A10, TOPREAL3: 6;

          then x in (C /\ ( L~ ( Cage (C,n)))) by A2, A7, A8, XBOOLE_0:def 4;

          then C meets ( L~ ( Cage (C,n)));

          hence contradiction by JORDAN10: 5;

        end;

        

         A16: ( Cage (C,n)) is_sequence_on ( Gauge (C,n)) by JORDAN9:def 1;

        

         A17: ( Cage (C,n)) is_sequence_on ( Gauge (C,n)) by JORDAN9:def 1;

        

         A18: 4 <= ( len ( Gauge (C,n))) by JORDAN8: 10;

        

         A19: 1 <= (i + 1) by A11, NAT_1: 13;

        then (i + 1) in ( Seg ( len ( Cage (C,n)))) by A12, FINSEQ_1: 1;

        then (i + 1) in ( dom ( Cage (C,n))) by FINSEQ_1:def 3;

        then

        consider l1,l2 be Nat such that

         A20: [l1, l2] in ( Indices ( Gauge (C,n))) and

         A21: (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (l1,l2)) by A16, GOBOARD1:def 9;

        

         A22: 1 <= l2 by A20, MATRIX_0: 32;

        

         A23: l2 <= ( width ( Gauge (C,n))) by A20, MATRIX_0: 32;

        then

         A24: l2 <= ( len ( Gauge (C,n))) by JORDAN8:def 1;

        

         A25: (x `1 ) = (( E-min C) `1 ) by A1, PSCOMP_1: 47

        .= ( E-bound C) by EUCLID: 52

        .= ((( Gauge (C,n)) * ((( len ( Gauge (C,n))) -' 1),l2)) `1 ) by A22, A24, JORDAN8: 12;

        

         A26: l1 <= ( len ( Gauge (C,n))) by A20, MATRIX_0: 32;

        

         A27: 1 <= l1 by A20, MATRIX_0: 32;

        

         A28: (( len ( Gauge (C,n))) -' 1) <= ( len ( Gauge (C,n))) by NAT_D: 35;

        

         A29: i < ( len ( Cage (C,n))) by A12, NAT_1: 13;

        then i in ( Seg ( len ( Cage (C,n)))) by A11, FINSEQ_1: 1;

        then i in ( dom ( Cage (C,n))) by FINSEQ_1:def 3;

        then

        consider i1,i2 be Nat such that

         A30: [i1, i2] in ( Indices ( Gauge (C,n))) and

         A31: (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (i1,i2)) by A17, GOBOARD1:def 9;

        

         A32: 1 <= i2 by A30, MATRIX_0: 32;

        

         A33: i1 <= ( len ( Gauge (C,n))) by A30, MATRIX_0: 32;

        

         A34: 1 <= i1 by A30, MATRIX_0: 32;

        

         A35: i2 <= ( width ( Gauge (C,n))) by A30, MATRIX_0: 32;

        then

         A36: i2 <= ( len ( Gauge (C,n))) by JORDAN8:def 1;

        

         A37: (x `1 ) = (( E-min C) `1 ) by A1, PSCOMP_1: 47

        .= ( E-bound C) by EUCLID: 52

        .= ((( Gauge (C,n)) * ((( len ( Gauge (C,n))) -' 1),i2)) `1 ) by A32, A36, JORDAN8: 12;

        now

          per cases ;

            suppose ((( Cage (C,n)) /. i) `1 ) >= ((( Cage (C,n)) /. (i + 1)) `1 );

            then ((( Cage (C,n)) /. i) `1 ) >= (q `1 ) by A8, A14, TOPREAL1: 3;

            then ((( Cage (C,n)) /. i) `1 ) > (x `1 ) by A15, XXREAL_0: 2;

            then i1 > (( len ( Gauge (C,n))) -' 1) by A31, A32, A35, A34, A37, A28, SPRECT_3: 13;

            then i1 >= ((( len ( Gauge (C,n))) -' 1) + 1) by NAT_1: 13;

            then i1 >= ( len ( Gauge (C,n))) by A18, XREAL_1: 235, XXREAL_0: 2;

            then (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (( len ( Gauge (C,n))),i2)) by A31, A33, XXREAL_0: 1;

            hence contradiction by A4, A11, A29, A32, A35;

          end;

            suppose ((( Cage (C,n)) /. i) `1 ) <= ((( Cage (C,n)) /. (i + 1)) `1 );

            then (q `1 ) <= ((( Cage (C,n)) /. (i + 1)) `1 ) by A8, A14, TOPREAL1: 3;

            then ((( Cage (C,n)) /. (i + 1)) `1 ) > (x `1 ) by A15, XXREAL_0: 2;

            then l1 > (( len ( Gauge (C,n))) -' 1) by A21, A22, A23, A27, A25, A28, SPRECT_3: 13;

            then l1 >= ((( len ( Gauge (C,n))) -' 1) + 1) by NAT_1: 13;

            then l1 >= ( len ( Gauge (C,n))) by A18, XREAL_1: 235, XXREAL_0: 2;

            then (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (( len ( Gauge (C,n))),l2)) by A21, A26, XXREAL_0: 1;

            hence contradiction by A4, A12, A19, A22, A23;

          end;

        end;

        hence x in ( UBD ( L~ ( Cage (C,n))));

      end;

      C c= ( BDD ( L~ ( Cage (C,n)))) by JORDAN10: 12;

      then x in (( BDD ( L~ ( Cage (C,n)))) /\ ( UBD ( L~ ( Cage (C,n))))) by A2, A5, XBOOLE_0:def 4;

      then ( BDD ( L~ ( Cage (C,n)))) meets ( UBD ( L~ ( Cage (C,n))));

      hence contradiction by JORDAN2C: 24;

    end;

    theorem :: JORDAN1A:55

    

     Th55: ex k, t st 1 <= k & k < ( len ( Cage (C,n))) & 1 <= t & t <= ( width ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (1,t))

    proof

      consider k, t such that

       A1: 1 <= k and

       A2: k <= ( len ( Cage (C,n))) and

       A3: 1 <= t & t <= ( width ( Gauge (C,n))) and

       A4: (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (1,t)) by Lm15;

      per cases by A2, XXREAL_0: 1;

        suppose k < ( len ( Cage (C,n)));

        hence thesis by A1, A3, A4;

      end;

        suppose

         A5: k = ( len ( Cage (C,n)));

        take 1, t;

        thus 1 <= 1 & 1 < ( len ( Cage (C,n))) by GOBOARD7: 34, XXREAL_0: 2;

        thus 1 <= t & t <= ( width ( Gauge (C,n))) by A3;

        thus thesis by A4, A5, FINSEQ_6:def 1;

      end;

    end;

    theorem :: JORDAN1A:56

    

     Th56: ex k, t st 1 <= k & k < ( len ( Cage (C,n))) & 1 <= t & t <= ( len ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (t,1))

    proof

      consider k, t such that

       A1: 1 <= k and

       A2: k <= ( len ( Cage (C,n))) and

       A3: 1 <= t & t <= ( len ( Gauge (C,n))) and

       A4: (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (t,1)) by Lm16;

      per cases by A2, XXREAL_0: 1;

        suppose k < ( len ( Cage (C,n)));

        hence thesis by A1, A3, A4;

      end;

        suppose

         A5: k = ( len ( Cage (C,n)));

        take 1, t;

        thus 1 <= 1 & 1 < ( len ( Cage (C,n))) by GOBOARD7: 34, XXREAL_0: 2;

        thus 1 <= t & t <= ( len ( Gauge (C,n))) by A3;

        thus thesis by A4, A5, FINSEQ_6:def 1;

      end;

    end;

    theorem :: JORDAN1A:57

    

     Th57: ex k, t st 1 <= k & k < ( len ( Cage (C,n))) & 1 <= t & t <= ( width ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (( len ( Gauge (C,n))),t))

    proof

      consider k, t such that

       A1: 1 <= k and

       A2: k <= ( len ( Cage (C,n))) and

       A3: 1 <= t & t <= ( width ( Gauge (C,n))) and

       A4: (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (( len ( Gauge (C,n))),t)) by Lm17;

      per cases by A2, XXREAL_0: 1;

        suppose k < ( len ( Cage (C,n)));

        hence thesis by A1, A3, A4;

      end;

        suppose

         A5: k = ( len ( Cage (C,n)));

        take 1, t;

        thus 1 <= 1 & 1 < ( len ( Cage (C,n))) by GOBOARD7: 34, XXREAL_0: 2;

        thus 1 <= t & t <= ( width ( Gauge (C,n))) by A3;

        thus thesis by A4, A5, FINSEQ_6:def 1;

      end;

    end;

    theorem :: JORDAN1A:58

    

     Th58: 1 <= k & k <= ( len ( Cage (C,n))) & 1 <= t & t <= ( len ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (t,( width ( Gauge (C,n))))) implies (( Cage (C,n)) /. k) in ( N-most ( L~ ( Cage (C,n))))

    proof

      assume that

       A1: 1 <= k & k <= ( len ( Cage (C,n))) and

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

       A3: (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (t,( width ( Gauge (C,n)))));

      ( Cage (C,n)) is_sequence_on ( Gauge (C,n)) by JORDAN9:def 1;

      then

       A4: ((( Gauge (C,n)) * (t,( width ( Gauge (C,n))))) `2 ) >= ( N-bound ( L~ ( Cage (C,n)))) by A2, Th20;

      ( len ( Cage (C,n))) >= 2 by GOBOARD7: 34, XXREAL_0: 2;

      then

       A5: (( Cage (C,n)) /. k) in ( L~ ( Cage (C,n))) by A1, TOPREAL3: 39;

      then ( N-bound ( L~ ( Cage (C,n)))) >= ((( Cage (C,n)) /. k) `2 ) by PSCOMP_1: 24;

      hence thesis by A3, A5, A4, SPRECT_2: 10, XXREAL_0: 1;

    end;

    theorem :: JORDAN1A:59

    

     Th59: 1 <= k & k <= ( len ( Cage (C,n))) & 1 <= t & t <= ( width ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (1,t)) implies (( Cage (C,n)) /. k) in ( W-most ( L~ ( Cage (C,n))))

    proof

      assume that

       A1: 1 <= k & k <= ( len ( Cage (C,n))) and

       A2: 1 <= t & t <= ( width ( Gauge (C,n))) and

       A3: (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (1,t));

      ( Cage (C,n)) is_sequence_on ( Gauge (C,n)) by JORDAN9:def 1;

      then

       A4: ((( Gauge (C,n)) * (1,t)) `1 ) <= ( W-bound ( L~ ( Cage (C,n)))) by A2, Th21;

      ( len ( Cage (C,n))) >= 2 by GOBOARD7: 34, XXREAL_0: 2;

      then

       A5: (( Cage (C,n)) /. k) in ( L~ ( Cage (C,n))) by A1, TOPREAL3: 39;

      then ( W-bound ( L~ ( Cage (C,n)))) <= ((( Cage (C,n)) /. k) `1 ) by PSCOMP_1: 24;

      hence thesis by A3, A5, A4, SPRECT_2: 12, XXREAL_0: 1;

    end;

    theorem :: JORDAN1A:60

    

     Th60: 1 <= k & k <= ( len ( Cage (C,n))) & 1 <= t & t <= ( len ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (t,1)) implies (( Cage (C,n)) /. k) in ( S-most ( L~ ( Cage (C,n))))

    proof

      assume that

       A1: 1 <= k & k <= ( len ( Cage (C,n))) and

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

       A3: (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (t,1));

      ( Cage (C,n)) is_sequence_on ( Gauge (C,n)) by JORDAN9:def 1;

      then

       A4: ((( Gauge (C,n)) * (t,1)) `2 ) <= ( S-bound ( L~ ( Cage (C,n)))) by A2, Th22;

      ( len ( Cage (C,n))) >= 2 by GOBOARD7: 34, XXREAL_0: 2;

      then

       A5: (( Cage (C,n)) /. k) in ( L~ ( Cage (C,n))) by A1, TOPREAL3: 39;

      then ( S-bound ( L~ ( Cage (C,n)))) <= ((( Cage (C,n)) /. k) `2 ) by PSCOMP_1: 24;

      hence thesis by A3, A5, A4, SPRECT_2: 11, XXREAL_0: 1;

    end;

    theorem :: JORDAN1A:61

    

     Th61: 1 <= k & k <= ( len ( Cage (C,n))) & 1 <= t & t <= ( width ( Gauge (C,n))) & (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (( len ( Gauge (C,n))),t)) implies (( Cage (C,n)) /. k) in ( E-most ( L~ ( Cage (C,n))))

    proof

      assume that

       A1: 1 <= k & k <= ( len ( Cage (C,n))) and

       A2: 1 <= t & t <= ( width ( Gauge (C,n))) and

       A3: (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (( len ( Gauge (C,n))),t));

      ( Cage (C,n)) is_sequence_on ( Gauge (C,n)) by JORDAN9:def 1;

      then

       A4: ((( Gauge (C,n)) * (( len ( Gauge (C,n))),t)) `1 ) >= ( E-bound ( L~ ( Cage (C,n)))) by A2, Th23;

      ( len ( Cage (C,n))) >= 2 by GOBOARD7: 34, XXREAL_0: 2;

      then

       A5: (( Cage (C,n)) /. k) in ( L~ ( Cage (C,n))) by A1, TOPREAL3: 39;

      then ( E-bound ( L~ ( Cage (C,n)))) >= ((( Cage (C,n)) /. k) `1 ) by PSCOMP_1: 24;

      hence thesis by A3, A5, A4, SPRECT_2: 13, XXREAL_0: 1;

    end;

    theorem :: JORDAN1A:62

    

     Th62: ( W-bound ( L~ ( Cage (C,n)))) = (( W-bound C) - ((( E-bound C) - ( W-bound C)) / (2 |^ n)))

    proof

      set a = ( N-bound C), s = ( S-bound C), w = ( W-bound C), e = ( E-bound C), f = ( Cage (C,n)), G = ( Gauge (C,n));

      consider p,q be Nat such that

       A1: 1 <= p & p < ( len f) and

       A2: 1 <= q & q <= ( width G) and

       A3: (f /. p) = (G * (1,q)) by Th55;

      (f /. p) in ( W-most ( L~ f)) by A1, A2, A3, Th59;

      then

       A4: ((f /. p) `1 ) = (( W-min ( L~ f)) `1 ) by PSCOMP_1: 31;

      4 <= ( len G) by JORDAN8: 10;

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

      then

       A5: [1, q] in ( Indices G) by A2, MATRIX_0: 30;

      

      thus ( W-bound ( L~ f)) = (( W-min ( L~ f)) `1 ) by EUCLID: 52

      .= ( |[(w + (((e - w) / (2 |^ n)) * (1 - 2))), (s + (((a - s) / (2 |^ n)) * (q - 2)))]| `1 ) by A3, A4, A5, JORDAN8:def 1

      .= (w - ((e - w) / (2 |^ n))) by EUCLID: 52;

    end;

    theorem :: JORDAN1A:63

    

     Th63: ( S-bound ( L~ ( Cage (C,n)))) = (( S-bound C) - ((( N-bound C) - ( S-bound C)) / (2 |^ n)))

    proof

      set a = ( N-bound C), s = ( S-bound C), w = ( W-bound C), e = ( E-bound C), f = ( Cage (C,n)), G = ( Gauge (C,n));

      consider p,q be Nat such that

       A1: 1 <= p & p < ( len f) and

       A2: 1 <= q & q <= ( len G) and

       A3: (f /. p) = (G * (q,1)) by Th56;

      (f /. p) in ( S-most ( L~ f)) by A1, A2, A3, Th60;

      then

       A4: ((f /. p) `2 ) = (( S-min ( L~ f)) `2 ) by PSCOMP_1: 55;

      4 <= ( len G) by JORDAN8: 10;

      then ( len G) = ( width G) & 1 <= ( len G) by JORDAN8:def 1, XXREAL_0: 2;

      then

       A5: [q, 1] in ( Indices G) by A2, MATRIX_0: 30;

      

      thus ( S-bound ( L~ f)) = (( S-min ( L~ f)) `2 ) by EUCLID: 52

      .= ( |[(w + (((e - w) / (2 |^ n)) * (q - 2))), (s + (((a - s) / (2 |^ n)) * (1 - 2)))]| `2 ) by A3, A4, A5, JORDAN8:def 1

      .= (s - ((a - s) / (2 |^ n))) by EUCLID: 52;

    end;

    theorem :: JORDAN1A:64

    

     Th64: ( E-bound ( L~ ( Cage (C,n)))) = (( E-bound C) + ((( E-bound C) - ( W-bound C)) / (2 |^ n)))

    proof

      set a = ( N-bound C), s = ( S-bound C), w = ( W-bound C), e = ( E-bound C), f = ( Cage (C,n)), G = ( Gauge (C,n));

      consider p,q be Nat such that

       A1: 1 <= p & p < ( len f) and

       A2: 1 <= q & q <= ( width G) and

       A3: (f /. p) = (G * (( len G),q)) by Th57;

      (f /. p) in ( E-most ( L~ f)) by A1, A2, A3, Th61;

      then

       A4: ((f /. p) `1 ) = (( E-min ( L~ f)) `1 ) by PSCOMP_1: 47;

      4 <= ( len G) by JORDAN8: 10;

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

      then

       A5: [( len G), q] in ( Indices G) by A2, MATRIX_0: 30;

      

      thus ( E-bound ( L~ f)) = (( E-min ( L~ f)) `1 ) by EUCLID: 52

      .= ( |[(w + (((e - w) / (2 |^ n)) * (( len G) - 2))), (s + (((a - s) / (2 |^ n)) * (q - 2)))]| `1 ) by A3, A4, A5, JORDAN8:def 1

      .= (w + (((e - w) / (2 |^ n)) * (( len G) - 2))) by EUCLID: 52

      .= (e + ((e - w) / (2 |^ n))) by Lm10;

    end;

    theorem :: JORDAN1A:65

    (( N-bound ( L~ ( Cage (C,n)))) + ( S-bound ( L~ ( Cage (C,n))))) = (( N-bound ( L~ ( Cage (C,m)))) + ( S-bound ( L~ ( Cage (C,m)))))

    proof

      

      thus (( N-bound ( L~ ( Cage (C,n)))) + ( S-bound ( L~ ( Cage (C,n))))) = ((( N-bound C) + ((( N-bound C) - ( S-bound C)) / (2 |^ n))) + ( S-bound ( L~ ( Cage (C,n))))) by JORDAN10: 6

      .= ((( N-bound C) + ((( N-bound C) - ( S-bound C)) / (2 |^ n))) + (( S-bound C) - ((( N-bound C) - ( S-bound C)) / (2 |^ n)))) by Th63

      .= ((( N-bound C) + ((( N-bound C) - ( S-bound C)) / (2 |^ m))) + (( S-bound C) - ((( N-bound C) - ( S-bound C)) / (2 |^ m))))

      .= ((( N-bound C) + ((( N-bound C) - ( S-bound C)) / (2 |^ m))) + ( S-bound ( L~ ( Cage (C,m))))) by Th63

      .= (( N-bound ( L~ ( Cage (C,m)))) + ( S-bound ( L~ ( Cage (C,m))))) by JORDAN10: 6;

    end;

    theorem :: JORDAN1A:66

    (( E-bound ( L~ ( Cage (C,n)))) + ( W-bound ( L~ ( Cage (C,n))))) = (( E-bound ( L~ ( Cage (C,m)))) + ( W-bound ( L~ ( Cage (C,m)))))

    proof

      

      thus (( E-bound ( L~ ( Cage (C,n)))) + ( W-bound ( L~ ( Cage (C,n))))) = ((( E-bound C) + ((( E-bound C) - ( W-bound C)) / (2 |^ n))) + ( W-bound ( L~ ( Cage (C,n))))) by Th64

      .= ((( E-bound C) + ((( E-bound C) - ( W-bound C)) / (2 |^ n))) + (( W-bound C) - ((( E-bound C) - ( W-bound C)) / (2 |^ n)))) by Th62

      .= ((( E-bound C) + ((( E-bound C) - ( W-bound C)) / (2 |^ m))) + (( W-bound C) - ((( E-bound C) - ( W-bound C)) / (2 |^ m))))

      .= ((( E-bound C) + ((( E-bound C) - ( W-bound C)) / (2 |^ m))) + ( W-bound ( L~ ( Cage (C,m))))) by Th62

      .= (( E-bound ( L~ ( Cage (C,m)))) + ( W-bound ( L~ ( Cage (C,m))))) by Th64;

    end;

    theorem :: JORDAN1A:67

    i < j implies ( E-bound ( L~ ( Cage (C,j)))) < ( E-bound ( L~ ( Cage (C,i))))

    proof

      assume

       A1: i < j;

      defpred P[ Nat] means i < $1 implies ( E-bound ( L~ ( Cage (C,$1)))) < ( E-bound ( L~ ( Cage (C,i))));

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A3: P[n];

        set j = (n + 1), a = ( E-bound C), s = ( W-bound C);

        

         A4: ((a + ((a - s) / (2 |^ j))) - (a + ((a - s) / (2 |^ n)))) = (( 0 + ((a - s) / (2 |^ j))) - ((a - s) / (2 |^ n)))

        .= (((a - s) / ((2 |^ n) * 2)) - (((a - s) / (2 |^ n)) / (2 / 2))) by NEWTON: 6

        .= (((a - s) / ((2 |^ n) * 2)) - (((a - s) * 2) / ((2 |^ n) * 2))) by XCMPLX_1: 84

        .= (((a - s) - ((2 * a) - (2 * s))) / ((2 |^ n) * 2)) by XCMPLX_1: 120

        .= ((s - a) / ((2 |^ n) * 2));

        (2 |^ n) > 0 by NEWTON: 83;

        then

         A5: ((2 |^ n) * 2) > ( 0 * 2) by XREAL_1: 68;

        

         A6: ( E-bound ( L~ ( Cage (C,n)))) = (a + ((a - s) / (2 |^ n))) & ( E-bound ( L~ ( Cage (C,j)))) = (a + ((a - s) / (2 |^ j))) by Th64;

        (s - a) < 0 by SPRECT_1: 31, XREAL_1: 49;

        then 0 > ((a + ((a - s) / (2 |^ j))) - (a + ((a - s) / (2 |^ n)))) by A5, A4, XREAL_1: 141;

        then

         A7: ( E-bound ( L~ ( Cage (C,j)))) < ( E-bound ( L~ ( Cage (C,n)))) by A6, XREAL_1: 48;

        assume i < (n + 1);

        then i <= n by NAT_1: 13;

        hence thesis by A3, A7, XXREAL_0: 1, XXREAL_0: 2;

      end;

      

       A8: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A8, A2);

      hence thesis by A1;

    end;

    theorem :: JORDAN1A:68

    i < j implies ( W-bound ( L~ ( Cage (C,i)))) < ( W-bound ( L~ ( Cage (C,j))))

    proof

      assume

       A1: i < j;

      defpred P[ Nat] means i < $1 implies ( W-bound ( L~ ( Cage (C,i)))) < ( W-bound ( L~ ( Cage (C,$1))));

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A3: P[n];

        set j = (n + 1), a = ( E-bound C), s = ( W-bound C);

        

         A4: ((s - ((a - s) / (2 |^ j))) - (s - ((a - s) / (2 |^ n)))) = (((s + ( - ((a - s) / (2 |^ j)))) - s) + ((a - s) / (2 |^ n)))

        .= (( - ((a - s) / ((2 |^ n) * 2))) + ((a - s) / (2 |^ n))) by NEWTON: 6

        .= ((( - (a - s)) / ((2 |^ n) * 2)) + ((a - s) / (2 |^ n))) by XCMPLX_1: 187

        .= ((( - (a - s)) / ((2 |^ n) * 2)) + (((a - s) * 2) / ((2 |^ n) * 2))) by XCMPLX_1: 91

        .= ((( - (a - s)) + ((a - s) * 2)) / ((2 |^ n) * 2)) by XCMPLX_1: 62

        .= ((a - s) / ((2 |^ n) * 2));

        (2 |^ n) > 0 by NEWTON: 83;

        then

         A5: ((2 |^ n) * 2) > ( 0 * 2) by XREAL_1: 68;

        

         A6: ( W-bound ( L~ ( Cage (C,n)))) = (s - ((a - s) / (2 |^ n))) & ( W-bound ( L~ ( Cage (C,j)))) = (s - ((a - s) / (2 |^ j))) by Th62;

        (a - s) > 0 by SPRECT_1: 31, XREAL_1: 50;

        then 0 < ((s - ((a - s) / (2 |^ j))) - (s - ((a - s) / (2 |^ n)))) by A5, A4, XREAL_1: 139;

        then

         A7: ( W-bound ( L~ ( Cage (C,n)))) < ( W-bound ( L~ ( Cage (C,j)))) by A6, XREAL_1: 47;

        assume i < (n + 1);

        then i <= n by NAT_1: 13;

        hence thesis by A3, A7, XXREAL_0: 1, XXREAL_0: 2;

      end;

      

       A8: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A8, A2);

      hence thesis by A1;

    end;

    theorem :: JORDAN1A:69

    i < j implies ( S-bound ( L~ ( Cage (C,i)))) < ( S-bound ( L~ ( Cage (C,j))))

    proof

      assume

       A1: i < j;

      defpred P[ Nat] means i < $1 implies ( S-bound ( L~ ( Cage (C,i)))) < ( S-bound ( L~ ( Cage (C,$1))));

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A3: P[n];

        set j = (n + 1), a = ( N-bound C), s = ( S-bound C);

        

         A4: ((s - ((a - s) / (2 |^ j))) - (s - ((a - s) / (2 |^ n)))) = (((s + ( - ((a - s) / (2 |^ j)))) - s) + ((a - s) / (2 |^ n)))

        .= (( - ((a - s) / ((2 |^ n) * 2))) + ((a - s) / (2 |^ n))) by NEWTON: 6

        .= ((( - (a - s)) / ((2 |^ n) * 2)) + ((a - s) / (2 |^ n))) by XCMPLX_1: 187

        .= ((( - (a - s)) / ((2 |^ n) * 2)) + (((a - s) * 2) / ((2 |^ n) * 2))) by XCMPLX_1: 91

        .= ((( - (a - s)) + ((a - s) * 2)) / ((2 |^ n) * 2)) by XCMPLX_1: 62

        .= ((a - s) / ((2 |^ n) * 2));

        (2 |^ n) > 0 by NEWTON: 83;

        then

         A5: ((2 |^ n) * 2) > ( 0 * 2) by XREAL_1: 68;

        

         A6: ( S-bound ( L~ ( Cage (C,n)))) = (s - ((a - s) / (2 |^ n))) & ( S-bound ( L~ ( Cage (C,j)))) = (s - ((a - s) / (2 |^ j))) by Th63;

        (a - s) > 0 by SPRECT_1: 32, XREAL_1: 50;

        then 0 < ((s - ((a - s) / (2 |^ j))) - (s - ((a - s) / (2 |^ n)))) by A5, A4, XREAL_1: 139;

        then

         A7: ( S-bound ( L~ ( Cage (C,n)))) < ( S-bound ( L~ ( Cage (C,j)))) by A6, XREAL_1: 47;

        assume i < (n + 1);

        then i <= n by NAT_1: 13;

        hence thesis by A3, A7, XXREAL_0: 1, XXREAL_0: 2;

      end;

      

       A8: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A8, A2);

      hence thesis by A1;

    end;

    theorem :: JORDAN1A:70

    1 <= i & i <= ( len ( Gauge (C,n))) implies ( N-bound ( L~ ( Cage (C,n)))) = ((( Gauge (C,n)) * (i,( len ( Gauge (C,n))))) `2 )

    proof

      set a = ( N-bound C), s = ( S-bound C), w = ( W-bound C), e = ( E-bound C), f = ( Cage (C,n)), G = ( Gauge (C,n));

      

       A1: ( len G) = ( width G) by JORDAN8:def 1;

      assume

       A2: 1 <= i & i <= ( len G);

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

      then

       A3: [i, ( len G)] in ( Indices G) by A2, A1, MATRIX_0: 30;

      

      thus ( N-bound ( L~ f)) = (a + ((a - s) / (2 |^ n))) by JORDAN10: 6

      .= (s + (((a - s) / (2 |^ n)) * (( len G) - 2))) by Lm10

      .= ( |[(w + (((e - w) / (2 |^ n)) * (i - 2))), (s + (((a - s) / (2 |^ n)) * (( len G) - 2)))]| `2 ) by EUCLID: 52

      .= ((G * (i,( len G))) `2 ) by A3, JORDAN8:def 1;

    end;

    theorem :: JORDAN1A:71

    1 <= i & i <= ( len ( Gauge (C,n))) implies ( E-bound ( L~ ( Cage (C,n)))) = ((( Gauge (C,n)) * (( len ( Gauge (C,n))),i)) `1 )

    proof

      set a = ( N-bound C), s = ( S-bound C), w = ( W-bound C), e = ( E-bound C), f = ( Cage (C,n)), G = ( Gauge (C,n));

      

       A1: ( len G) = ( width G) by JORDAN8:def 1;

      assume

       A2: 1 <= i & i <= ( len G);

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

      then

       A3: [( len G), i] in ( Indices G) by A2, A1, MATRIX_0: 30;

      

      thus ( E-bound ( L~ f)) = (e + ((e - w) / (2 |^ n))) by Th64

      .= (w + (((e - w) / (2 |^ n)) * (( len G) - 2))) by Lm10

      .= ( |[(w + (((e - w) / (2 |^ n)) * (( len G) - 2))), (s + (((a - s) / (2 |^ n)) * (i - 2)))]| `1 ) by EUCLID: 52

      .= ((G * (( len G),i)) `1 ) by A3, JORDAN8:def 1;

    end;

    theorem :: JORDAN1A:72

    1 <= i & i <= ( len ( Gauge (C,n))) implies ( S-bound ( L~ ( Cage (C,n)))) = ((( Gauge (C,n)) * (i,1)) `2 )

    proof

      set a = ( N-bound C), s = ( S-bound C), w = ( W-bound C), e = ( E-bound C), f = ( Cage (C,n)), G = ( Gauge (C,n));

      

       A1: ( len G) = ( width G) by JORDAN8:def 1;

      assume

       A2: 1 <= i & i <= ( len G);

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

      then

       A3: [i, 1] in ( Indices G) by A2, A1, MATRIX_0: 30;

      

      thus ( S-bound ( L~ f)) = (s - ((a - s) / (2 |^ n))) by Th63

      .= ( |[(w + (((e - w) / (2 |^ n)) * (i - 2))), (s + (((a - s) / (2 |^ n)) * (1 - 2)))]| `2 ) by EUCLID: 52

      .= ((G * (i,1)) `2 ) by A3, JORDAN8:def 1;

    end;

    theorem :: JORDAN1A:73

    1 <= i & i <= ( len ( Gauge (C,n))) implies ( W-bound ( L~ ( Cage (C,n)))) = ((( Gauge (C,n)) * (1,i)) `1 )

    proof

      set a = ( N-bound C), s = ( S-bound C), w = ( W-bound C), e = ( E-bound C), f = ( Cage (C,n)), G = ( Gauge (C,n));

      

       A1: ( len G) = ( width G) by JORDAN8:def 1;

      assume

       A2: 1 <= i & i <= ( len G);

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

      then

       A3: [1, i] in ( Indices G) by A2, A1, MATRIX_0: 30;

      

      thus ( W-bound ( L~ f)) = (w - ((e - w) / (2 |^ n))) by Th62

      .= ( |[(w + (((e - w) / (2 |^ n)) * (1 - 2))), (s + (((a - s) / (2 |^ n)) * (i - 2)))]| `1 ) by EUCLID: 52

      .= ((G * (1,i)) `1 ) by A3, JORDAN8:def 1;

    end;

    theorem :: JORDAN1A:74

    

     Th74: x in C & p in (( north_halfline x) /\ ( L~ ( Cage (C,n)))) implies (p `2 ) > (x `2 )

    proof

      set f = ( Cage (C,n));

      assume

       A1: x in C;

      assume

       A2: p in (( north_halfline x) /\ ( L~ f));

      then

       A3: p in ( north_halfline x) by XBOOLE_0:def 4;

      then

       A4: (p `1 ) = (x `1 ) by TOPREAL1:def 10;

      assume

       A5: (p `2 ) <= (x `2 );

      (p `2 ) >= (x `2 ) by A3, TOPREAL1:def 10;

      then (p `2 ) = (x `2 ) by A5, XXREAL_0: 1;

      then

       A6: p = x by A4, TOPREAL3: 6;

      p in ( L~ f) by A2, XBOOLE_0:def 4;

      then x in (C /\ ( L~ f)) by A1, A6, XBOOLE_0:def 4;

      then C meets ( L~ f);

      hence contradiction by JORDAN10: 5;

    end;

    theorem :: JORDAN1A:75

    

     Th75: x in C & p in (( east_halfline x) /\ ( L~ ( Cage (C,n)))) implies (p `1 ) > (x `1 )

    proof

      set f = ( Cage (C,n));

      assume

       A1: x in C;

      assume

       A2: p in (( east_halfline x) /\ ( L~ f));

      then

       A3: p in ( east_halfline x) by XBOOLE_0:def 4;

      then

       A4: (p `2 ) = (x `2 ) by TOPREAL1:def 11;

      assume

       A5: (p `1 ) <= (x `1 );

      (p `1 ) >= (x `1 ) by A3, TOPREAL1:def 11;

      then (p `1 ) = (x `1 ) by A5, XXREAL_0: 1;

      then

       A6: p = x by A4, TOPREAL3: 6;

      p in ( L~ f) by A2, XBOOLE_0:def 4;

      then x in (C /\ ( L~ f)) by A1, A6, XBOOLE_0:def 4;

      then C meets ( L~ f);

      hence contradiction by JORDAN10: 5;

    end;

    theorem :: JORDAN1A:76

    

     Th76: x in C & p in (( south_halfline x) /\ ( L~ ( Cage (C,n)))) implies (p `2 ) < (x `2 )

    proof

      set f = ( Cage (C,n));

      assume

       A1: x in C;

      assume

       A2: p in (( south_halfline x) /\ ( L~ f));

      then

       A3: p in ( south_halfline x) by XBOOLE_0:def 4;

      then

       A4: (p `1 ) = (x `1 ) by TOPREAL1:def 12;

      assume

       A5: (p `2 ) >= (x `2 );

      (p `2 ) <= (x `2 ) by A3, TOPREAL1:def 12;

      then (p `2 ) = (x `2 ) by A5, XXREAL_0: 1;

      then

       A6: p = x by A4, TOPREAL3: 6;

      p in ( L~ f) by A2, XBOOLE_0:def 4;

      then x in (C /\ ( L~ f)) by A1, A6, XBOOLE_0:def 4;

      then C meets ( L~ f);

      hence contradiction by JORDAN10: 5;

    end;

    theorem :: JORDAN1A:77

    

     Th77: x in C & p in (( west_halfline x) /\ ( L~ ( Cage (C,n)))) implies (p `1 ) < (x `1 )

    proof

      set f = ( Cage (C,n));

      assume

       A1: x in C;

      assume

       A2: p in (( west_halfline x) /\ ( L~ f));

      then

       A3: p in ( west_halfline x) by XBOOLE_0:def 4;

      then

       A4: (p `2 ) = (x `2 ) by TOPREAL1:def 13;

      assume

       A5: (p `1 ) >= (x `1 );

      (p `1 ) <= (x `1 ) by A3, TOPREAL1:def 13;

      then (p `1 ) = (x `1 ) by A5, XXREAL_0: 1;

      then

       A6: p = x by A4, TOPREAL3: 6;

      p in ( L~ f) by A2, XBOOLE_0:def 4;

      then x in (C /\ ( L~ f)) by A1, A6, XBOOLE_0:def 4;

      then C meets ( L~ f);

      hence contradiction by JORDAN10: 5;

    end;

    theorem :: JORDAN1A:78

    

     Th78: x in ( N-most C) & p in ( north_halfline x) & 1 <= i & i < ( len ( Cage (C,n))) & p in ( LSeg (( Cage (C,n)),i)) implies ( LSeg (( Cage (C,n)),i)) is horizontal

    proof

      set G = ( Gauge (C,n)), f = ( Cage (C,n));

      assume that

       A1: x in ( N-most C) and

       A2: p in ( north_halfline x) and

       A3: 1 <= i and

       A4: i < ( len f) and

       A5: p in ( LSeg (f,i));

      assume

       A6: not thesis;

      

       A7: (i + 1) <= ( len f) by A4, NAT_1: 13;

      then

       A8: ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A3, TOPREAL1:def 3;

      1 <= (i + 1) by A3, NAT_1: 13;

      then (i + 1) in ( Seg ( len f)) by A7, FINSEQ_1: 1;

      then

       A9: (i + 1) in ( dom f) by FINSEQ_1:def 3;

      i in ( Seg ( len f)) by A3, A4, FINSEQ_1: 1;

      then

       A10: i in ( dom f) by FINSEQ_1:def 3;

      

       A11: ( len G) = ( width G) by JORDAN8:def 1;

      then

       A12: (( len G) -' 1) <= ( width G) by NAT_D: 35;

      

       A13: x in C by A1, XBOOLE_0:def 4;

      p in ( L~ f) by A5, SPPOL_2: 17;

      then

       A14: p in (( north_halfline x) /\ ( L~ f)) by A2, XBOOLE_0:def 4;

      

       A15: f is_sequence_on G by JORDAN9:def 1;

      

       A16: (x `1 ) = (p `1 ) by A2, TOPREAL1:def 10

      .= ((f /. i) `1 ) by A5, A8, A6, SPPOL_1: 19, SPPOL_1: 41;

      

       A17: (x `1 ) = (p `1 ) by A2, TOPREAL1:def 10

      .= ((f /. (i + 1)) `1 ) by A5, A8, A6, SPPOL_1: 19, SPPOL_1: 41;

      per cases ;

        suppose

         A18: ((f /. i) `2 ) <= ((f /. (i + 1)) `2 );

        then (p `2 ) <= ((f /. (i + 1)) `2 ) by A5, A8, TOPREAL1: 4;

        then

         A19: ((f /. (i + 1)) `2 ) > (x `2 ) by A13, A14, Th74, XXREAL_0: 2;

        consider i1,i2 be Nat such that

         A20: [i1, i2] in ( Indices G) and

         A21: (f /. (i + 1)) = (G * (i1,i2)) by A15, A9, GOBOARD1:def 9;

        

         A22: 1 <= i2 by A20, MATRIX_0: 32;

        i2 <= ( width G) by A20, MATRIX_0: 32;

        then

         A23: i2 <= ( len G) by JORDAN8:def 1;

        

         A24: 1 <= i1 & i1 <= ( len G) by A20, MATRIX_0: 32;

        consider j1,j2 be Nat such that

         A25: [j1, j2] in ( Indices G) and

         A26: (f /. i) = (G * (j1,j2)) by A15, A10, GOBOARD1:def 9;

        

         A27: 1 <= j1 & j1 <= ( len G) by A25, MATRIX_0: 32;

        now

          assume ((f /. i) `2 ) = ((f /. (i + 1)) `2 );

          then

           A28: (f /. i) = (f /. (i + 1)) by A17, A16, TOPREAL3: 6;

          then

           A29: i2 = j2 by A20, A21, A25, A26, GOBOARD1: 5;

          i1 = j1 & ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A15, A10, A9, A20, A21, A25, A26, A28, GOBOARD1: 5, GOBOARD1:def 9;

          

          then 1 = ( 0 + |.(i2 - j2).|) by GOBOARD7: 2

          .= ( 0 + 0 ) by A29, GOBOARD7: 2;

          hence contradiction;

        end;

        then

         A30: ((f /. i) `2 ) < ((f /. (i + 1)) `2 ) by A18, XXREAL_0: 1;

        

         A31: 1 <= j2 by A25, MATRIX_0: 32;

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

        then i2 > j2 by A21, A22, A24, A26, A27, A30, Th19;

        then ( len G) > j2 by A23, XXREAL_0: 2;

        then

         A32: (( len G) -' 1) >= j2 by NAT_D: 49;

        (x `2 ) = (( N-min C) `2 ) by A1, PSCOMP_1: 39

        .= ( N-bound C) by EUCLID: 52

        .= ((G * (i1,(( len G) -' 1))) `2 ) by A24, JORDAN8: 14;

        then (x `2 ) >= ((f /. i) `2 ) by A12, A24, A26, A31, A27, A32, Th19;

        then x in ( L~ f) by A8, A17, A16, A19, GOBOARD7: 7, SPPOL_2: 17;

        then ( L~ f) meets C by A13, XBOOLE_0: 3;

        hence contradiction by JORDAN10: 5;

      end;

        suppose

         A33: ((f /. i) `2 ) >= ((f /. (i + 1)) `2 );

        then (p `2 ) <= ((f /. i) `2 ) by A5, A8, TOPREAL1: 4;

        then

         A34: ((f /. i) `2 ) > (x `2 ) by A13, A14, Th74, XXREAL_0: 2;

        consider i1,i2 be Nat such that

         A35: [i1, i2] in ( Indices G) and

         A36: (f /. i) = (G * (i1,i2)) by A15, A10, GOBOARD1:def 9;

        

         A37: 1 <= i2 by A35, MATRIX_0: 32;

        consider j1,j2 be Nat such that

         A38: [j1, j2] in ( Indices G) and

         A39: (f /. (i + 1)) = (G * (j1,j2)) by A15, A9, GOBOARD1:def 9;

        

         A40: 1 <= j1 & j1 <= ( len G) by A38, MATRIX_0: 32;

        now

          assume ((f /. i) `2 ) = ((f /. (i + 1)) `2 );

          then

           A41: (f /. i) = (f /. (i + 1)) by A17, A16, TOPREAL3: 6;

          then

           A42: i2 = j2 by A35, A36, A38, A39, GOBOARD1: 5;

          i1 = j1 & ( |.(j1 - i1).| + |.(j2 - i2).|) = 1 by A15, A10, A9, A35, A36, A38, A39, A41, GOBOARD1: 5, GOBOARD1:def 9;

          

          then 1 = ( 0 + |.(i2 - j2).|) by A42, GOBOARD7: 2

          .= ( 0 + 0 ) by A42, GOBOARD7: 2;

          hence contradiction;

        end;

        then

         A43: ((f /. (i + 1)) `2 ) < ((f /. i) `2 ) by A33, XXREAL_0: 1;

        

         A44: i2 <= ( width G) by A35, MATRIX_0: 32;

        

         A45: 1 <= i1 & i1 <= ( len G) by A35, MATRIX_0: 32;

        

         A46: 1 <= j2 by A38, MATRIX_0: 32;

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

        then i2 > j2 by A36, A37, A45, A39, A40, A43, Th19;

        then ( len G) > j2 by A11, A44, XXREAL_0: 2;

        then

         A47: (( len G) -' 1) >= j2 by NAT_D: 49;

        (x `2 ) = (( N-min C) `2 ) by A1, PSCOMP_1: 39

        .= ( N-bound C) by EUCLID: 52

        .= ((G * (i1,(( len G) -' 1))) `2 ) by A45, JORDAN8: 14;

        then (x `2 ) >= ((f /. (i + 1)) `2 ) by A12, A45, A39, A46, A40, A47, Th19;

        then x in ( L~ f) by A8, A17, A16, A34, GOBOARD7: 7, SPPOL_2: 17;

        then x in (( L~ f) /\ C) by A13, XBOOLE_0:def 4;

        then ( L~ f) meets C;

        hence contradiction by JORDAN10: 5;

      end;

    end;

    theorem :: JORDAN1A:79

    

     Th79: x in ( E-most C) & p in ( east_halfline x) & 1 <= i & i < ( len ( Cage (C,n))) & p in ( LSeg (( Cage (C,n)),i)) implies ( LSeg (( Cage (C,n)),i)) is vertical

    proof

      set G = ( Gauge (C,n)), f = ( Cage (C,n));

      assume that

       A1: x in ( E-most C) and

       A2: p in ( east_halfline x) and

       A3: 1 <= i and

       A4: i < ( len f) and

       A5: p in ( LSeg (f,i));

      assume

       A6: not thesis;

      

       A7: (i + 1) <= ( len f) by A4, NAT_1: 13;

      then

       A8: ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A3, TOPREAL1:def 3;

      1 <= (i + 1) by A3, NAT_1: 13;

      then (i + 1) in ( Seg ( len f)) by A7, FINSEQ_1: 1;

      then

       A9: (i + 1) in ( dom f) by FINSEQ_1:def 3;

      i in ( Seg ( len f)) by A3, A4, FINSEQ_1: 1;

      then

       A10: i in ( dom f) by FINSEQ_1:def 3;

      p in ( L~ f) by A5, SPPOL_2: 17;

      then

       A11: p in (( east_halfline x) /\ ( L~ f)) by A2, XBOOLE_0:def 4;

      

       A12: f is_sequence_on G by JORDAN9:def 1;

      

       A13: (x `2 ) = (p `2 ) by A2, TOPREAL1:def 11

      .= ((f /. i) `2 ) by A5, A8, A6, SPPOL_1: 19, SPPOL_1: 40;

      

       A14: (x `2 ) = (p `2 ) by A2, TOPREAL1:def 11

      .= ((f /. (i + 1)) `2 ) by A5, A8, A6, SPPOL_1: 19, SPPOL_1: 40;

      

       A15: ( len G) = ( width G) by JORDAN8:def 1;

      then

       A16: (( len G) -' 1) <= ( width G) by NAT_D: 35;

      

       A17: x in C by A1, XBOOLE_0:def 4;

      per cases ;

        suppose

         A18: ((f /. i) `1 ) <= ((f /. (i + 1)) `1 );

        then (p `1 ) <= ((f /. (i + 1)) `1 ) by A5, A8, TOPREAL1: 3;

        then

         A19: ((f /. (i + 1)) `1 ) > (x `1 ) by A17, A11, Th75, XXREAL_0: 2;

        consider i1,i2 be Nat such that

         A20: [i1, i2] in ( Indices G) and

         A21: (f /. (i + 1)) = (G * (i1,i2)) by A12, A9, GOBOARD1:def 9;

        

         A22: 1 <= i2 & i2 <= ( width G) by A20, MATRIX_0: 32;

        consider j1,j2 be Nat such that

         A23: [j1, j2] in ( Indices G) and

         A24: (f /. i) = (G * (j1,j2)) by A12, A10, GOBOARD1:def 9;

        

         A25: 1 <= j2 & j2 <= ( width G) by A23, MATRIX_0: 32;

        

         A26: i1 <= ( len G) by A20, MATRIX_0: 32;

        

         A27: 1 <= i1 by A20, MATRIX_0: 32;

        now

          assume ((f /. i) `1 ) = ((f /. (i + 1)) `1 );

          then

           A28: (f /. i) = (f /. (i + 1)) by A14, A13, TOPREAL3: 6;

          then

           A29: i2 = j2 by A20, A21, A23, A24, GOBOARD1: 5;

          i1 = j1 & ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A12, A10, A9, A20, A21, A23, A24, A28, GOBOARD1: 5, GOBOARD1:def 9;

          

          then 1 = ( 0 + |.(i2 - j2).|) by GOBOARD7: 2

          .= ( 0 + 0 ) by A29, GOBOARD7: 2;

          hence contradiction;

        end;

        then

         A30: ((f /. i) `1 ) < ((f /. (i + 1)) `1 ) by A18, XXREAL_0: 1;

        

         A31: 1 <= j1 by A23, MATRIX_0: 32;

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

        then i1 > j1 by A21, A22, A27, A24, A25, A30, Th18;

        then ( len G) > j1 by A26, XXREAL_0: 2;

        then

         A32: (( len G) -' 1) >= j1 by NAT_D: 49;

        (x `1 ) = (( E-min C) `1 ) by A1, PSCOMP_1: 47

        .= ( E-bound C) by EUCLID: 52

        .= ((G * ((( len G) -' 1),i2)) `1 ) by A15, A22, JORDAN8: 12;

        then (x `1 ) >= ((f /. i) `1 ) by A15, A16, A22, A24, A25, A31, A32, Th18;

        then x in ( L~ f) by A8, A14, A13, A19, GOBOARD7: 8, SPPOL_2: 17;

        then x in (( L~ f) /\ C) by A17, XBOOLE_0:def 4;

        then ( L~ f) meets C;

        hence contradiction by JORDAN10: 5;

      end;

        suppose

         A33: ((f /. i) `1 ) >= ((f /. (i + 1)) `1 );

        then (p `1 ) <= ((f /. i) `1 ) by A5, A8, TOPREAL1: 3;

        then

         A34: ((f /. i) `1 ) > (x `1 ) by A17, A11, Th75, XXREAL_0: 2;

        consider i1,i2 be Nat such that

         A35: [i1, i2] in ( Indices G) and

         A36: (f /. i) = (G * (i1,i2)) by A12, A10, GOBOARD1:def 9;

        

         A37: 1 <= i2 & i2 <= ( width G) by A35, MATRIX_0: 32;

        consider j1,j2 be Nat such that

         A38: [j1, j2] in ( Indices G) and

         A39: (f /. (i + 1)) = (G * (j1,j2)) by A12, A9, GOBOARD1:def 9;

        

         A40: 1 <= j2 & j2 <= ( width G) by A38, MATRIX_0: 32;

        

         A41: i1 <= ( len G) by A35, MATRIX_0: 32;

        

         A42: 1 <= i1 by A35, MATRIX_0: 32;

        now

          assume ((f /. i) `1 ) = ((f /. (i + 1)) `1 );

          then

           A43: (f /. i) = (f /. (i + 1)) by A14, A13, TOPREAL3: 6;

          then

           A44: i2 = j2 by A35, A36, A38, A39, GOBOARD1: 5;

          i1 = j1 & ( |.(j1 - i1).| + |.(j2 - i2).|) = 1 by A12, A10, A9, A35, A36, A38, A39, A43, GOBOARD1: 5, GOBOARD1:def 9;

          

          then 1 = ( 0 + |.(i2 - j2).|) by A44, GOBOARD7: 2

          .= ( 0 + 0 ) by A44, GOBOARD7: 2;

          hence contradiction;

        end;

        then

         A45: ((f /. (i + 1)) `1 ) < ((f /. i) `1 ) by A33, XXREAL_0: 1;

        

         A46: 1 <= j1 by A38, MATRIX_0: 32;

        j1 <= ( len G) by A38, MATRIX_0: 32;

        then i1 > j1 by A36, A37, A42, A39, A40, A45, Th18;

        then ( len G) > j1 by A41, XXREAL_0: 2;

        then

         A47: (( len G) -' 1) >= j1 by NAT_D: 49;

        (x `1 ) = (( E-min C) `1 ) by A1, PSCOMP_1: 47

        .= ( E-bound C) by EUCLID: 52

        .= ((G * ((( len G) -' 1),i2)) `1 ) by A15, A37, JORDAN8: 12;

        then (x `1 ) >= ((f /. (i + 1)) `1 ) by A15, A16, A37, A39, A40, A46, A47, Th18;

        then x in ( L~ f) by A8, A14, A13, A34, GOBOARD7: 8, SPPOL_2: 17;

        then x in (( L~ f) /\ C) by A17, XBOOLE_0:def 4;

        then ( L~ f) meets C;

        hence contradiction by JORDAN10: 5;

      end;

    end;

    theorem :: JORDAN1A:80

    

     Th80: x in ( S-most C) & p in ( south_halfline x) & 1 <= i & i < ( len ( Cage (C,n))) & p in ( LSeg (( Cage (C,n)),i)) implies ( LSeg (( Cage (C,n)),i)) is horizontal

    proof

      set G = ( Gauge (C,n)), f = ( Cage (C,n));

      assume that

       A1: x in ( S-most C) and

       A2: p in ( south_halfline x) and

       A3: 1 <= i and

       A4: i < ( len f) and

       A5: p in ( LSeg (f,i));

      assume

       A6: not thesis;

      

       A7: (i + 1) <= ( len f) by A4, NAT_1: 13;

      then

       A8: ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A3, TOPREAL1:def 3;

      1 <= (i + 1) by A3, NAT_1: 13;

      then (i + 1) in ( Seg ( len f)) by A7, FINSEQ_1: 1;

      then

       A9: (i + 1) in ( dom f) by FINSEQ_1:def 3;

      p in ( L~ f) by A5, SPPOL_2: 17;

      then

       A10: p in (( south_halfline x) /\ ( L~ f)) by A2, XBOOLE_0:def 4;

      

       A11: f is_sequence_on G by JORDAN9:def 1;

      

       A12: (x `1 ) = (p `1 ) by A2, TOPREAL1:def 12

      .= ((f /. i) `1 ) by A5, A8, A6, SPPOL_1: 19, SPPOL_1: 41;

      i in ( Seg ( len f)) by A3, A4, FINSEQ_1: 1;

      then

       A13: i in ( dom f) by FINSEQ_1:def 3;

      

       A14: (x `1 ) = (p `1 ) by A2, TOPREAL1:def 12

      .= ((f /. (i + 1)) `1 ) by A5, A8, A6, SPPOL_1: 19, SPPOL_1: 41;

      

       A15: x in C by A1, XBOOLE_0:def 4;

      per cases ;

        suppose

         A16: ((f /. i) `2 ) <= ((f /. (i + 1)) `2 );

        then ((f /. i) `2 ) <= (p `2 ) by A5, A8, TOPREAL1: 4;

        then

         A17: ((f /. i) `2 ) < (x `2 ) by A15, A10, Th76, XXREAL_0: 2;

        consider i1,i2 be Nat such that

         A18: [i1, i2] in ( Indices G) and

         A19: (f /. i) = (G * (i1,i2)) by A11, A13, GOBOARD1:def 9;

        

         A20: i2 <= ( width G) by A18, MATRIX_0: 32;

        

         A21: 1 <= i2 by A18, MATRIX_0: 32;

        

         A22: 1 <= i1 & i1 <= ( len G) by A18, MATRIX_0: 32;

        

         A23: (x `2 ) = (( S-min C) `2 ) by A1, PSCOMP_1: 55

        .= ( S-bound C) by EUCLID: 52

        .= ((G * (i1,2)) `2 ) by A22, JORDAN8: 13;

        then i2 < (1 + 1) by A17, A19, A20, A22, SPRECT_3: 12;

        then

         A24: i2 <= 1 by NAT_1: 13;

        consider j1,j2 be Nat such that

         A25: [j1, j2] in ( Indices G) and

         A26: (f /. (i + 1)) = (G * (j1,j2)) by A11, A9, GOBOARD1:def 9;

        

         A27: j2 <= ( width G) by A25, MATRIX_0: 32;

        now

          assume ((f /. i) `2 ) = ((f /. (i + 1)) `2 );

          then

           A28: (f /. i) = (f /. (i + 1)) by A14, A12, TOPREAL3: 6;

          then

           A29: i1 = j1 by A18, A19, A25, A26, GOBOARD1: 5;

          

           A30: i2 = j2 by A18, A19, A25, A26, A28, GOBOARD1: 5;

          ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A11, A13, A9, A18, A19, A25, A26, GOBOARD1:def 9;

          

          then 1 = ( 0 + |.(i2 - j2).|) by A29, GOBOARD7: 2

          .= ( 0 + 0 ) by A30, GOBOARD7: 2;

          hence contradiction;

        end;

        then

         A31: ((f /. i) `2 ) < ((f /. (i + 1)) `2 ) by A16, XXREAL_0: 1;

        

         A32: 1 <= j1 & j1 <= ( len G) by A25, MATRIX_0: 32;

        1 <= j2 by A25, MATRIX_0: 32;

        then i2 < j2 by A19, A20, A22, A26, A32, A31, Th19;

        then 1 < j2 by A21, A24, XXREAL_0: 1;

        then (1 + 1) <= j2 by NAT_1: 13;

        then (x `2 ) <= ((f /. (i + 1)) `2 ) by A22, A23, A26, A27, A32, Th19;

        then x in ( L~ f) by A8, A14, A12, A17, GOBOARD7: 7, SPPOL_2: 17;

        then x in (( L~ f) /\ C) by A15, XBOOLE_0:def 4;

        then ( L~ f) meets C;

        hence contradiction by JORDAN10: 5;

      end;

        suppose

         A33: ((f /. i) `2 ) >= ((f /. (i + 1)) `2 );

        then ((f /. (i + 1)) `2 ) <= (p `2 ) by A5, A8, TOPREAL1: 4;

        then

         A34: ((f /. (i + 1)) `2 ) < (x `2 ) by A15, A10, Th76, XXREAL_0: 2;

        consider i1,i2 be Nat such that

         A35: [i1, i2] in ( Indices G) and

         A36: (f /. (i + 1)) = (G * (i1,i2)) by A11, A9, GOBOARD1:def 9;

        

         A37: i2 <= ( width G) by A35, MATRIX_0: 32;

        

         A38: 1 <= i2 by A35, MATRIX_0: 32;

        

         A39: 1 <= i1 & i1 <= ( len G) by A35, MATRIX_0: 32;

        

         A40: (x `2 ) = (( S-min C) `2 ) by A1, PSCOMP_1: 55

        .= ( S-bound C) by EUCLID: 52

        .= ((G * (i1,2)) `2 ) by A39, JORDAN8: 13;

        then i2 < (1 + 1) by A34, A36, A37, A39, SPRECT_3: 12;

        then

         A41: i2 <= 1 by NAT_1: 13;

        consider j1,j2 be Nat such that

         A42: [j1, j2] in ( Indices G) and

         A43: (f /. i) = (G * (j1,j2)) by A11, A13, GOBOARD1:def 9;

        

         A44: j2 <= ( width G) by A42, MATRIX_0: 32;

        now

          assume ((f /. i) `2 ) = ((f /. (i + 1)) `2 );

          then

           A45: (f /. i) = (f /. (i + 1)) by A14, A12, TOPREAL3: 6;

          then

           A46: i1 = j1 by A35, A36, A42, A43, GOBOARD1: 5;

          

           A47: i2 = j2 by A35, A36, A42, A43, A45, GOBOARD1: 5;

          ( |.(j1 - i1).| + |.(j2 - i2).|) = 1 by A11, A13, A9, A35, A36, A42, A43, GOBOARD1:def 9;

          

          then 1 = ( 0 + |.(i2 - j2).|) by A46, A47, GOBOARD7: 2

          .= ( 0 + 0 ) by A47, GOBOARD7: 2;

          hence contradiction;

        end;

        then

         A48: ((f /. (i + 1)) `2 ) < ((f /. i) `2 ) by A33, XXREAL_0: 1;

        

         A49: 1 <= j1 & j1 <= ( len G) by A42, MATRIX_0: 32;

        1 <= j2 by A42, MATRIX_0: 32;

        then i2 < j2 by A36, A37, A39, A43, A49, A48, Th19;

        then 1 < j2 by A38, A41, XXREAL_0: 1;

        then (1 + 1) <= j2 by NAT_1: 13;

        then (x `2 ) <= ((f /. i) `2 ) by A39, A40, A43, A44, A49, Th19;

        then x in ( L~ f) by A8, A14, A12, A34, GOBOARD7: 7, SPPOL_2: 17;

        then x in (( L~ f) /\ C) by A15, XBOOLE_0:def 4;

        then ( L~ f) meets C;

        hence contradiction by JORDAN10: 5;

      end;

    end;

    theorem :: JORDAN1A:81

    

     Th81: x in ( W-most C) & p in ( west_halfline x) & 1 <= i & i < ( len ( Cage (C,n))) & p in ( LSeg (( Cage (C,n)),i)) implies ( LSeg (( Cage (C,n)),i)) is vertical

    proof

      set G = ( Gauge (C,n)), f = ( Cage (C,n));

      assume that

       A1: x in ( W-most C) and

       A2: p in ( west_halfline x) and

       A3: 1 <= i and

       A4: i < ( len f) and

       A5: p in ( LSeg (f,i));

      assume

       A6: not thesis;

      

       A7: (i + 1) <= ( len f) by A4, NAT_1: 13;

      then

       A8: ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A3, TOPREAL1:def 3;

      1 <= (i + 1) by A3, NAT_1: 13;

      then (i + 1) in ( Seg ( len f)) by A7, FINSEQ_1: 1;

      then

       A9: (i + 1) in ( dom f) by FINSEQ_1:def 3;

      p in ( L~ f) by A5, SPPOL_2: 17;

      then

       A10: p in (( west_halfline x) /\ ( L~ f)) by A2, XBOOLE_0:def 4;

      

       A11: f is_sequence_on G by JORDAN9:def 1;

      

       A12: (x `2 ) = (p `2 ) by A2, TOPREAL1:def 13

      .= ((f /. i) `2 ) by A5, A8, A6, SPPOL_1: 19, SPPOL_1: 40;

      i in ( Seg ( len f)) by A3, A4, FINSEQ_1: 1;

      then

       A13: i in ( dom f) by FINSEQ_1:def 3;

      

       A14: (x `2 ) = (p `2 ) by A2, TOPREAL1:def 13

      .= ((f /. (i + 1)) `2 ) by A5, A8, A6, SPPOL_1: 19, SPPOL_1: 40;

      

       A15: x in C by A1, XBOOLE_0:def 4;

      per cases ;

        suppose

         A16: ((f /. i) `1 ) <= ((f /. (i + 1)) `1 );

        consider i1,i2 be Nat such that

         A17: [i1, i2] in ( Indices G) and

         A18: (f /. i) = (G * (i1,i2)) by A11, A13, GOBOARD1:def 9;

        

         A19: 1 <= i2 by A17, MATRIX_0: 32;

        

         A20: i2 <= ( width G) by A17, MATRIX_0: 32;

        then

         A21: i2 <= ( len G) by JORDAN8:def 1;

        consider j1,j2 be Nat such that

         A22: [j1, j2] in ( Indices G) and

         A23: (f /. (i + 1)) = (G * (j1,j2)) by A11, A9, GOBOARD1:def 9;

        

         A24: 1 <= j2 & j2 <= ( width G) by A22, MATRIX_0: 32;

        now

          assume ((f /. i) `1 ) = ((f /. (i + 1)) `1 );

          then

           A25: (f /. i) = (f /. (i + 1)) by A14, A12, TOPREAL3: 6;

          then

           A26: i1 = j1 by A17, A18, A22, A23, GOBOARD1: 5;

          

           A27: i2 = j2 by A17, A18, A22, A23, A25, GOBOARD1: 5;

          ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A11, A13, A9, A17, A18, A22, A23, GOBOARD1:def 9;

          

          then 1 = ( 0 + |.(i2 - j2).|) by A26, GOBOARD7: 2

          .= ( 0 + 0 ) by A27, GOBOARD7: 2;

          hence contradiction;

        end;

        then

         A28: ((f /. i) `1 ) < ((f /. (i + 1)) `1 ) by A16, XXREAL_0: 1;

        ((f /. i) `1 ) <= (p `1 ) by A5, A8, A16, TOPREAL1: 3;

        then

         A29: ((f /. i) `1 ) < (x `1 ) by A15, A10, Th77, XXREAL_0: 2;

        

         A30: 1 <= i1 by A17, MATRIX_0: 32;

        

         A31: i1 <= ( len G) by A17, MATRIX_0: 32;

        

         A32: (x `1 ) = (( W-min C) `1 ) by A1, PSCOMP_1: 31

        .= ( W-bound C) by EUCLID: 52

        .= ((G * (2,i2)) `1 ) by A19, A21, JORDAN8: 11;

        then i1 < (1 + 1) by A29, A18, A19, A20, A31, SPRECT_3: 13;

        then

         A33: i1 <= 1 by NAT_1: 13;

        

         A34: j1 <= ( len G) by A22, MATRIX_0: 32;

        1 <= j1 by A22, MATRIX_0: 32;

        then i1 < j1 by A18, A19, A20, A31, A23, A24, A28, Th18;

        then 1 < j1 by A30, A33, XXREAL_0: 1;

        then (1 + 1) <= j1 by NAT_1: 13;

        then (x `1 ) <= ((f /. (i + 1)) `1 ) by A19, A20, A32, A23, A24, A34, Th18;

        then x in ( L~ f) by A8, A14, A12, A29, GOBOARD7: 8, SPPOL_2: 17;

        then x in (( L~ f) /\ C) by A15, XBOOLE_0:def 4;

        then ( L~ f) meets C;

        hence contradiction by JORDAN10: 5;

      end;

        suppose

         A35: ((f /. i) `1 ) >= ((f /. (i + 1)) `1 );

        consider i1,i2 be Nat such that

         A36: [i1, i2] in ( Indices G) and

         A37: (f /. (i + 1)) = (G * (i1,i2)) by A11, A9, GOBOARD1:def 9;

        

         A38: 1 <= i2 by A36, MATRIX_0: 32;

        

         A39: i2 <= ( width G) by A36, MATRIX_0: 32;

        then

         A40: i2 <= ( len G) by JORDAN8:def 1;

        consider j1,j2 be Nat such that

         A41: [j1, j2] in ( Indices G) and

         A42: (f /. i) = (G * (j1,j2)) by A11, A13, GOBOARD1:def 9;

        

         A43: 1 <= j2 & j2 <= ( width G) by A41, MATRIX_0: 32;

        now

          assume ((f /. i) `1 ) = ((f /. (i + 1)) `1 );

          then

           A44: (f /. i) = (f /. (i + 1)) by A14, A12, TOPREAL3: 6;

          then

           A45: i1 = j1 by A36, A37, A41, A42, GOBOARD1: 5;

          

           A46: i2 = j2 by A36, A37, A41, A42, A44, GOBOARD1: 5;

          ( |.(j1 - i1).| + |.(j2 - i2).|) = 1 by A11, A13, A9, A36, A37, A41, A42, GOBOARD1:def 9;

          

          then 1 = ( 0 + |.(i2 - j2).|) by A45, A46, GOBOARD7: 2

          .= ( 0 + 0 ) by A46, GOBOARD7: 2;

          hence contradiction;

        end;

        then

         A47: ((f /. (i + 1)) `1 ) < ((f /. i) `1 ) by A35, XXREAL_0: 1;

        ((f /. (i + 1)) `1 ) <= (p `1 ) by A5, A8, A35, TOPREAL1: 3;

        then

         A48: ((f /. (i + 1)) `1 ) < (x `1 ) by A15, A10, Th77, XXREAL_0: 2;

        

         A49: 1 <= i1 by A36, MATRIX_0: 32;

        

         A50: i1 <= ( len G) by A36, MATRIX_0: 32;

        

         A51: (x `1 ) = (( W-min C) `1 ) by A1, PSCOMP_1: 31

        .= ( W-bound C) by EUCLID: 52

        .= ((G * (2,i2)) `1 ) by A38, A40, JORDAN8: 11;

        then i1 < (1 + 1) by A48, A37, A38, A39, A50, SPRECT_3: 13;

        then

         A52: i1 <= 1 by NAT_1: 13;

        

         A53: j1 <= ( len G) by A41, MATRIX_0: 32;

        1 <= j1 by A41, MATRIX_0: 32;

        then i1 < j1 by A37, A38, A39, A50, A42, A43, A47, Th18;

        then 1 < j1 by A49, A52, XXREAL_0: 1;

        then (1 + 1) <= j1 by NAT_1: 13;

        then (x `1 ) <= ((f /. i) `1 ) by A38, A39, A51, A42, A43, A53, Th18;

        then x in ( L~ f) by A8, A14, A12, A48, GOBOARD7: 8, SPPOL_2: 17;

        then x in (( L~ f) /\ C) by A15, XBOOLE_0:def 4;

        then ( L~ f) meets C;

        hence contradiction by JORDAN10: 5;

      end;

    end;

    theorem :: JORDAN1A:82

    

     Th82: x in ( N-most C) & p in (( north_halfline x) /\ ( L~ ( Cage (C,n)))) implies (p `2 ) = ( N-bound ( L~ ( Cage (C,n))))

    proof

      set G = ( Gauge (C,n)), f = ( Cage (C,n));

      

       A1: f is_sequence_on G by JORDAN9:def 1;

      assume

       A2: x in ( N-most C);

      then

       A3: x in C by XBOOLE_0:def 4;

      assume

       A4: p in (( north_halfline x) /\ ( L~ f));

      then p in ( L~ f) by XBOOLE_0:def 4;

      then

      consider i such that

       A5: 1 <= i and

       A6: (i + 1) <= ( len f) and

       A7: p in ( LSeg (f,i)) by SPPOL_2: 13;

      

       A8: ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A5, A6, TOPREAL1:def 3;

      

       A9: i < ( len f) by A6, NAT_1: 13;

      then i in ( Seg ( len f)) by A5, FINSEQ_1: 1;

      then i in ( dom f) by FINSEQ_1:def 3;

      then

      consider i1,i2 be Nat such that

       A10: [i1, i2] in ( Indices G) and

       A11: (f /. i) = (G * (i1,i2)) by A1, GOBOARD1:def 9;

      

       A12: 1 <= i2 by A10, MATRIX_0: 32;

      p in ( north_halfline x) by A4, XBOOLE_0:def 4;

      then ( LSeg (f,i)) is horizontal by A2, A5, A7, A9, Th78;

      then ((f /. i) `2 ) = ((f /. (i + 1)) `2 ) by A8, SPPOL_1: 15;

      then

       A13: (p `2 ) = ((f /. i) `2 ) by A7, A8, GOBOARD7: 6;

      

       A14: i2 <= ( width G) by A10, MATRIX_0: 32;

      

       A15: 1 <= i1 & i1 <= ( len G) by A10, MATRIX_0: 32;

      

       A16: (( len G) -' 1) <= ( len G) by NAT_D: 35;

      

       A17: ( len G) = ( width G) by JORDAN8:def 1;

      (x `2 ) = (( N-min C) `2 ) by A2, PSCOMP_1: 39

      .= ( N-bound C) by EUCLID: 52

      .= ((G * (i1,(( len G) -' 1))) `2 ) by A15, JORDAN8: 14;

      then i2 > (( len G) -' 1) by A3, A4, A11, A17, A12, A15, A13, A16, Th74, SPRECT_3: 12;

      then i2 >= ((( len G) -' 1) + 1) by NAT_1: 13;

      then i2 >= ( len G) by A12, XREAL_1: 235, XXREAL_0: 2;

      then i2 = ( len G) by A17, A14, XXREAL_0: 1;

      then (f /. i) in ( N-most ( L~ f)) by A5, A9, A11, A17, A15, Th58;

      hence thesis by A13, Th3;

    end;

    theorem :: JORDAN1A:83

    

     Th83: x in ( E-most C) & p in (( east_halfline x) /\ ( L~ ( Cage (C,n)))) implies (p `1 ) = ( E-bound ( L~ ( Cage (C,n))))

    proof

      set G = ( Gauge (C,n)), f = ( Cage (C,n));

      

       A1: f is_sequence_on G by JORDAN9:def 1;

      assume

       A2: x in ( E-most C);

      then

       A3: x in C by XBOOLE_0:def 4;

      

       A4: (( len G) -' 1) <= ( len G) by NAT_D: 35;

      

       A5: ( len G) = ( width G) by JORDAN8:def 1;

      assume

       A6: p in (( east_halfline x) /\ ( L~ f));

      then p in ( L~ f) by XBOOLE_0:def 4;

      then

      consider i such that

       A7: 1 <= i and

       A8: (i + 1) <= ( len f) and

       A9: p in ( LSeg (f,i)) by SPPOL_2: 13;

      

       A10: ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A7, A8, TOPREAL1:def 3;

      

       A11: i < ( len f) by A8, NAT_1: 13;

      then i in ( Seg ( len f)) by A7, FINSEQ_1: 1;

      then i in ( dom f) by FINSEQ_1:def 3;

      then

      consider i1,i2 be Nat such that

       A12: [i1, i2] in ( Indices G) and

       A13: (f /. i) = (G * (i1,i2)) by A1, GOBOARD1:def 9;

      

       A14: 1 <= i2 & i2 <= ( width G) by A12, MATRIX_0: 32;

      p in ( east_halfline x) by A6, XBOOLE_0:def 4;

      then ( LSeg (f,i)) is vertical by A2, A7, A9, A11, Th79;

      then ((f /. i) `1 ) = ((f /. (i + 1)) `1 ) by A10, SPPOL_1: 16;

      then

       A15: (p `1 ) = ((f /. i) `1 ) by A9, A10, GOBOARD7: 5;

      

       A16: i1 <= ( len G) by A12, MATRIX_0: 32;

      

       A17: 1 <= i1 by A12, MATRIX_0: 32;

      (x `1 ) = (( E-min C) `1 ) by A2, PSCOMP_1: 47

      .= ( E-bound C) by EUCLID: 52

      .= ((G * ((( len G) -' 1),i2)) `1 ) by A5, A14, JORDAN8: 12;

      then i1 > (( len G) -' 1) by A3, A6, A13, A14, A17, A15, A4, Th75, SPRECT_3: 13;

      then i1 >= ((( len G) -' 1) + 1) by NAT_1: 13;

      then i1 >= ( len G) by A17, XREAL_1: 235, XXREAL_0: 2;

      then i1 = ( len G) by A16, XXREAL_0: 1;

      then (f /. i) in ( E-most ( L~ f)) by A7, A11, A13, A14, Th61;

      hence thesis by A15, Th4;

    end;

    theorem :: JORDAN1A:84

    

     Th84: x in ( S-most C) & p in (( south_halfline x) /\ ( L~ ( Cage (C,n)))) implies (p `2 ) = ( S-bound ( L~ ( Cage (C,n))))

    proof

      set G = ( Gauge (C,n)), f = ( Cage (C,n));

      

       A1: f is_sequence_on G by JORDAN9:def 1;

      assume

       A2: x in ( S-most C);

      then

       A3: x in C by XBOOLE_0:def 4;

      assume

       A4: p in (( south_halfline x) /\ ( L~ f));

      then p in ( L~ f) by XBOOLE_0:def 4;

      then

      consider i such that

       A5: 1 <= i and

       A6: (i + 1) <= ( len f) and

       A7: p in ( LSeg (f,i)) by SPPOL_2: 13;

      

       A8: ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A5, A6, TOPREAL1:def 3;

      

       A9: i < ( len f) by A6, NAT_1: 13;

      then i in ( Seg ( len f)) by A5, FINSEQ_1: 1;

      then i in ( dom f) by FINSEQ_1:def 3;

      then

      consider i1,i2 be Nat such that

       A10: [i1, i2] in ( Indices G) and

       A11: (f /. i) = (G * (i1,i2)) by A1, GOBOARD1:def 9;

      

       A12: 1 <= i2 by A10, MATRIX_0: 32;

      p in ( south_halfline x) by A4, XBOOLE_0:def 4;

      then ( LSeg (f,i)) is horizontal by A2, A5, A7, A9, Th80;

      then ((f /. i) `2 ) = ((f /. (i + 1)) `2 ) by A8, SPPOL_1: 15;

      then

       A13: (p `2 ) = ((f /. i) `2 ) by A7, A8, GOBOARD7: 6;

      

       A14: i2 <= ( width G) by A10, MATRIX_0: 32;

      

       A15: 1 <= i1 & i1 <= ( len G) by A10, MATRIX_0: 32;

      (x `2 ) = (( S-min C) `2 ) by A2, PSCOMP_1: 55

      .= ( S-bound C) by EUCLID: 52

      .= ((G * (i1,2)) `2 ) by A15, JORDAN8: 13;

      then i2 < (1 + 1) by A3, A4, A11, A14, A15, A13, Th76, SPRECT_3: 12;

      then i2 <= 1 by NAT_1: 13;

      then i2 = 1 by A12, XXREAL_0: 1;

      then (f /. i) in ( S-most ( L~ f)) by A5, A9, A11, A15, Th60;

      hence thesis by A13, Th5;

    end;

    theorem :: JORDAN1A:85

    

     Th85: x in ( W-most C) & p in (( west_halfline x) /\ ( L~ ( Cage (C,n)))) implies (p `1 ) = ( W-bound ( L~ ( Cage (C,n))))

    proof

      set G = ( Gauge (C,n)), f = ( Cage (C,n));

      

       A1: f is_sequence_on G by JORDAN9:def 1;

      assume

       A2: x in ( W-most C);

      then

       A3: x in C by XBOOLE_0:def 4;

      

       A4: ( len G) = ( width G) by JORDAN8:def 1;

      assume

       A5: p in (( west_halfline x) /\ ( L~ f));

      then p in ( L~ f) by XBOOLE_0:def 4;

      then

      consider i such that

       A6: 1 <= i and

       A7: (i + 1) <= ( len f) and

       A8: p in ( LSeg (f,i)) by SPPOL_2: 13;

      

       A9: ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A6, A7, TOPREAL1:def 3;

      

       A10: i < ( len f) by A7, NAT_1: 13;

      then i in ( Seg ( len f)) by A6, FINSEQ_1: 1;

      then i in ( dom f) by FINSEQ_1:def 3;

      then

      consider i1,i2 be Nat such that

       A11: [i1, i2] in ( Indices G) and

       A12: (f /. i) = (G * (i1,i2)) by A1, GOBOARD1:def 9;

      

       A13: 1 <= i2 & i2 <= ( width G) by A11, MATRIX_0: 32;

      p in ( west_halfline x) by A5, XBOOLE_0:def 4;

      then ( LSeg (f,i)) is vertical by A2, A6, A8, A10, Th81;

      then ((f /. i) `1 ) = ((f /. (i + 1)) `1 ) by A9, SPPOL_1: 16;

      then

       A14: (p `1 ) = ((f /. i) `1 ) by A8, A9, GOBOARD7: 5;

      

       A15: i1 <= ( len G) by A11, MATRIX_0: 32;

      

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

      (x `1 ) = (( W-min C) `1 ) by A2, PSCOMP_1: 31

      .= ( W-bound C) by EUCLID: 52

      .= ((G * (2,i2)) `1 ) by A4, A13, JORDAN8: 11;

      then i1 < (1 + 1) by A3, A5, A12, A13, A15, A14, Th77, SPRECT_3: 13;

      then i1 <= 1 by NAT_1: 13;

      then i1 = 1 by A16, XXREAL_0: 1;

      then (f /. i) in ( W-most ( L~ f)) by A6, A10, A12, A13, Th59;

      hence thesis by A14, Th6;

    end;

    theorem :: JORDAN1A:86

    x in ( N-most C) implies ex p be Point of ( TOP-REAL 2) st (( north_halfline x) /\ ( L~ ( Cage (C,n)))) = {p}

    proof

      set f = ( Cage (C,n));

      assume

       A1: x in ( N-most C);

      then x in C by XBOOLE_0:def 4;

      then ( north_halfline x) meets ( L~ f) by Th51;

      then

      consider p be object such that

       A2: p in ( north_halfline x) and

       A3: p in ( L~ f) by XBOOLE_0: 3;

      

       A4: p in (( north_halfline x) /\ ( L~ f)) by A2, A3, XBOOLE_0:def 4;

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

      take p;

      hereby

        let a be object;

        assume

         A5: a in (( north_halfline x) /\ ( L~ f));

        then

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

        y in ( north_halfline x) by A5, XBOOLE_0:def 4;

        

        then

         A6: (y `1 ) = (x `1 ) by TOPREAL1:def 10

        .= (p `1 ) by A2, TOPREAL1:def 10;

        (p `2 ) = ( N-bound ( L~ f)) by A1, A4, Th82

        .= (y `2 ) by A1, A5, Th82;

        then y = p by A6, TOPREAL3: 6;

        hence a in {p} by TARSKI:def 1;

      end;

      thus thesis by A4, ZFMISC_1: 31;

    end;

    theorem :: JORDAN1A:87

    x in ( E-most C) implies ex p be Point of ( TOP-REAL 2) st (( east_halfline x) /\ ( L~ ( Cage (C,n)))) = {p}

    proof

      set f = ( Cage (C,n));

      assume

       A1: x in ( E-most C);

      then x in C by XBOOLE_0:def 4;

      then ( east_halfline x) meets ( L~ f) by Th52;

      then

      consider p be object such that

       A2: p in ( east_halfline x) and

       A3: p in ( L~ f) by XBOOLE_0: 3;

      

       A4: p in (( east_halfline x) /\ ( L~ f)) by A2, A3, XBOOLE_0:def 4;

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

      take p;

      hereby

        let a be object;

        assume

         A5: a in (( east_halfline x) /\ ( L~ f));

        then

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

        y in ( east_halfline x) by A5, XBOOLE_0:def 4;

        

        then

         A6: (y `2 ) = (x `2 ) by TOPREAL1:def 11

        .= (p `2 ) by A2, TOPREAL1:def 11;

        (p `1 ) = ( E-bound ( L~ f)) by A1, A4, Th83

        .= (y `1 ) by A1, A5, Th83;

        then y = p by A6, TOPREAL3: 6;

        hence a in {p} by TARSKI:def 1;

      end;

      thus thesis by A4, ZFMISC_1: 31;

    end;

    theorem :: JORDAN1A:88

    x in ( S-most C) implies ex p be Point of ( TOP-REAL 2) st (( south_halfline x) /\ ( L~ ( Cage (C,n)))) = {p}

    proof

      set f = ( Cage (C,n));

      assume

       A1: x in ( S-most C);

      then x in C by XBOOLE_0:def 4;

      then ( south_halfline x) meets ( L~ f) by Th53;

      then

      consider p be object such that

       A2: p in ( south_halfline x) and

       A3: p in ( L~ f) by XBOOLE_0: 3;

      

       A4: p in (( south_halfline x) /\ ( L~ f)) by A2, A3, XBOOLE_0:def 4;

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

      take p;

      hereby

        let a be object;

        assume

         A5: a in (( south_halfline x) /\ ( L~ f));

        then

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

        y in ( south_halfline x) by A5, XBOOLE_0:def 4;

        

        then

         A6: (y `1 ) = (x `1 ) by TOPREAL1:def 12

        .= (p `1 ) by A2, TOPREAL1:def 12;

        (p `2 ) = ( S-bound ( L~ f)) by A1, A4, Th84

        .= (y `2 ) by A1, A5, Th84;

        then y = p by A6, TOPREAL3: 6;

        hence a in {p} by TARSKI:def 1;

      end;

      thus thesis by A4, ZFMISC_1: 31;

    end;

    theorem :: JORDAN1A:89

    x in ( W-most C) implies ex p be Point of ( TOP-REAL 2) st (( west_halfline x) /\ ( L~ ( Cage (C,n)))) = {p}

    proof

      set f = ( Cage (C,n));

      assume

       A1: x in ( W-most C);

      then x in C by XBOOLE_0:def 4;

      then ( west_halfline x) meets ( L~ f) by Th54;

      then

      consider p be object such that

       A2: p in ( west_halfline x) and

       A3: p in ( L~ f) by XBOOLE_0: 3;

      

       A4: p in (( west_halfline x) /\ ( L~ f)) by A2, A3, XBOOLE_0:def 4;

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

      take p;

      hereby

        let a be object;

        assume

         A5: a in (( west_halfline x) /\ ( L~ f));

        then

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

        y in ( west_halfline x) by A5, XBOOLE_0:def 4;

        

        then

         A6: (y `2 ) = (x `2 ) by TOPREAL1:def 13

        .= (p `2 ) by A2, TOPREAL1:def 13;

        (p `1 ) = ( W-bound ( L~ f)) by A1, A4, Th85

        .= (y `1 ) by A1, A5, Th85;

        then y = p by A6, TOPREAL3: 6;

        hence a in {p} by TARSKI:def 1;

      end;

      thus thesis by A4, ZFMISC_1: 31;

    end;