jordan1f.miz



    begin

    reserve i,j,k,m,n for Nat,

f for FinSequence of the carrier of ( TOP-REAL 2),

G for Go-board;

    theorem :: JORDAN1F:1

    

     Th1: f is_sequence_on G & ( LSeg ((G * (i,j)),(G * (i,k)))) meets ( L~ f) & [i, j] in ( Indices G) & [i, k] in ( Indices G) & j <= k implies ex n st j <= n & n <= k & ((G * (i,n)) `2 ) = ( lower_bound ( proj2 .: (( LSeg ((G * (i,j)),(G * (i,k)))) /\ ( L~ f))))

    proof

      set X = (( LSeg ((G * (i,j)),(G * (i,k)))) /\ ( L~ f));

      assume that

       A1: f is_sequence_on G and

       A2: ( LSeg ((G * (i,j)),(G * (i,k)))) meets ( L~ f) and

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

       A4: [i, k] in ( Indices G) and

       A5: j <= k;

      

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

      ex x be object st x in ( LSeg ((G * (i,j)),(G * (i,k)))) & x in ( L~ f) by A2, XBOOLE_0: 3;

      then

      reconsider X1 = X as non empty compact Subset of ( TOP-REAL 2) by XBOOLE_0:def 4;

      consider p be object such that

       A7: p in ( S-most X1) by XBOOLE_0:def 1;

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

      

       A8: p in X by A7, XBOOLE_0:def 4;

      then

       A9: p in ( LSeg ((G * (i,j)),(G * (i,k)))) by XBOOLE_0:def 4;

      ( proj2 .: X) = (( proj2 | X) .: X) by RELAT_1: 129;

      

      then

       A10: ( lower_bound ( proj2 .: X)) = ( lower_bound (( proj2 | X) .: ( [#] (( TOP-REAL 2) | X)))) by PRE_TOPC:def 5

      .= ( S-bound X);

      

       A11: 1 <= k by A4, MATRIX_0: 32;

      

       A12: (p `2 ) = (( S-min X) `2 ) by A7, PSCOMP_1: 55

      .= ( lower_bound ( proj2 .: X)) by A10, EUCLID: 52;

      

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

      

       A14: 1 <= j by A3, MATRIX_0: 32;

      

       A15: k <= ( width G) by A4, MATRIX_0: 32;

      then

       A16: ((G * (i,j)) `2 ) <= ((G * (i,k)) `2 ) by A5, A6, A14, SPRECT_3: 12;

      then

       A17: ((G * (i,j)) `2 ) <= (p `2 ) by A9, TOPREAL1: 4;

      

       A18: (p `2 ) <= ((G * (i,k)) `2 ) by A9, A16, TOPREAL1: 4;

      

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

      

      then

       A20: ((G * (i,j)) `1 ) = ((G * (i,1)) `1 ) by A6, A14, GOBOARD5: 2

      .= ((G * (i,k)) `1 ) by A13, A11, A15, GOBOARD5: 2;

      p in ( L~ f) by A8, XBOOLE_0:def 4;

      then p in ( union { ( LSeg (f,k1)) where k1 be Nat : 1 <= k1 & (k1 + 1) <= ( len f) }) by TOPREAL1:def 4;

      then

      consider Y be set such that

       A21: p in Y and

       A22: Y in { ( LSeg (f,k1)) where k1 be Nat : 1 <= k1 & (k1 + 1) <= ( len f) } by TARSKI:def 4;

      consider i1 be Nat such that

       A23: Y = ( LSeg (f,i1)) and

       A24: 1 <= i1 and

       A25: (i1 + 1) <= ( len f) by A22;

      

       A26: p in ( LSeg ((f /. i1),(f /. (i1 + 1)))) by A21, A23, A24, A25, TOPREAL1:def 3;

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

      then (i1 + 1) in ( Seg ( len f)) by A25, FINSEQ_1: 1;

      then

       A27: (i1 + 1) in ( dom f) by FINSEQ_1:def 3;

      then

      consider io,jo be Nat such that

       A28: [io, jo] in ( Indices G) and

       A29: (f /. (i1 + 1)) = (G * (io,jo)) by A1, GOBOARD1:def 9;

      

       A30: 1 <= io & io <= ( len G) by A28, MATRIX_0: 32;

      

       A31: 1 <= jo by A28, MATRIX_0: 32;

      i1 <= ( len f) by A25, NAT_1: 13;

      then i1 in ( Seg ( len f)) by A24, FINSEQ_1: 1;

      then

       A32: i1 in ( dom f) by FINSEQ_1:def 3;

      then

      consider i0,j0 be Nat such that

       A33: [i0, j0] in ( Indices G) and

       A34: (f /. i1) = (G * (i0,j0)) by A1, GOBOARD1:def 9;

      

       A35: 1 <= i0 & i0 <= ( len G) by A33, MATRIX_0: 32;

      

       A36: 1 <= j0 by A33, MATRIX_0: 32;

      

       A37: j0 <= ( width G) by A33, MATRIX_0: 32;

      

       A38: jo <= ( width G) by A28, MATRIX_0: 32;

      

       A39: f is special by A1, A32, JORDAN8: 4, RELAT_1: 38;

      ex n st j <= n & n <= k & (G * (i,n)) = p

      proof

        per cases by A24, A25, A39, TOPREAL1:def 5;

          suppose

           A40: ((f /. i1) `1 ) = ((f /. (i1 + 1)) `1 );

          ((G * (io,j)) `1 ) = ((G * (io,1)) `1 ) by A14, A19, A30, GOBOARD5: 2

          .= ((G * (io,jo)) `1 ) by A30, A31, A38, GOBOARD5: 2

          .= (p `1 ) by A26, A29, A40, GOBOARD7: 5

          .= ((G * (i,j)) `1 ) by A20, A9, GOBOARD7: 5;

          then io <= i & io >= i by A6, A14, A19, A30, GOBOARD5: 3;

          then

           A41: i = io by XXREAL_0: 1;

          ((G * (i0,j)) `1 ) = ((G * (i0,1)) `1 ) by A14, A19, A35, GOBOARD5: 2

          .= ((G * (i0,j0)) `1 ) by A35, A36, A37, GOBOARD5: 2

          .= (p `1 ) by A26, A34, A40, GOBOARD7: 5

          .= ((G * (i,j)) `1 ) by A20, A9, GOBOARD7: 5;

          then i0 <= i & i0 >= i by A6, A14, A19, A35, GOBOARD5: 3;

          then

           A42: i = i0 by XXREAL_0: 1;

          thus thesis

          proof

            per cases ;

              suppose

               A43: ((f /. i1) `2 ) <= ((f /. (i1 + 1)) `2 );

              thus thesis

              proof

                per cases ;

                  suppose

                   A44: (f /. i1) in ( LSeg ((G * (i,j)),(G * (i,k))));

                  (1 + 1) <= (i1 + 1) by A24, XREAL_1: 6;

                  then (f /. i1) in ( L~ f) by A25, A32, GOBOARD1: 1, XXREAL_0: 2;

                  then (f /. i1) in X1 by A44, XBOOLE_0:def 4;

                  then

                   A45: (p `2 ) <= ((f /. i1) `2 ) by A10, A12, PSCOMP_1: 24;

                  take n = j0;

                  

                   A46: p in ( LSeg ((G * (i,j)),(G * (i,k)))) by A8, XBOOLE_0:def 4;

                  (p `2 ) >= ((f /. i1) `2 ) by A26, A43, TOPREAL1: 4;

                  then (p `2 ) = ((f /. i1) `2 ) by A45, XXREAL_0: 1;

                  

                  then

                   A47: (p `2 ) = ((G * (1,j0)) `2 ) by A34, A35, A36, A37, GOBOARD5: 1

                  .= ((G * (i,n)) `2 ) by A6, A36, A37, GOBOARD5: 1;

                  

                   A48: ((G * (i,j)) `2 ) <= ((G * (i,k)) `2 ) by A5, A6, A14, A15, SPRECT_3: 12;

                  then ((G * (i,j)) `2 ) <= ((G * (i,n)) `2 ) by A46, A47, TOPREAL1: 4;

                  hence j <= n by A6, A19, A36, GOBOARD5: 4;

                  ((G * (i,n)) `2 ) <= ((G * (i,k)) `2 ) by A46, A47, A48, TOPREAL1: 4;

                  hence n <= k by A13, A11, A37, GOBOARD5: 4;

                  (p `1 ) = ((G * (i,j)) `1 ) by A20, A46, GOBOARD7: 5

                  .= ((G * (i,1)) `1 ) by A6, A14, A19, GOBOARD5: 2

                  .= ((G * (i,n)) `1 ) by A6, A36, A37, GOBOARD5: 2;

                  hence thesis by A47, TOPREAL3: 6;

                end;

                  suppose

                   A49: not (f /. i1) in ( LSeg ((G * (i,j)),(G * (i,k))));

                  

                   A50: ((f /. i1) `1 ) = (p `1 ) by A26, A40, GOBOARD7: 5

                  .= ((G * (i,j)) `1 ) by A20, A9, GOBOARD7: 5;

                  thus thesis

                  proof

                    per cases by A20, A49, A50, GOBOARD7: 7;

                      suppose

                       A51: ((f /. i1) `2 ) < ((G * (i,j)) `2 );

                      (p `2 ) <= ((G * (io,jo)) `2 ) by A26, A29, A43, TOPREAL1: 4;

                      then (p `2 ) <= ((G * (1,jo)) `2 ) by A30, A31, A38, GOBOARD5: 1;

                      then (p `2 ) <= ((G * (i,jo)) `2 ) by A6, A31, A38, GOBOARD5: 1;

                      then ((G * (i,j)) `2 ) <= ((G * (i,jo)) `2 ) by A17, XXREAL_0: 2;

                      then

                       A52: j <= jo by A6, A19, A31, GOBOARD5: 4;

                      ( |.(i0 - io).| + |.(j0 - jo).|) = 1 by A1, A32, A27, A33, A34, A28, A29, GOBOARD1:def 9;

                      then ( 0 + |.(j0 - jo).|) = 1 by A42, A41, ABSVALUE: 2;

                      then

                       A53: |.( - (j0 - jo)).| = 1 by COMPLEX1: 52;

                      j0 <= (jo + 0 ) by A34, A29, A35, A37, A31, A42, A41, A43, GOBOARD5: 4;

                      then (j0 - jo) <= 0 by XREAL_1: 20;

                      then (jo - j0) = 1 by A53, ABSVALUE:def 1;

                      then

                       A54: (j0 + 1) = (jo + 0 );

                      ((G * (i,j0)) `2 ) < ((G * (i,j)) `2 ) & j0 <= j by A34, A6, A14, A37, A42, A51, GOBOARD5: 4;

                      then j0 < j by XXREAL_0: 1;

                      then jo <= j by A54, NAT_1: 13;

                      then

                       A55: j = jo by A52, XXREAL_0: 1;

                      take n = jo;

                      

                       A56: (p `1 ) = ((G * (i,j)) `1 ) by A20, A9, GOBOARD7: 5

                      .= ((G * (i,1)) `1 ) by A6, A14, A19, GOBOARD5: 2

                      .= ((G * (i,n)) `1 ) by A6, A31, A38, GOBOARD5: 2;

                      (p `2 ) <= ((G * (io,jo)) `2 ) by A26, A29, A43, TOPREAL1: 4;

                      then (p `2 ) <= ((G * (1,jo)) `2 ) by A30, A31, A38, GOBOARD5: 1;

                      then (p `2 ) <= ((G * (i,jo)) `2 ) by A6, A31, A38, GOBOARD5: 1;

                      then (p `2 ) = ((G * (i,j)) `2 ) by A17, A55, XXREAL_0: 1;

                      hence thesis by A5, A55, A56, TOPREAL3: 6;

                    end;

                      suppose

                       A57: ((f /. i1) `2 ) > ((G * (i,k)) `2 );

                      (p `2 ) >= ((f /. i1) `2 ) by A26, A43, TOPREAL1: 4;

                      hence thesis by A18, A57, XXREAL_0: 2;

                    end;

                  end;

                end;

              end;

            end;

              suppose

               A58: ((f /. i1) `2 ) > ((f /. (i1 + 1)) `2 );

              thus thesis

              proof

                per cases ;

                  suppose

                   A59: (f /. (i1 + 1)) in ( LSeg ((G * (i,j)),(G * (i,k))));

                  (1 + 1) <= (i1 + 1) by A24, XREAL_1: 6;

                  then (f /. (i1 + 1)) in ( L~ f) by A25, A27, GOBOARD1: 1, XXREAL_0: 2;

                  then (f /. (i1 + 1)) in X1 by A59, XBOOLE_0:def 4;

                  then

                   A60: (p `2 ) <= ((f /. (i1 + 1)) `2 ) by A10, A12, PSCOMP_1: 24;

                  take n = jo;

                  

                   A61: p in ( LSeg ((G * (i,j)),(G * (i,k)))) by A8, XBOOLE_0:def 4;

                  (p `2 ) >= ((f /. (i1 + 1)) `2 ) by A26, A58, TOPREAL1: 4;

                  then (p `2 ) = ((f /. (i1 + 1)) `2 ) by A60, XXREAL_0: 1;

                  

                  then

                   A62: (p `2 ) = ((G * (1,jo)) `2 ) by A29, A30, A31, A38, GOBOARD5: 1

                  .= ((G * (i,n)) `2 ) by A6, A31, A38, GOBOARD5: 1;

                  

                   A63: ((G * (i,j)) `2 ) <= ((G * (i,k)) `2 ) by A5, A6, A14, A15, SPRECT_3: 12;

                  then ((G * (i,j)) `2 ) <= ((G * (i,n)) `2 ) by A61, A62, TOPREAL1: 4;

                  hence j <= n by A6, A19, A31, GOBOARD5: 4;

                  ((G * (i,n)) `2 ) <= ((G * (i,k)) `2 ) by A61, A62, A63, TOPREAL1: 4;

                  hence n <= k by A13, A11, A38, GOBOARD5: 4;

                  (p `1 ) = ((G * (i,j)) `1 ) by A20, A61, GOBOARD7: 5

                  .= ((G * (i,1)) `1 ) by A6, A14, A19, GOBOARD5: 2

                  .= ((G * (i,n)) `1 ) by A6, A31, A38, GOBOARD5: 2;

                  hence thesis by A62, TOPREAL3: 6;

                end;

                  suppose

                   A64: not (f /. (i1 + 1)) in ( LSeg ((G * (i,j)),(G * (i,k))));

                  

                   A65: ((f /. (i1 + 1)) `1 ) = (p `1 ) by A26, A40, GOBOARD7: 5

                  .= ((G * (i,j)) `1 ) by A20, A9, GOBOARD7: 5;

                  thus thesis

                  proof

                    per cases by A20, A64, A65, GOBOARD7: 7;

                      suppose

                       A66: ((f /. (i1 + 1)) `2 ) < ((G * (i,j)) `2 );

                      (p `2 ) <= ((G * (i0,j0)) `2 ) by A26, A34, A58, TOPREAL1: 4;

                      then (p `2 ) <= ((G * (1,j0)) `2 ) by A35, A36, A37, GOBOARD5: 1;

                      then (p `2 ) <= ((G * (i,j0)) `2 ) by A6, A36, A37, GOBOARD5: 1;

                      then ((G * (i,j)) `2 ) <= ((G * (i,j0)) `2 ) by A17, XXREAL_0: 2;

                      then

                       A67: j <= j0 by A6, A19, A36, GOBOARD5: 4;

                      jo <= (j0 + 0 ) by A34, A29, A35, A36, A38, A42, A41, A58, GOBOARD5: 4;

                      then (jo - j0) <= 0 by XREAL_1: 20;

                      then

                       A68: ( - (jo - j0)) >= ( - 0 );

                      ( |.(i0 - io).| + |.(j0 - jo).|) = 1 by A1, A32, A27, A33, A34, A28, A29, GOBOARD1:def 9;

                      then ( 0 + |.(j0 - jo).|) = 1 by A42, A41, ABSVALUE: 2;

                      then (j0 - jo) = 1 by A68, ABSVALUE:def 1;

                      then

                       A69: (jo + 1) = (j0 - 0 );

                      ((G * (i,jo)) `2 ) < ((G * (i,j)) `2 ) & jo <= j by A29, A6, A14, A38, A41, A66, GOBOARD5: 4;

                      then jo < j by XXREAL_0: 1;

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

                      then

                       A70: j = j0 by A67, XXREAL_0: 1;

                      take n = j0;

                      

                       A71: (p `1 ) = ((G * (i,j)) `1 ) by A20, A9, GOBOARD7: 5

                      .= ((G * (i,1)) `1 ) by A6, A14, A19, GOBOARD5: 2

                      .= ((G * (i,n)) `1 ) by A6, A36, A37, GOBOARD5: 2;

                      (p `2 ) <= ((G * (i0,j0)) `2 ) by A26, A34, A58, TOPREAL1: 4;

                      then (p `2 ) <= ((G * (1,j0)) `2 ) by A35, A36, A37, GOBOARD5: 1;

                      then (p `2 ) <= ((G * (i,j0)) `2 ) by A6, A36, A37, GOBOARD5: 1;

                      then (p `2 ) = ((G * (i,j)) `2 ) by A17, A70, XXREAL_0: 1;

                      hence thesis by A5, A70, A71, TOPREAL3: 6;

                    end;

                      suppose

                       A72: ((f /. (i1 + 1)) `2 ) > ((G * (i,k)) `2 );

                      (p `2 ) >= ((f /. (i1 + 1)) `2 ) by A26, A58, TOPREAL1: 4;

                      hence thesis by A18, A72, XXREAL_0: 2;

                    end;

                  end;

                end;

              end;

            end;

          end;

        end;

          suppose

           A73: ((f /. i1) `2 ) = ((f /. (i1 + 1)) `2 );

          take n = j0;

          (p `2 ) = ((f /. i1) `2 ) by A26, A73, GOBOARD7: 6;

          

          then

           A74: (p `2 ) = ((G * (1,j0)) `2 ) by A34, A35, A36, A37, GOBOARD5: 1

          .= ((G * (i,n)) `2 ) by A6, A36, A37, GOBOARD5: 1;

          

           A75: ((G * (i,j)) `2 ) <= ((G * (i,k)) `2 ) by A5, A6, A14, A15, SPRECT_3: 12;

          then ((G * (i,j)) `2 ) <= ((G * (i,n)) `2 ) by A9, A74, TOPREAL1: 4;

          hence j <= n by A6, A19, A36, GOBOARD5: 4;

          ((G * (i,n)) `2 ) <= ((G * (i,k)) `2 ) by A9, A74, A75, TOPREAL1: 4;

          hence n <= k by A13, A11, A37, GOBOARD5: 4;

          (p `1 ) = ((G * (i,j)) `1 ) by A20, A9, GOBOARD7: 5

          .= ((G * (i,1)) `1 ) by A6, A14, A19, GOBOARD5: 2

          .= ((G * (i,n)) `1 ) by A6, A36, A37, GOBOARD5: 2;

          hence thesis by A74, TOPREAL3: 6;

        end;

      end;

      hence thesis by A12;

    end;

    theorem :: JORDAN1F:2

    f is_sequence_on G & ( LSeg ((G * (i,j)),(G * (i,k)))) meets ( L~ f) & [i, j] in ( Indices G) & [i, k] in ( Indices G) & j <= k implies ex n st j <= n & n <= k & ((G * (i,n)) `2 ) = ( upper_bound ( proj2 .: (( LSeg ((G * (i,j)),(G * (i,k)))) /\ ( L~ f))))

    proof

      set X = (( LSeg ((G * (i,j)),(G * (i,k)))) /\ ( L~ f));

      assume that

       A1: f is_sequence_on G and

       A2: ( LSeg ((G * (i,j)),(G * (i,k)))) meets ( L~ f) and

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

       A4: [i, k] in ( Indices G) and

       A5: j <= k;

      

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

      ex x be object st x in ( LSeg ((G * (i,j)),(G * (i,k)))) & x in ( L~ f) by A2, XBOOLE_0: 3;

      then

      reconsider X1 = X as non empty compact Subset of ( TOP-REAL 2) by XBOOLE_0:def 4;

      consider p be object such that

       A7: p in ( N-most X1) by XBOOLE_0:def 1;

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

      

       A8: p in X by A7, XBOOLE_0:def 4;

      then

       A9: p in ( LSeg ((G * (i,j)),(G * (i,k)))) by XBOOLE_0:def 4;

      p in ( L~ f) by A8, XBOOLE_0:def 4;

      then p in ( union { ( LSeg (f,k1)) where k1 be Nat : 1 <= k1 & (k1 + 1) <= ( len f) }) by TOPREAL1:def 4;

      then

      consider Y be set such that

       A10: p in Y and

       A11: Y in { ( LSeg (f,k1)) where k1 be Nat : 1 <= k1 & (k1 + 1) <= ( len f) } by TARSKI:def 4;

      consider i1 be Nat such that

       A12: Y = ( LSeg (f,i1)) and

       A13: 1 <= i1 and

       A14: (i1 + 1) <= ( len f) by A11;

      

       A15: p in ( LSeg ((f /. i1),(f /. (i1 + 1)))) by A10, A12, A13, A14, TOPREAL1:def 3;

      ( proj2 .: X) = (( proj2 | X) .: X) by RELAT_1: 129;

      

      then

       A16: ( upper_bound ( proj2 .: X)) = ( upper_bound (( proj2 | X) .: ( [#] (( TOP-REAL 2) | X)))) by PRE_TOPC:def 5

      .= ( N-bound X);

      

       A17: 1 <= k by A4, MATRIX_0: 32;

      

       A18: 1 <= j by A3, MATRIX_0: 32;

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

      then (i1 + 1) in ( Seg ( len f)) by A14, FINSEQ_1: 1;

      then

       A19: (i1 + 1) in ( dom f) by FINSEQ_1:def 3;

      then

      consider io,jo be Nat such that

       A20: [io, jo] in ( Indices G) and

       A21: (f /. (i1 + 1)) = (G * (io,jo)) by A1, GOBOARD1:def 9;

      

       A22: 1 <= io & io <= ( len G) by A20, MATRIX_0: 32;

      

       A23: 1 <= jo by A20, MATRIX_0: 32;

      

       A24: (p `2 ) = (( N-min X) `2 ) by A7, PSCOMP_1: 39

      .= ( upper_bound ( proj2 .: X)) by A16, EUCLID: 52;

      

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

      

       A26: k <= ( width G) by A4, MATRIX_0: 32;

      then

       A27: ((G * (i,j)) `2 ) <= ((G * (i,k)) `2 ) by A5, A6, A18, SPRECT_3: 12;

      then

       A28: ((G * (i,j)) `2 ) <= (p `2 ) by A9, TOPREAL1: 4;

      

       A29: (p `2 ) <= ((G * (i,k)) `2 ) by A9, A27, TOPREAL1: 4;

      

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

      

      then

       A31: ((G * (i,j)) `1 ) = ((G * (i,1)) `1 ) by A6, A18, GOBOARD5: 2

      .= ((G * (i,k)) `1 ) by A25, A17, A26, GOBOARD5: 2;

      

       A32: jo <= ( width G) by A20, MATRIX_0: 32;

      i1 <= ( len f) by A14, NAT_1: 13;

      then i1 in ( Seg ( len f)) by A13, FINSEQ_1: 1;

      then

       A33: i1 in ( dom f) by FINSEQ_1:def 3;

      then

      consider i0,j0 be Nat such that

       A34: [i0, j0] in ( Indices G) and

       A35: (f /. i1) = (G * (i0,j0)) by A1, GOBOARD1:def 9;

      

       A36: 1 <= i0 & i0 <= ( len G) by A34, MATRIX_0: 32;

      

       A37: 1 <= j0 by A34, MATRIX_0: 32;

      

       A38: j0 <= ( width G) by A34, MATRIX_0: 32;

      

       A39: f is special by A1, A33, JORDAN8: 4, RELAT_1: 38;

      ex n st j <= n & n <= k & (G * (i,n)) = p

      proof

        per cases by A13, A14, A39, TOPREAL1:def 5;

          suppose

           A40: ((f /. i1) `1 ) = ((f /. (i1 + 1)) `1 );

          ((G * (io,j)) `1 ) = ((G * (io,1)) `1 ) by A18, A30, A22, GOBOARD5: 2

          .= ((G * (io,jo)) `1 ) by A22, A23, A32, GOBOARD5: 2

          .= (p `1 ) by A15, A21, A40, GOBOARD7: 5

          .= ((G * (i,j)) `1 ) by A31, A9, GOBOARD7: 5;

          then io <= i & io >= i by A6, A18, A30, A22, GOBOARD5: 3;

          then

           A41: i = io by XXREAL_0: 1;

          ((G * (i0,j)) `1 ) = ((G * (i0,1)) `1 ) by A18, A30, A36, GOBOARD5: 2

          .= ((G * (i0,j0)) `1 ) by A36, A37, A38, GOBOARD5: 2

          .= (p `1 ) by A15, A35, A40, GOBOARD7: 5

          .= ((G * (i,j)) `1 ) by A31, A9, GOBOARD7: 5;

          then i0 <= i & i0 >= i by A6, A18, A30, A36, GOBOARD5: 3;

          then

           A42: i = i0 by XXREAL_0: 1;

          thus thesis

          proof

            per cases ;

              suppose

               A43: ((f /. i1) `2 ) <= ((f /. (i1 + 1)) `2 );

              thus thesis

              proof

                per cases ;

                  suppose

                   A44: (f /. (i1 + 1)) in ( LSeg ((G * (i,j)),(G * (i,k))));

                  (1 + 1) <= (i1 + 1) by A13, XREAL_1: 6;

                  then (f /. (i1 + 1)) in ( L~ f) by A14, A19, GOBOARD1: 1, XXREAL_0: 2;

                  then (f /. (i1 + 1)) in X1 by A44, XBOOLE_0:def 4;

                  then

                   A45: (p `2 ) >= ((f /. (i1 + 1)) `2 ) by A16, A24, PSCOMP_1: 24;

                  take n = jo;

                  

                   A46: p in ( LSeg ((G * (i,j)),(G * (i,k)))) by A8, XBOOLE_0:def 4;

                  (p `2 ) <= ((f /. (i1 + 1)) `2 ) by A15, A43, TOPREAL1: 4;

                  then (p `2 ) = ((f /. (i1 + 1)) `2 ) by A45, XXREAL_0: 1;

                  

                  then

                   A47: (p `2 ) = ((G * (1,jo)) `2 ) by A21, A22, A23, A32, GOBOARD5: 1

                  .= ((G * (i,n)) `2 ) by A6, A23, A32, GOBOARD5: 1;

                  

                   A48: ((G * (i,j)) `2 ) <= ((G * (i,k)) `2 ) by A5, A6, A18, A26, SPRECT_3: 12;

                  then ((G * (i,j)) `2 ) <= ((G * (i,n)) `2 ) by A46, A47, TOPREAL1: 4;

                  hence j <= n by A6, A30, A23, GOBOARD5: 4;

                  ((G * (i,n)) `2 ) <= ((G * (i,k)) `2 ) by A46, A47, A48, TOPREAL1: 4;

                  hence n <= k by A25, A17, A32, GOBOARD5: 4;

                  (p `1 ) = ((G * (i,j)) `1 ) by A31, A46, GOBOARD7: 5

                  .= ((G * (i,1)) `1 ) by A6, A18, A30, GOBOARD5: 2

                  .= ((G * (i,n)) `1 ) by A6, A23, A32, GOBOARD5: 2;

                  hence thesis by A47, TOPREAL3: 6;

                end;

                  suppose

                   A49: not (f /. (i1 + 1)) in ( LSeg ((G * (i,j)),(G * (i,k))));

                  

                   A50: ((f /. (i1 + 1)) `1 ) = (p `1 ) by A15, A40, GOBOARD7: 5

                  .= ((G * (i,j)) `1 ) by A31, A9, GOBOARD7: 5;

                  thus thesis

                  proof

                    per cases by A31, A49, A50, GOBOARD7: 7;

                      suppose

                       A51: ((f /. (i1 + 1)) `2 ) > ((G * (i,k)) `2 );

                      (p `2 ) >= ((G * (i0,j0)) `2 ) by A15, A35, A43, TOPREAL1: 4;

                      then (p `2 ) >= ((G * (1,j0)) `2 ) by A36, A37, A38, GOBOARD5: 1;

                      then (p `2 ) >= ((G * (i,j0)) `2 ) by A6, A37, A38, GOBOARD5: 1;

                      then ((G * (i,k)) `2 ) >= ((G * (i,j0)) `2 ) by A29, XXREAL_0: 2;

                      then

                       A52: k >= j0 by A25, A17, A38, GOBOARD5: 4;

                      ( |.(i0 - io).| + |.(j0 - jo).|) = 1 by A1, A33, A19, A34, A35, A20, A21, GOBOARD1:def 9;

                      then ( 0 + |.(j0 - jo).|) = 1 by A42, A41, ABSVALUE: 2;

                      then

                       A53: |.( - (j0 - jo)).| = 1 by COMPLEX1: 52;

                      j0 <= (jo + 0 ) by A35, A21, A36, A38, A23, A42, A41, A43, GOBOARD5: 4;

                      then (j0 - jo) <= 0 by XREAL_1: 20;

                      then (jo - j0) = 1 by A53, ABSVALUE:def 1;

                      then

                       A54: (j0 + 1) = (jo + 0 );

                      ((G * (i,jo)) `2 ) > ((G * (i,k)) `2 ) & jo >= k by A21, A25, A26, A23, A41, A51, GOBOARD5: 4;

                      then jo > k by XXREAL_0: 1;

                      then j0 >= k by A54, NAT_1: 13;

                      then

                       A55: k = j0 by A52, XXREAL_0: 1;

                      take n = j0;

                      

                       A56: (p `1 ) = ((G * (i,j)) `1 ) by A31, A9, GOBOARD7: 5

                      .= ((G * (i,1)) `1 ) by A6, A18, A30, GOBOARD5: 2

                      .= ((G * (i,n)) `1 ) by A6, A37, A38, GOBOARD5: 2;

                      (p `2 ) >= ((G * (i0,j0)) `2 ) by A15, A35, A43, TOPREAL1: 4;

                      then (p `2 ) >= ((G * (1,j0)) `2 ) by A36, A37, A38, GOBOARD5: 1;

                      then (p `2 ) >= ((G * (i,j0)) `2 ) by A6, A37, A38, GOBOARD5: 1;

                      then (p `2 ) = ((G * (i,k)) `2 ) by A29, A55, XXREAL_0: 1;

                      hence thesis by A5, A55, A56, TOPREAL3: 6;

                    end;

                      suppose

                       A57: ((f /. (i1 + 1)) `2 ) < ((G * (i,j)) `2 );

                      (p `2 ) <= ((f /. (i1 + 1)) `2 ) by A15, A43, TOPREAL1: 4;

                      hence thesis by A28, A57, XXREAL_0: 2;

                    end;

                  end;

                end;

              end;

            end;

              suppose

               A58: ((f /. i1) `2 ) > ((f /. (i1 + 1)) `2 );

              thus thesis

              proof

                per cases ;

                  suppose

                   A59: (f /. i1) in ( LSeg ((G * (i,j)),(G * (i,k))));

                  (1 + 1) <= (i1 + 1) by A13, XREAL_1: 6;

                  then (f /. i1) in ( L~ f) by A14, A33, GOBOARD1: 1, XXREAL_0: 2;

                  then (f /. i1) in X1 by A59, XBOOLE_0:def 4;

                  then

                   A60: (p `2 ) >= ((f /. i1) `2 ) by A16, A24, PSCOMP_1: 24;

                  take n = j0;

                  

                   A61: p in ( LSeg ((G * (i,j)),(G * (i,k)))) by A8, XBOOLE_0:def 4;

                  (p `2 ) <= ((f /. i1) `2 ) by A15, A58, TOPREAL1: 4;

                  then (p `2 ) = ((f /. i1) `2 ) by A60, XXREAL_0: 1;

                  

                  then

                   A62: (p `2 ) = ((G * (1,j0)) `2 ) by A35, A36, A37, A38, GOBOARD5: 1

                  .= ((G * (i,n)) `2 ) by A6, A37, A38, GOBOARD5: 1;

                  

                   A63: ((G * (i,j)) `2 ) <= ((G * (i,k)) `2 ) by A5, A6, A18, A26, SPRECT_3: 12;

                  then ((G * (i,j)) `2 ) <= ((G * (i,n)) `2 ) by A61, A62, TOPREAL1: 4;

                  hence j <= n by A6, A30, A37, GOBOARD5: 4;

                  ((G * (i,n)) `2 ) <= ((G * (i,k)) `2 ) by A61, A62, A63, TOPREAL1: 4;

                  hence n <= k by A25, A17, A38, GOBOARD5: 4;

                  (p `1 ) = ((G * (i,j)) `1 ) by A31, A61, GOBOARD7: 5

                  .= ((G * (i,1)) `1 ) by A6, A18, A30, GOBOARD5: 2

                  .= ((G * (i,n)) `1 ) by A6, A37, A38, GOBOARD5: 2;

                  hence thesis by A62, TOPREAL3: 6;

                end;

                  suppose

                   A64: not (f /. i1) in ( LSeg ((G * (i,j)),(G * (i,k))));

                  

                   A65: ((f /. i1) `1 ) = (p `1 ) by A15, A40, GOBOARD7: 5

                  .= ((G * (i,j)) `1 ) by A31, A9, GOBOARD7: 5;

                  thus thesis

                  proof

                    per cases by A31, A64, A65, GOBOARD7: 7;

                      suppose

                       A66: ((f /. i1) `2 ) > ((G * (i,k)) `2 );

                      (p `2 ) >= ((G * (io,jo)) `2 ) by A15, A21, A58, TOPREAL1: 4;

                      then (p `2 ) >= ((G * (1,jo)) `2 ) by A22, A23, A32, GOBOARD5: 1;

                      then (p `2 ) >= ((G * (i,jo)) `2 ) by A6, A23, A32, GOBOARD5: 1;

                      then ((G * (i,k)) `2 ) >= ((G * (i,jo)) `2 ) by A29, XXREAL_0: 2;

                      then

                       A67: k >= jo by A25, A17, A32, GOBOARD5: 4;

                      jo <= (j0 + 0 ) by A35, A21, A36, A37, A32, A42, A41, A58, GOBOARD5: 4;

                      then (jo - j0) <= 0 by XREAL_1: 20;

                      then

                       A68: ( - (jo - j0)) >= ( - 0 );

                      ( |.(i0 - io).| + |.(j0 - jo).|) = 1 by A1, A33, A19, A34, A35, A20, A21, GOBOARD1:def 9;

                      then ( 0 + |.(j0 - jo).|) = 1 by A42, A41, ABSVALUE: 2;

                      then (j0 - jo) = 1 by A68, ABSVALUE:def 1;

                      then

                       A69: (jo + 1) = (j0 - 0 );

                      ((G * (i,j0)) `2 ) > ((G * (i,k)) `2 ) & j0 >= k by A35, A25, A26, A37, A42, A66, GOBOARD5: 4;

                      then j0 > k by XXREAL_0: 1;

                      then jo >= k by A69, NAT_1: 13;

                      then

                       A70: k = jo by A67, XXREAL_0: 1;

                      take n = jo;

                      

                       A71: (p `1 ) = ((G * (i,j)) `1 ) by A31, A9, GOBOARD7: 5

                      .= ((G * (i,1)) `1 ) by A6, A18, A30, GOBOARD5: 2

                      .= ((G * (i,n)) `1 ) by A6, A23, A32, GOBOARD5: 2;

                      (p `2 ) >= ((G * (io,jo)) `2 ) by A15, A21, A58, TOPREAL1: 4;

                      then (p `2 ) >= ((G * (1,jo)) `2 ) by A22, A23, A32, GOBOARD5: 1;

                      then (p `2 ) >= ((G * (i,jo)) `2 ) by A6, A23, A32, GOBOARD5: 1;

                      then (p `2 ) = ((G * (i,k)) `2 ) by A29, A70, XXREAL_0: 1;

                      hence thesis by A5, A70, A71, TOPREAL3: 6;

                    end;

                      suppose

                       A72: ((f /. i1) `2 ) < ((G * (i,j)) `2 );

                      (p `2 ) <= ((f /. i1) `2 ) by A15, A58, TOPREAL1: 4;

                      hence thesis by A28, A72, XXREAL_0: 2;

                    end;

                  end;

                end;

              end;

            end;

          end;

        end;

          suppose

           A73: ((f /. i1) `2 ) = ((f /. (i1 + 1)) `2 );

          take n = j0;

          (p `2 ) = ((f /. i1) `2 ) by A15, A73, GOBOARD7: 6;

          

          then

           A74: (p `2 ) = ((G * (1,j0)) `2 ) by A35, A36, A37, A38, GOBOARD5: 1

          .= ((G * (i,n)) `2 ) by A6, A37, A38, GOBOARD5: 1;

          

           A75: ((G * (i,j)) `2 ) <= ((G * (i,k)) `2 ) by A5, A6, A18, A26, SPRECT_3: 12;

          then ((G * (i,j)) `2 ) <= ((G * (i,n)) `2 ) by A9, A74, TOPREAL1: 4;

          hence j <= n by A6, A30, A37, GOBOARD5: 4;

          ((G * (i,n)) `2 ) <= ((G * (i,k)) `2 ) by A9, A74, A75, TOPREAL1: 4;

          hence n <= k by A25, A17, A38, GOBOARD5: 4;

          (p `1 ) = ((G * (i,j)) `1 ) by A31, A9, GOBOARD7: 5

          .= ((G * (i,1)) `1 ) by A6, A18, A30, GOBOARD5: 2

          .= ((G * (i,n)) `1 ) by A6, A37, A38, GOBOARD5: 2;

          hence thesis by A74, TOPREAL3: 6;

        end;

      end;

      hence thesis by A24;

    end;

    theorem :: JORDAN1F:3

    f is_sequence_on G & ( LSeg ((G * (j,i)),(G * (k,i)))) meets ( L~ f) & [j, i] in ( Indices G) & [k, i] in ( Indices G) & j <= k implies ex n st j <= n & n <= k & ((G * (n,i)) `1 ) = ( lower_bound ( proj1 .: (( LSeg ((G * (j,i)),(G * (k,i)))) /\ ( L~ f))))

    proof

      set X = (( LSeg ((G * (j,i)),(G * (k,i)))) /\ ( L~ f));

      assume that

       A1: f is_sequence_on G and

       A2: ( LSeg ((G * (j,i)),(G * (k,i)))) meets ( L~ f) and

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

       A4: [k, i] in ( Indices G) and

       A5: j <= k;

      

       A6: 1 <= j by A3, MATRIX_0: 32;

      ex x be object st x in ( LSeg ((G * (j,i)),(G * (k,i)))) & x in ( L~ f) by A2, XBOOLE_0: 3;

      then

      reconsider X1 = X as non empty compact Subset of ( TOP-REAL 2) by XBOOLE_0:def 4;

      consider p be object such that

       A7: p in ( W-most X1) by XBOOLE_0:def 1;

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

      

       A8: p in X by A7, XBOOLE_0:def 4;

      then

       A9: p in ( LSeg ((G * (j,i)),(G * (k,i)))) by XBOOLE_0:def 4;

      ( proj1 .: X) = (( proj1 | X) .: X) by RELAT_1: 129;

      

      then

       A10: ( lower_bound ( proj1 .: X)) = ( lower_bound (( proj1 | X) .: ( [#] (( TOP-REAL 2) | X)))) by PRE_TOPC:def 5

      .= ( W-bound X);

      

       A11: 1 <= k & 1 <= i by A4, MATRIX_0: 32;

      

       A12: (p `1 ) = (( W-min X) `1 ) by A7, PSCOMP_1: 31

      .= ( lower_bound ( proj1 .: X)) by A10, EUCLID: 52;

      

       A13: i <= ( width G) by A3, MATRIX_0: 32;

      

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

      

       A15: k <= ( len G) by A4, MATRIX_0: 32;

      then

       A16: ((G * (j,i)) `1 ) <= ((G * (k,i)) `1 ) by A5, A6, A14, SPRECT_3: 13;

      then

       A17: ((G * (j,i)) `1 ) <= (p `1 ) by A9, TOPREAL1: 3;

      

       A18: (p `1 ) <= ((G * (k,i)) `1 ) by A9, A16, TOPREAL1: 3;

      

       A19: j <= ( len G) by A3, MATRIX_0: 32;

      

      then

       A20: ((G * (j,i)) `2 ) = ((G * (1,i)) `2 ) by A6, A14, GOBOARD5: 1

      .= ((G * (k,i)) `2 ) by A15, A11, A13, GOBOARD5: 1;

      p in ( L~ f) by A8, XBOOLE_0:def 4;

      then p in ( union { ( LSeg (f,k1)) where k1 be Nat : 1 <= k1 & (k1 + 1) <= ( len f) }) by TOPREAL1:def 4;

      then

      consider Y be set such that

       A21: p in Y and

       A22: Y in { ( LSeg (f,k1)) where k1 be Nat : 1 <= k1 & (k1 + 1) <= ( len f) } by TARSKI:def 4;

      consider i1 be Nat such that

       A23: Y = ( LSeg (f,i1)) and

       A24: 1 <= i1 and

       A25: (i1 + 1) <= ( len f) by A22;

      

       A26: p in ( LSeg ((f /. i1),(f /. (i1 + 1)))) by A21, A23, A24, A25, TOPREAL1:def 3;

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

      then (i1 + 1) in ( Seg ( len f)) by A25, FINSEQ_1: 1;

      then

       A27: (i1 + 1) in ( dom f) by FINSEQ_1:def 3;

      then

      consider jo,io be Nat such that

       A28: [jo, io] in ( Indices G) and

       A29: (f /. (i1 + 1)) = (G * (jo,io)) by A1, GOBOARD1:def 9;

      

       A30: 1 <= jo by A28, MATRIX_0: 32;

      i1 <= ( len f) by A25, NAT_1: 13;

      then i1 in ( Seg ( len f)) by A24, FINSEQ_1: 1;

      then

       A31: i1 in ( dom f) by FINSEQ_1:def 3;

      then

      consider j0,i0 be Nat such that

       A32: [j0, i0] in ( Indices G) and

       A33: (f /. i1) = (G * (j0,i0)) by A1, GOBOARD1:def 9;

      

       A34: 1 <= j0 by A32, MATRIX_0: 32;

      

       A35: 1 <= i0 & i0 <= ( width G) by A32, MATRIX_0: 32;

      

       A36: j0 <= ( len G) by A32, MATRIX_0: 32;

      

       A37: 1 <= io & io <= ( width G) by A28, MATRIX_0: 32;

      

       A38: jo <= ( len G) by A28, MATRIX_0: 32;

      

       A39: f is special by A1, A31, JORDAN8: 4, RELAT_1: 38;

      ex n st j <= n & n <= k & (G * (n,i)) = p

      proof

        per cases by A24, A25, A39, TOPREAL1:def 5;

          suppose

           A40: ((f /. i1) `2 ) = ((f /. (i1 + 1)) `2 );

          ((G * (j,io)) `2 ) = ((G * (1,io)) `2 ) by A6, A19, A37, GOBOARD5: 1

          .= ((G * (jo,io)) `2 ) by A30, A38, A37, GOBOARD5: 1

          .= (p `2 ) by A26, A29, A40, GOBOARD7: 6

          .= ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6;

          then io <= i & io >= i by A6, A19, A14, A37, GOBOARD5: 4;

          then

           A41: i = io by XXREAL_0: 1;

          ((G * (j,i0)) `2 ) = ((G * (1,i0)) `2 ) by A6, A19, A35, GOBOARD5: 1

          .= ((G * (j0,i0)) `2 ) by A34, A36, A35, GOBOARD5: 1

          .= (p `2 ) by A26, A33, A40, GOBOARD7: 6

          .= ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6;

          then i0 <= i & i0 >= i by A6, A19, A14, A35, GOBOARD5: 4;

          then

           A42: i = i0 by XXREAL_0: 1;

          thus thesis

          proof

            per cases ;

              suppose

               A43: ((f /. i1) `1 ) <= ((f /. (i1 + 1)) `1 );

              thus thesis

              proof

                per cases ;

                  suppose

                   A44: (f /. i1) in ( LSeg ((G * (j,i)),(G * (k,i))));

                  (1 + 1) <= (i1 + 1) by A24, XREAL_1: 6;

                  then (f /. i1) in ( L~ f) by A25, A31, GOBOARD1: 1, XXREAL_0: 2;

                  then (f /. i1) in X1 by A44, XBOOLE_0:def 4;

                  then

                   A45: (p `1 ) <= ((f /. i1) `1 ) by A10, A12, PSCOMP_1: 24;

                  take n = j0;

                  

                   A46: p in ( LSeg ((G * (j,i)),(G * (k,i)))) by A8, XBOOLE_0:def 4;

                  (p `1 ) >= ((f /. i1) `1 ) by A26, A43, TOPREAL1: 3;

                  then (p `1 ) = ((f /. i1) `1 ) by A45, XXREAL_0: 1;

                  

                  then

                   A47: (p `1 ) = ((G * (j0,1)) `1 ) by A33, A34, A36, A35, GOBOARD5: 2

                  .= ((G * (n,i)) `1 ) by A14, A34, A36, GOBOARD5: 2;

                  

                   A48: ((G * (j,i)) `1 ) <= ((G * (k,i)) `1 ) by A5, A6, A14, A15, SPRECT_3: 13;

                  then ((G * (j,i)) `1 ) <= ((G * (n,i)) `1 ) by A46, A47, TOPREAL1: 3;

                  hence j <= n by A19, A14, A34, GOBOARD5: 3;

                  ((G * (n,i)) `1 ) <= ((G * (k,i)) `1 ) by A46, A47, A48, TOPREAL1: 3;

                  hence n <= k by A11, A13, A36, GOBOARD5: 3;

                  (p `2 ) = ((G * (j,i)) `2 ) by A20, A46, GOBOARD7: 6

                  .= ((G * (1,i)) `2 ) by A6, A19, A14, GOBOARD5: 1

                  .= ((G * (n,i)) `2 ) by A14, A34, A36, GOBOARD5: 1;

                  hence thesis by A47, TOPREAL3: 6;

                end;

                  suppose

                   A49: not (f /. i1) in ( LSeg ((G * (j,i)),(G * (k,i))));

                  

                   A50: ((f /. i1) `2 ) = (p `2 ) by A26, A40, GOBOARD7: 6

                  .= ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6;

                  thus thesis

                  proof

                    per cases by A20, A49, A50, GOBOARD7: 8;

                      suppose

                       A51: ((f /. i1) `1 ) < ((G * (j,i)) `1 );

                      (p `1 ) <= ((G * (jo,io)) `1 ) by A26, A29, A43, TOPREAL1: 3;

                      then (p `1 ) <= ((G * (jo,1)) `1 ) by A30, A38, A37, GOBOARD5: 2;

                      then (p `1 ) <= ((G * (jo,i)) `1 ) by A14, A30, A38, GOBOARD5: 2;

                      then ((G * (j,i)) `1 ) <= ((G * (jo,i)) `1 ) by A17, XXREAL_0: 2;

                      then

                       A52: j <= jo by A19, A14, A30, GOBOARD5: 3;

                      ( |.(i0 - io).| + |.(j0 - jo).|) = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def 9;

                      then ( 0 + |.(j0 - jo).|) = 1 by A42, A41, ABSVALUE: 2;

                      then

                       A53: |.( - (j0 - jo)).| = 1 by COMPLEX1: 52;

                      j0 <= (jo + 0 ) by A33, A29, A36, A35, A30, A42, A41, A43, GOBOARD5: 3;

                      then (j0 - jo) <= 0 by XREAL_1: 20;

                      then (jo - j0) = 1 by A53, ABSVALUE:def 1;

                      then

                       A54: (j0 + 1) = (jo + 0 );

                      ((G * (j0,i)) `1 ) < ((G * (j,i)) `1 ) & j0 <= j by A33, A6, A14, A36, A42, A51, GOBOARD5: 3;

                      then j0 < j by XXREAL_0: 1;

                      then jo <= j by A54, NAT_1: 13;

                      then

                       A55: j = jo by A52, XXREAL_0: 1;

                      take n = jo;

                      

                       A56: (p `2 ) = ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6

                      .= ((G * (1,i)) `2 ) by A6, A19, A14, GOBOARD5: 1

                      .= ((G * (n,i)) `2 ) by A14, A30, A38, GOBOARD5: 1;

                      (p `1 ) <= ((G * (jo,io)) `1 ) by A26, A29, A43, TOPREAL1: 3;

                      then (p `1 ) <= ((G * (jo,1)) `1 ) by A30, A38, A37, GOBOARD5: 2;

                      then (p `1 ) <= ((G * (jo,i)) `1 ) by A14, A30, A38, GOBOARD5: 2;

                      then (p `1 ) = ((G * (j,i)) `1 ) by A17, A55, XXREAL_0: 1;

                      hence thesis by A5, A55, A56, TOPREAL3: 6;

                    end;

                      suppose

                       A57: ((f /. i1) `1 ) > ((G * (k,i)) `1 );

                      (p `1 ) >= ((f /. i1) `1 ) by A26, A43, TOPREAL1: 3;

                      hence thesis by A18, A57, XXREAL_0: 2;

                    end;

                  end;

                end;

              end;

            end;

              suppose

               A58: ((f /. i1) `1 ) > ((f /. (i1 + 1)) `1 );

              thus thesis

              proof

                per cases ;

                  suppose

                   A59: (f /. (i1 + 1)) in ( LSeg ((G * (j,i)),(G * (k,i))));

                  (1 + 1) <= (i1 + 1) by A24, XREAL_1: 6;

                  then (f /. (i1 + 1)) in ( L~ f) by A25, A27, GOBOARD1: 1, XXREAL_0: 2;

                  then (f /. (i1 + 1)) in X1 by A59, XBOOLE_0:def 4;

                  then

                   A60: (p `1 ) <= ((f /. (i1 + 1)) `1 ) by A10, A12, PSCOMP_1: 24;

                  take n = jo;

                  

                   A61: p in ( LSeg ((G * (j,i)),(G * (k,i)))) by A8, XBOOLE_0:def 4;

                  (p `1 ) >= ((f /. (i1 + 1)) `1 ) by A26, A58, TOPREAL1: 3;

                  then (p `1 ) = ((f /. (i1 + 1)) `1 ) by A60, XXREAL_0: 1;

                  

                  then

                   A62: (p `1 ) = ((G * (jo,1)) `1 ) by A29, A30, A38, A37, GOBOARD5: 2

                  .= ((G * (n,i)) `1 ) by A14, A30, A38, GOBOARD5: 2;

                  

                   A63: ((G * (j,i)) `1 ) <= ((G * (k,i)) `1 ) by A5, A6, A14, A15, SPRECT_3: 13;

                  then ((G * (j,i)) `1 ) <= ((G * (n,i)) `1 ) by A61, A62, TOPREAL1: 3;

                  hence j <= n by A19, A14, A30, GOBOARD5: 3;

                  ((G * (n,i)) `1 ) <= ((G * (k,i)) `1 ) by A61, A62, A63, TOPREAL1: 3;

                  hence n <= k by A11, A13, A38, GOBOARD5: 3;

                  (p `2 ) = ((G * (j,i)) `2 ) by A20, A61, GOBOARD7: 6

                  .= ((G * (1,i)) `2 ) by A6, A19, A14, GOBOARD5: 1

                  .= ((G * (n,i)) `2 ) by A14, A30, A38, GOBOARD5: 1;

                  hence thesis by A62, TOPREAL3: 6;

                end;

                  suppose

                   A64: not (f /. (i1 + 1)) in ( LSeg ((G * (j,i)),(G * (k,i))));

                  

                   A65: ((f /. (i1 + 1)) `2 ) = (p `2 ) by A26, A40, GOBOARD7: 6

                  .= ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6;

                  thus thesis

                  proof

                    per cases by A20, A64, A65, GOBOARD7: 8;

                      suppose

                       A66: ((f /. (i1 + 1)) `1 ) < ((G * (j,i)) `1 );

                      (p `1 ) <= ((G * (j0,i0)) `1 ) by A26, A33, A58, TOPREAL1: 3;

                      then (p `1 ) <= ((G * (j0,1)) `1 ) by A34, A36, A35, GOBOARD5: 2;

                      then (p `1 ) <= ((G * (j0,i)) `1 ) by A14, A34, A36, GOBOARD5: 2;

                      then ((G * (j,i)) `1 ) <= ((G * (j0,i)) `1 ) by A17, XXREAL_0: 2;

                      then

                       A67: j <= j0 by A19, A14, A34, GOBOARD5: 3;

                      jo <= (j0 + 0 ) by A33, A29, A34, A35, A38, A42, A41, A58, GOBOARD5: 3;

                      then (jo - j0) <= 0 by XREAL_1: 20;

                      then

                       A68: ( - (jo - j0)) >= ( - 0 );

                      ( |.(i0 - io).| + |.(j0 - jo).|) = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def 9;

                      then ( 0 + |.(j0 - jo).|) = 1 by A42, A41, ABSVALUE: 2;

                      then (j0 - jo) = 1 by A68, ABSVALUE:def 1;

                      then

                       A69: (jo + 1) = (j0 - 0 );

                      ((G * (jo,i)) `1 ) < ((G * (j,i)) `1 ) & jo <= j by A29, A6, A14, A38, A41, A66, GOBOARD5: 3;

                      then jo < j by XXREAL_0: 1;

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

                      then

                       A70: j = j0 by A67, XXREAL_0: 1;

                      take n = j0;

                      

                       A71: (p `2 ) = ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6

                      .= ((G * (1,i)) `2 ) by A6, A19, A14, GOBOARD5: 1

                      .= ((G * (n,i)) `2 ) by A14, A34, A36, GOBOARD5: 1;

                      (p `1 ) <= ((G * (j0,i0)) `1 ) by A26, A33, A58, TOPREAL1: 3;

                      then (p `1 ) <= ((G * (j0,1)) `1 ) by A34, A36, A35, GOBOARD5: 2;

                      then (p `1 ) <= ((G * (j0,i)) `1 ) by A14, A34, A36, GOBOARD5: 2;

                      then (p `1 ) = ((G * (j,i)) `1 ) by A17, A70, XXREAL_0: 1;

                      hence thesis by A5, A70, A71, TOPREAL3: 6;

                    end;

                      suppose

                       A72: ((f /. (i1 + 1)) `1 ) > ((G * (k,i)) `1 );

                      (p `1 ) >= ((f /. (i1 + 1)) `1 ) by A26, A58, TOPREAL1: 3;

                      hence thesis by A18, A72, XXREAL_0: 2;

                    end;

                  end;

                end;

              end;

            end;

          end;

        end;

          suppose

           A73: ((f /. i1) `1 ) = ((f /. (i1 + 1)) `1 );

          take n = j0;

          (p `1 ) = ((f /. i1) `1 ) by A26, A73, GOBOARD7: 5;

          

          then

           A74: (p `1 ) = ((G * (j0,1)) `1 ) by A33, A34, A36, A35, GOBOARD5: 2

          .= ((G * (n,i)) `1 ) by A14, A34, A36, GOBOARD5: 2;

          

           A75: ((G * (j,i)) `1 ) <= ((G * (k,i)) `1 ) by A5, A6, A14, A15, SPRECT_3: 13;

          then ((G * (j,i)) `1 ) <= ((G * (n,i)) `1 ) by A9, A74, TOPREAL1: 3;

          hence j <= n by A19, A14, A34, GOBOARD5: 3;

          ((G * (n,i)) `1 ) <= ((G * (k,i)) `1 ) by A9, A74, A75, TOPREAL1: 3;

          hence n <= k by A11, A13, A36, GOBOARD5: 3;

          (p `2 ) = ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6

          .= ((G * (1,i)) `2 ) by A6, A19, A14, GOBOARD5: 1

          .= ((G * (n,i)) `2 ) by A14, A34, A36, GOBOARD5: 1;

          hence thesis by A74, TOPREAL3: 6;

        end;

      end;

      hence thesis by A12;

    end;

    theorem :: JORDAN1F:4

    f is_sequence_on G & ( LSeg ((G * (j,i)),(G * (k,i)))) meets ( L~ f) & [j, i] in ( Indices G) & [k, i] in ( Indices G) & j <= k implies ex n st j <= n & n <= k & ((G * (n,i)) `1 ) = ( upper_bound ( proj1 .: (( LSeg ((G * (j,i)),(G * (k,i)))) /\ ( L~ f))))

    proof

      set X = (( LSeg ((G * (j,i)),(G * (k,i)))) /\ ( L~ f));

      assume that

       A1: f is_sequence_on G and

       A2: ( LSeg ((G * (j,i)),(G * (k,i)))) meets ( L~ f) and

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

       A4: [k, i] in ( Indices G) and

       A5: j <= k;

      

       A6: 1 <= j by A3, MATRIX_0: 32;

      ex x be object st x in ( LSeg ((G * (j,i)),(G * (k,i)))) & x in ( L~ f) by A2, XBOOLE_0: 3;

      then

      reconsider X1 = X as non empty compact Subset of ( TOP-REAL 2) by XBOOLE_0:def 4;

      consider p be object such that

       A7: p in ( E-most X1) by XBOOLE_0:def 1;

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

      

       A8: p in X by A7, XBOOLE_0:def 4;

      then

       A9: p in ( LSeg ((G * (j,i)),(G * (k,i)))) by XBOOLE_0:def 4;

      ( proj1 .: X) = (( proj1 | X) .: X) by RELAT_1: 129;

      

      then

       A10: ( upper_bound ( proj1 .: X)) = ( upper_bound (( proj1 | X) .: ( [#] (( TOP-REAL 2) | X)))) by PRE_TOPC:def 5

      .= ( E-bound X);

      

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

      

       A12: (p `1 ) = (( E-min X) `1 ) by A7, PSCOMP_1: 47

      .= ( upper_bound ( proj1 .: X)) by A10, EUCLID: 52;

      

       A13: 1 <= k by A4, MATRIX_0: 32;

      

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

      

       A15: k <= ( len G) by A4, MATRIX_0: 32;

      then

       A16: ((G * (j,i)) `1 ) <= ((G * (k,i)) `1 ) by A5, A6, A14, SPRECT_3: 13;

      then

       A17: ((G * (j,i)) `1 ) <= (p `1 ) by A9, TOPREAL1: 3;

      

       A18: (p `1 ) <= ((G * (k,i)) `1 ) by A9, A16, TOPREAL1: 3;

      

       A19: j <= ( len G) by A3, MATRIX_0: 32;

      

      then

       A20: ((G * (j,i)) `2 ) = ((G * (1,i)) `2 ) by A6, A14, GOBOARD5: 1

      .= ((G * (k,i)) `2 ) by A13, A15, A11, GOBOARD5: 1;

      p in ( L~ f) by A8, XBOOLE_0:def 4;

      then p in ( union { ( LSeg (f,k1)) where k1 be Nat : 1 <= k1 & (k1 + 1) <= ( len f) }) by TOPREAL1:def 4;

      then

      consider Y be set such that

       A21: p in Y and

       A22: Y in { ( LSeg (f,k1)) where k1 be Nat : 1 <= k1 & (k1 + 1) <= ( len f) } by TARSKI:def 4;

      consider i1 be Nat such that

       A23: Y = ( LSeg (f,i1)) and

       A24: 1 <= i1 and

       A25: (i1 + 1) <= ( len f) by A22;

      

       A26: p in ( LSeg ((f /. i1),(f /. (i1 + 1)))) by A21, A23, A24, A25, TOPREAL1:def 3;

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

      then (i1 + 1) in ( Seg ( len f)) by A25, FINSEQ_1: 1;

      then

       A27: (i1 + 1) in ( dom f) by FINSEQ_1:def 3;

      then

      consider jo,io be Nat such that

       A28: [jo, io] in ( Indices G) and

       A29: (f /. (i1 + 1)) = (G * (jo,io)) by A1, GOBOARD1:def 9;

      

       A30: 1 <= jo by A28, MATRIX_0: 32;

      i1 <= ( len f) by A25, NAT_1: 13;

      then i1 in ( Seg ( len f)) by A24, FINSEQ_1: 1;

      then

       A31: i1 in ( dom f) by FINSEQ_1:def 3;

      then

      consider j0,i0 be Nat such that

       A32: [j0, i0] in ( Indices G) and

       A33: (f /. i1) = (G * (j0,i0)) by A1, GOBOARD1:def 9;

      

       A34: 1 <= j0 by A32, MATRIX_0: 32;

      

       A35: 1 <= i0 & i0 <= ( width G) by A32, MATRIX_0: 32;

      

       A36: j0 <= ( len G) by A32, MATRIX_0: 32;

      

       A37: 1 <= io & io <= ( width G) by A28, MATRIX_0: 32;

      

       A38: jo <= ( len G) by A28, MATRIX_0: 32;

      

       A39: f is special by A1, A31, JORDAN8: 4, RELAT_1: 38;

      ex n st j <= n & n <= k & (G * (n,i)) = p

      proof

        per cases by A24, A25, A39, TOPREAL1:def 5;

          suppose

           A40: ((f /. i1) `2 ) = ((f /. (i1 + 1)) `2 );

          ((G * (j,io)) `2 ) = ((G * (1,io)) `2 ) by A6, A19, A37, GOBOARD5: 1

          .= ((G * (jo,io)) `2 ) by A30, A38, A37, GOBOARD5: 1

          .= (p `2 ) by A26, A29, A40, GOBOARD7: 6

          .= ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6;

          then io <= i & io >= i by A6, A19, A14, A37, GOBOARD5: 4;

          then

           A41: i = io by XXREAL_0: 1;

          ((G * (j,i0)) `2 ) = ((G * (1,i0)) `2 ) by A6, A19, A35, GOBOARD5: 1

          .= ((G * (j0,i0)) `2 ) by A34, A36, A35, GOBOARD5: 1

          .= (p `2 ) by A26, A33, A40, GOBOARD7: 6

          .= ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6;

          then i0 <= i & i0 >= i by A6, A19, A14, A35, GOBOARD5: 4;

          then

           A42: i = i0 by XXREAL_0: 1;

          thus thesis

          proof

            per cases ;

              suppose

               A43: ((f /. i1) `1 ) <= ((f /. (i1 + 1)) `1 );

              thus thesis

              proof

                per cases ;

                  suppose

                   A44: (f /. (i1 + 1)) in ( LSeg ((G * (j,i)),(G * (k,i))));

                  (1 + 1) <= (i1 + 1) by A24, XREAL_1: 6;

                  then (f /. (i1 + 1)) in ( L~ f) by A25, A27, GOBOARD1: 1, XXREAL_0: 2;

                  then (f /. (i1 + 1)) in X1 by A44, XBOOLE_0:def 4;

                  then

                   A45: (p `1 ) >= ((f /. (i1 + 1)) `1 ) by A10, A12, PSCOMP_1: 24;

                  take n = jo;

                  

                   A46: p in ( LSeg ((G * (j,i)),(G * (k,i)))) by A8, XBOOLE_0:def 4;

                  (p `1 ) <= ((f /. (i1 + 1)) `1 ) by A26, A43, TOPREAL1: 3;

                  then (p `1 ) = ((f /. (i1 + 1)) `1 ) by A45, XXREAL_0: 1;

                  

                  then

                   A47: (p `1 ) = ((G * (jo,1)) `1 ) by A29, A30, A38, A37, GOBOARD5: 2

                  .= ((G * (n,i)) `1 ) by A14, A30, A38, GOBOARD5: 2;

                  

                   A48: ((G * (j,i)) `1 ) <= ((G * (k,i)) `1 ) by A5, A6, A14, A15, SPRECT_3: 13;

                  then ((G * (j,i)) `1 ) <= ((G * (n,i)) `1 ) by A46, A47, TOPREAL1: 3;

                  hence j <= n by A19, A14, A30, GOBOARD5: 3;

                  ((G * (n,i)) `1 ) <= ((G * (k,i)) `1 ) by A46, A47, A48, TOPREAL1: 3;

                  hence n <= k by A13, A11, A38, GOBOARD5: 3;

                  (p `2 ) = ((G * (j,i)) `2 ) by A20, A46, GOBOARD7: 6

                  .= ((G * (1,i)) `2 ) by A6, A19, A14, GOBOARD5: 1

                  .= ((G * (n,i)) `2 ) by A14, A30, A38, GOBOARD5: 1;

                  hence thesis by A47, TOPREAL3: 6;

                end;

                  suppose

                   A49: not (f /. (i1 + 1)) in ( LSeg ((G * (j,i)),(G * (k,i))));

                  

                   A50: ((f /. (i1 + 1)) `2 ) = (p `2 ) by A26, A40, GOBOARD7: 6

                  .= ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6;

                  thus thesis

                  proof

                    per cases by A20, A49, A50, GOBOARD7: 8;

                      suppose

                       A51: ((f /. (i1 + 1)) `1 ) > ((G * (k,i)) `1 );

                      (p `1 ) >= ((G * (j0,i0)) `1 ) by A26, A33, A43, TOPREAL1: 3;

                      then (p `1 ) >= ((G * (j0,1)) `1 ) by A34, A36, A35, GOBOARD5: 2;

                      then (p `1 ) >= ((G * (j0,i)) `1 ) by A14, A34, A36, GOBOARD5: 2;

                      then ((G * (k,i)) `1 ) >= ((G * (j0,i)) `1 ) by A18, XXREAL_0: 2;

                      then

                       A52: k >= j0 by A13, A11, A36, GOBOARD5: 3;

                      ( |.(i0 - io).| + |.(j0 - jo).|) = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def 9;

                      then ( 0 + |.(j0 - jo).|) = 1 by A42, A41, ABSVALUE: 2;

                      then

                       A53: |.( - (j0 - jo)).| = 1 by COMPLEX1: 52;

                      j0 <= (jo + 0 ) by A33, A29, A36, A35, A30, A42, A41, A43, GOBOARD5: 3;

                      then (j0 - jo) <= 0 by XREAL_1: 20;

                      then (jo - j0) = 1 by A53, ABSVALUE:def 1;

                      then

                       A54: (j0 + 1) = (jo + 0 );

                      ((G * (jo,i)) `1 ) > ((G * (k,i)) `1 ) & jo >= k by A29, A15, A11, A30, A41, A51, GOBOARD5: 3;

                      then jo > k by XXREAL_0: 1;

                      then j0 >= k by A54, NAT_1: 13;

                      then

                       A55: k = j0 by A52, XXREAL_0: 1;

                      take n = j0;

                      

                       A56: (p `2 ) = ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6

                      .= ((G * (1,i)) `2 ) by A6, A19, A14, GOBOARD5: 1

                      .= ((G * (n,i)) `2 ) by A14, A34, A36, GOBOARD5: 1;

                      (p `1 ) >= ((G * (j0,i0)) `1 ) by A26, A33, A43, TOPREAL1: 3;

                      then (p `1 ) >= ((G * (j0,1)) `1 ) by A34, A36, A35, GOBOARD5: 2;

                      then (p `1 ) >= ((G * (j0,i)) `1 ) by A14, A34, A36, GOBOARD5: 2;

                      then (p `1 ) = ((G * (k,i)) `1 ) by A18, A55, XXREAL_0: 1;

                      hence thesis by A5, A55, A56, TOPREAL3: 6;

                    end;

                      suppose

                       A57: ((f /. (i1 + 1)) `1 ) < ((G * (j,i)) `1 );

                      (p `1 ) <= ((f /. (i1 + 1)) `1 ) by A26, A43, TOPREAL1: 3;

                      hence thesis by A17, A57, XXREAL_0: 2;

                    end;

                  end;

                end;

              end;

            end;

              suppose

               A58: ((f /. i1) `1 ) > ((f /. (i1 + 1)) `1 );

              thus thesis

              proof

                per cases ;

                  suppose

                   A59: (f /. i1) in ( LSeg ((G * (j,i)),(G * (k,i))));

                  (1 + 1) <= (i1 + 1) by A24, XREAL_1: 6;

                  then (f /. i1) in ( L~ f) by A25, A31, GOBOARD1: 1, XXREAL_0: 2;

                  then (f /. i1) in X1 by A59, XBOOLE_0:def 4;

                  then

                   A60: (p `1 ) >= ((f /. i1) `1 ) by A10, A12, PSCOMP_1: 24;

                  take n = j0;

                  

                   A61: p in ( LSeg ((G * (j,i)),(G * (k,i)))) by A8, XBOOLE_0:def 4;

                  (p `1 ) <= ((f /. i1) `1 ) by A26, A58, TOPREAL1: 3;

                  then (p `1 ) = ((f /. i1) `1 ) by A60, XXREAL_0: 1;

                  

                  then

                   A62: (p `1 ) = ((G * (j0,1)) `1 ) by A33, A34, A36, A35, GOBOARD5: 2

                  .= ((G * (n,i)) `1 ) by A14, A34, A36, GOBOARD5: 2;

                  

                   A63: ((G * (j,i)) `1 ) <= ((G * (k,i)) `1 ) by A5, A6, A14, A15, SPRECT_3: 13;

                  then ((G * (j,i)) `1 ) <= ((G * (n,i)) `1 ) by A61, A62, TOPREAL1: 3;

                  hence j <= n by A19, A14, A34, GOBOARD5: 3;

                  ((G * (n,i)) `1 ) <= ((G * (k,i)) `1 ) by A61, A62, A63, TOPREAL1: 3;

                  hence n <= k by A13, A11, A36, GOBOARD5: 3;

                  (p `2 ) = ((G * (j,i)) `2 ) by A20, A61, GOBOARD7: 6

                  .= ((G * (1,i)) `2 ) by A6, A19, A14, GOBOARD5: 1

                  .= ((G * (n,i)) `2 ) by A14, A34, A36, GOBOARD5: 1;

                  hence thesis by A62, TOPREAL3: 6;

                end;

                  suppose

                   A64: not (f /. i1) in ( LSeg ((G * (j,i)),(G * (k,i))));

                  

                   A65: ((f /. i1) `2 ) = (p `2 ) by A26, A40, GOBOARD7: 6

                  .= ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6;

                  thus thesis

                  proof

                    per cases by A20, A64, A65, GOBOARD7: 8;

                      suppose

                       A66: ((f /. i1) `1 ) > ((G * (k,i)) `1 );

                      (p `1 ) >= ((G * (jo,io)) `1 ) by A26, A29, A58, TOPREAL1: 3;

                      then (p `1 ) >= ((G * (jo,1)) `1 ) by A30, A38, A37, GOBOARD5: 2;

                      then (p `1 ) >= ((G * (jo,i)) `1 ) by A14, A30, A38, GOBOARD5: 2;

                      then ((G * (k,i)) `1 ) >= ((G * (jo,i)) `1 ) by A18, XXREAL_0: 2;

                      then

                       A67: k >= jo by A13, A11, A38, GOBOARD5: 3;

                      jo <= (j0 + 0 ) by A33, A29, A34, A35, A38, A42, A41, A58, GOBOARD5: 3;

                      then (jo - j0) <= 0 by XREAL_1: 20;

                      then

                       A68: ( - (jo - j0)) >= ( - 0 );

                      ( |.(i0 - io).| + |.(j0 - jo).|) = 1 by A1, A31, A27, A32, A33, A28, A29, GOBOARD1:def 9;

                      then ( 0 + |.(j0 - jo).|) = 1 by A42, A41, ABSVALUE: 2;

                      then (j0 - jo) = 1 by A68, ABSVALUE:def 1;

                      then

                       A69: (jo + 1) = (j0 - 0 );

                      ((G * (j0,i)) `1 ) > ((G * (k,i)) `1 ) & j0 >= k by A33, A15, A11, A34, A42, A66, GOBOARD5: 3;

                      then j0 > k by XXREAL_0: 1;

                      then jo >= k by A69, NAT_1: 13;

                      then

                       A70: k = jo by A67, XXREAL_0: 1;

                      take n = jo;

                      

                       A71: (p `2 ) = ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6

                      .= ((G * (1,i)) `2 ) by A6, A19, A14, GOBOARD5: 1

                      .= ((G * (n,i)) `2 ) by A14, A30, A38, GOBOARD5: 1;

                      (p `1 ) >= ((G * (jo,io)) `1 ) by A26, A29, A58, TOPREAL1: 3;

                      then (p `1 ) >= ((G * (jo,1)) `1 ) by A30, A38, A37, GOBOARD5: 2;

                      then (p `1 ) >= ((G * (jo,i)) `1 ) by A14, A30, A38, GOBOARD5: 2;

                      then (p `1 ) = ((G * (k,i)) `1 ) by A18, A70, XXREAL_0: 1;

                      hence thesis by A5, A70, A71, TOPREAL3: 6;

                    end;

                      suppose

                       A72: ((f /. i1) `1 ) < ((G * (j,i)) `1 );

                      (p `1 ) <= ((f /. i1) `1 ) by A26, A58, TOPREAL1: 3;

                      hence thesis by A17, A72, XXREAL_0: 2;

                    end;

                  end;

                end;

              end;

            end;

          end;

        end;

          suppose

           A73: ((f /. i1) `1 ) = ((f /. (i1 + 1)) `1 );

          take n = j0;

          (p `1 ) = ((f /. i1) `1 ) by A26, A73, GOBOARD7: 5;

          

          then

           A74: (p `1 ) = ((G * (j0,1)) `1 ) by A33, A34, A36, A35, GOBOARD5: 2

          .= ((G * (n,i)) `1 ) by A14, A34, A36, GOBOARD5: 2;

          

           A75: ((G * (j,i)) `1 ) <= ((G * (k,i)) `1 ) by A5, A6, A14, A15, SPRECT_3: 13;

          then ((G * (j,i)) `1 ) <= ((G * (n,i)) `1 ) by A9, A74, TOPREAL1: 3;

          hence j <= n by A19, A14, A34, GOBOARD5: 3;

          ((G * (n,i)) `1 ) <= ((G * (k,i)) `1 ) by A9, A74, A75, TOPREAL1: 3;

          hence n <= k by A13, A11, A36, GOBOARD5: 3;

          (p `2 ) = ((G * (j,i)) `2 ) by A20, A9, GOBOARD7: 6

          .= ((G * (1,i)) `2 ) by A6, A19, A14, GOBOARD5: 1

          .= ((G * (n,i)) `2 ) by A14, A34, A36, GOBOARD5: 1;

          hence thesis by A74, TOPREAL3: 6;

        end;

      end;

      hence thesis by A12;

    end;

    theorem :: JORDAN1F:5

    

     Th5: for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds (( Upper_Seq (C,n)) /. 1) = ( W-min ( L~ ( Cage (C,n))))

    proof

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

      let n be Nat;

      ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 46;

      then ( Upper_Seq (C,n)) = (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) -: ( E-max ( L~ ( Cage (C,n))))) & ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by FINSEQ_6: 90, JORDAN1E:def 1, SPRECT_2: 43;

      then ( W-min ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) & (( Upper_Seq (C,n)) /. 1) = (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. 1) by FINSEQ_5: 44, SPRECT_2: 43;

      hence thesis by FINSEQ_6: 92;

    end;

    theorem :: JORDAN1F:6

    

     Th6: for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds (( Lower_Seq (C,n)) /. 1) = ( E-max ( L~ ( Cage (C,n))))

    proof

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

      let n be Nat;

      ( Lower_Seq (C,n)) = (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) :- ( E-max ( L~ ( Cage (C,n))))) by JORDAN1E:def 2;

      hence thesis by FINSEQ_5: 53;

    end;

    theorem :: JORDAN1F:7

    

     Th7: for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds (( Upper_Seq (C,n)) /. ( len ( Upper_Seq (C,n)))) = ( E-max ( L~ ( Cage (C,n))))

    proof

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

      let n be Nat;

      

       A1: ( Upper_Seq (C,n)) = (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) -: ( E-max ( L~ ( Cage (C,n))))) & ( rng ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) = ( rng ( Cage (C,n))) by FINSEQ_6: 90, JORDAN1E:def 1, SPRECT_2: 43;

      then ( len ( Upper_Seq (C,n))) = (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by FINSEQ_5: 42, SPRECT_2: 46;

      hence thesis by A1, FINSEQ_5: 45, SPRECT_2: 46;

    end;

    theorem :: JORDAN1F:8

    

     Th8: for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds (( Lower_Seq (C,n)) /. ( len ( Lower_Seq (C,n)))) = ( W-min ( L~ ( Cage (C,n))))

    proof

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

      let n be Nat;

      

       A1: ( W-min ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 43;

      ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 46;

      then ( Lower_Seq (C,n)) = (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) :- ( E-max ( L~ ( Cage (C,n))))) & ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by FINSEQ_6: 90, JORDAN1E:def 2, SPRECT_2: 43;

      

      hence (( Lower_Seq (C,n)) /. ( len ( Lower_Seq (C,n)))) = (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. ( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) by FINSEQ_5: 54

      .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. 1) by FINSEQ_6:def 1

      .= ( W-min ( L~ ( Cage (C,n)))) by A1, FINSEQ_6: 92;

    end;

    theorem :: JORDAN1F:9

    

     Th9: for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds ( L~ ( Upper_Seq (C,n))) = ( Upper_Arc ( L~ ( Cage (C,n)))) & ( L~ ( Lower_Seq (C,n))) = ( Lower_Arc ( L~ ( Cage (C,n)))) or ( L~ ( Upper_Seq (C,n))) = ( Lower_Arc ( L~ ( Cage (C,n)))) & ( L~ ( Lower_Seq (C,n))) = ( Upper_Arc ( L~ ( Cage (C,n))))

    proof

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

      let n be Nat;

      set WC = ( W-min ( L~ ( Cage (C,n))));

      set EC = ( E-max ( L~ ( Cage (C,n))));

      

       A1: ( Lower_Arc ( L~ ( Cage (C,n)))) is_an_arc_of (WC,EC) & (( Upper_Arc ( L~ ( Cage (C,n)))) \/ ( Lower_Arc ( L~ ( Cage (C,n))))) = ( L~ ( Cage (C,n))) by JORDAN6: 50;

      (( Upper_Seq (C,n)) /. 1) = WC & (( Upper_Seq (C,n)) /. ( len ( Upper_Seq (C,n)))) = EC by Th5, Th7;

      then

       A2: ( L~ ( Upper_Seq (C,n))) is_an_arc_of (WC,EC) by TOPREAL1: 25;

      (( Lower_Seq (C,n)) /. 1) = EC & (( Lower_Seq (C,n)) /. ( len ( Lower_Seq (C,n)))) = WC by Th6, Th8;

      then

       A3: ( L~ ( Lower_Seq (C,n))) is_an_arc_of (WC,EC) by JORDAN5B: 14, TOPREAL1: 25;

      (( L~ ( Upper_Seq (C,n))) \/ ( L~ ( Lower_Seq (C,n)))) = ( L~ ( Cage (C,n))) & ( Upper_Arc ( L~ ( Cage (C,n)))) is_an_arc_of (WC,EC) by JORDAN1E: 13, JORDAN6: 50;

      hence thesis by A2, A3, A1, JORDAN6: 48;

    end;

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

p for Point of ( TOP-REAL 2),

i1,j1,i2,j2 for Nat;

    theorem :: JORDAN1F:10

    

     Th10: for C be connected compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds ( Upper_Seq (C,n)) is_sequence_on ( Gauge (C,n))

    proof

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

      let n be Nat;

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

      then

       A1: ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) is_sequence_on ( Gauge (C,n)) by REVROT_1: 34;

      ( Upper_Seq (C,n)) = (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) -: ( E-max ( L~ ( Cage (C,n))))) by JORDAN1E:def 1

      .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) | (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) by FINSEQ_5:def 1;

      hence thesis by A1, GOBOARD1: 22;

    end;

    theorem :: JORDAN1F:11

    

     Th11: for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on G & (ex i, j st [i, j] in ( Indices G) & p = (G * (i,j))) & (for i1, j1, i2, j2 st [i1, j1] in ( Indices G) & [i2, j2] in ( Indices G) & p = (G * (i1,j1)) & (f /. 1) = (G * (i2,j2)) holds ( |.(i2 - i1).| + |.(j2 - j1).|) = 1) holds ( <*p*> ^ f) is_sequence_on G

    proof

      let f be FinSequence of ( TOP-REAL 2) such that

       A1: f is_sequence_on G and

       A2: ex i, j st [i, j] in ( Indices G) & p = (G * (i,j)) and

       A3: for i1, j1, i2, j2 st [i1, j1] in ( Indices G) & [i2, j2] in ( Indices G) & p = (G * (i1,j1)) & (f /. 1) = (G * (i2,j2)) holds ( |.(i2 - i1).| + |.(j2 - j1).|) = 1;

       A4:

      now

        let m, k, i, j such that

         A5: [m, k] in ( Indices G) & [i, j] in ( Indices G) & ( <*p*> /. ( len <*p*>)) = (G * (m,k)) & (f /. 1) = (G * (i,j)) and

         A6: ( len <*p*>) in ( dom <*p*>) and 1 in ( dom f);

        ( len <*p*>) = 1 by FINSEQ_1: 40;

        then ( <*p*> . ( len <*p*>)) = p by FINSEQ_1: 40;

        then ( <*p*> /. ( len <*p*>)) = p by A6, PARTFUN1:def 6;

        then ( |.(i - m).| + |.(j - k).|) = 1 by A3, A5;

        

        hence 1 = ( |.(m - i).| + |.(j - k).|) by UNIFORM1: 11

        .= ( |.(m - i).| + |.(k - j).|) by UNIFORM1: 11;

      end;

       A7:

      now

        let n such that

         A8: n in ( dom ( <*p*> ^ f));

        per cases by A8, FINSEQ_1: 25;

          suppose

           A9: n in ( dom <*p*>);

          consider i, j such that

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

           A11: p = (G * (i,j)) by A2;

          take i, j;

          thus [i, j] in ( Indices G) by A10;

          n in ( Seg 1) by A9, FINSEQ_1: 38;

          then 1 <= n & n <= 1 by FINSEQ_1: 1;

          then n = 1 by XXREAL_0: 1;

          then ( <*p*> . n) = p by FINSEQ_1: 40;

          then ( <*p*> /. n) = p by A9, PARTFUN1:def 6;

          hence (( <*p*> ^ f) /. n) = (G * (i,j)) by A9, A11, FINSEQ_4: 68;

        end;

          suppose ex l be Nat st l in ( dom f) & n = (( len <*p*>) + l);

          then

          consider l be Nat such that

           A12: l in ( dom f) and

           A13: n = (( len <*p*>) + l);

          consider i, j such that

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

           A15: (f /. l) = (G * (i,j)) by A1, A12, GOBOARD1:def 9;

          take i, j;

          thus [i, j] in ( Indices G) by A14;

          thus (( <*p*> ^ f) /. n) = (G * (i,j)) by A12, A13, A15, FINSEQ_4: 69;

        end;

      end;

       A16:

      now

        let n;

        assume that

         A17: n in ( dom <*p*>) and

         A18: (n + 1) in ( dom <*p*>);

        (n + 1) <= ( len <*p*>) by A18, FINSEQ_3: 25;

        then

         A19: (n + 1) <= 1 by FINSEQ_1: 39;

        1 <= n by A17, FINSEQ_3: 25;

        then (1 + 1) <= (n + 1) by XREAL_1: 6;

        hence for m, k, i, j st [m, k] in ( Indices G) & [i, j] in ( Indices G) & ( <*p*> /. n) = (G * (m,k)) & ( <*p*> /. (n + 1)) = (G * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 by A19, XXREAL_0: 2;

      end;

      for n st n in ( dom f) & (n + 1) in ( dom f) holds for m, k, i, j st [m, k] in ( Indices G) & [i, j] in ( Indices G) & (f /. n) = (G * (m,k)) & (f /. (n + 1)) = (G * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 by A1, GOBOARD1:def 9;

      then for n st n in ( dom ( <*p*> ^ f)) & (n + 1) in ( dom ( <*p*> ^ f)) holds for m, k, i, j st [m, k] in ( Indices G) & [i, j] in ( Indices G) & (( <*p*> ^ f) /. n) = (G * (m,k)) & (( <*p*> ^ f) /. (n + 1)) = (G * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 by A16, A4, GOBOARD1: 24;

      hence thesis by A7, GOBOARD1:def 9;

    end;

    theorem :: JORDAN1F:12

    

     Th12: for C be connected compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds ( Lower_Seq (C,n)) is_sequence_on ( Gauge (C,n))

    proof

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

      let n be Nat;

      consider j such that

       A1: 1 <= j & j <= ( width ( Gauge (C,n))) and

       A2: ( E-max ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (( len ( Gauge (C,n))),j)) by JORDAN1D: 25;

      set E1 = ((( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /^ (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) /. 1);

      set i = ( len ( Gauge (C,n)));

      

       A3: ( Lower_Seq (C,n)) = (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) :- ( E-max ( L~ ( Cage (C,n))))) by JORDAN1E:def 2

      .= ( <*( E-max ( L~ ( Cage (C,n))))*> ^ (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /^ (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))))) by FINSEQ_5:def 2;

      

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

      then ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) is_sequence_on ( Gauge (C,n)) by REVROT_1: 34;

      then

       A5: (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /^ (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) is_sequence_on ( Gauge (C,n)) by JORDAN8: 2;

      

       A6: for i1, j1, i2, j2 st [i1, j1] in ( Indices ( Gauge (C,n))) & [i2, j2] in ( Indices ( Gauge (C,n))) & ( E-max ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (i1,j1)) & E1 = (( Gauge (C,n)) * (i2,j2)) holds ( |.(i2 - i1).| + |.(j2 - j1).|) = 1

      proof

        set en = (( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n)));

        let i1, j1, i2, j2;

        assume

         A7: [i1, j1] in ( Indices ( Gauge (C,n))) & [i2, j2] in ( Indices ( Gauge (C,n))) & ( E-max ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (i1,j1)) & E1 = (( Gauge (C,n)) * (i2,j2));

        en < ( len ( Cage (C,n))) by SPRECT_5: 16;

        then 1 <= (en + 1) & (en + 1) <= ( len ( Cage (C,n))) by NAT_1: 11, NAT_1: 13;

        then

         A8: (en + 1) in ( dom ( Cage (C,n))) by FINSEQ_3: 25;

        

         A9: ( W-min ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 43;

        

         A10: (( Cage (C,n)) /. 1) = ( N-min ( L~ ( Cage (C,n)))) by JORDAN9: 32;

        then (( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) < (( E-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by SPRECT_2: 71;

        then (( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) < (( S-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by A10, SPRECT_2: 72, XXREAL_0: 2;

        then (( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) < (( S-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by A10, SPRECT_2: 73, XXREAL_0: 2;

        then

         A11: (( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) < (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by A10, SPRECT_2: 74, XXREAL_0: 2;

        then

         A12: ((( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) + 1) <= (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by NAT_1: 13;

        

         A13: (( len ( Cage (C,n))) - (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n)))) > 0 by SPRECT_5: 20, XREAL_1: 50;

        then

         A14: (((( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) + 1) + (( len ( Cage (C,n))) - (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))))) >= ( 0 + 0 );

        

         A15: ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 46;

        then 1 <= (( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by FINSEQ_4: 21;

        then

         A16: 1 < ((( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) + 1) by NAT_1: 13;

        ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by A15, FINSEQ_6: 90, SPRECT_2: 43;

        then

         A17: (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) <= ( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by FINSEQ_4: 21;

        now

          assume (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) = ( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))));

          then (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) = ( len ( Cage (C,n))) by FINSEQ_6: 179;

          then ( len ( Upper_Seq (C,n))) = ( len ( Cage (C,n))) by JORDAN1E: 8;

          then (( len ( Cage (C,n))) + ( len ( Lower_Seq (C,n)))) = (( len ( Cage (C,n))) + 1) by JORDAN1E: 10;

          hence contradiction by JORDAN1E: 15;

        end;

        then (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) < ( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by A17, XXREAL_0: 1;

        then ((( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) + 1) <= ( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by NAT_1: 13;

        then ((1 + (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) - (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) <= (( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) - (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) by XREAL_1: 9;

        then 1 <= ( len (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /^ (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))))) by A17, RFINSEQ:def 1;

        then 1 in ( dom (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /^ (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))))) by FINSEQ_3: 25;

        

        then E1 = (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. ((( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) + 1)) by FINSEQ_5: 27

        .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. (((( len ( Cage (C,n))) + (( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n)))) - (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n)))) + 1)) by A15, A9, A11, SPRECT_5: 9

        .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. (((( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) + (( len ( Cage (C,n))) - (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))))) + 1))

        .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. (((( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) + (( len ( Cage (C,n))) -' (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))))) + 1)) by A13, XREAL_0:def 2

        .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. (((( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) + 1) + (( len ( Cage (C,n))) -' (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))))))

        .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. (((( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) + 1) + (( len ( Cage (C,n))) - (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n)))))) by A13, XREAL_0:def 2

        .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. ((((( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) + 1) + ( len ( Cage (C,n)))) - (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n)))))

        .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. ((((( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) + 1) + ( len ( Cage (C,n)))) -' (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))))) by A14, XREAL_0:def 2;

        then

         A18: E1 = (( Cage (C,n)) /. (en + 1)) by A9, A16, A12, FINSEQ_6: 178;

        ( E-max ( L~ ( Cage (C,n)))) = (( Cage (C,n)) /. en) & en in ( dom ( Cage (C,n))) by A15, FINSEQ_4: 20, FINSEQ_5: 38;

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

        then ( |.(i1 - i2).| + |.(j2 - j1).|) = 1 by UNIFORM1: 11;

        hence thesis by UNIFORM1: 11;

      end;

      i >= 4 by JORDAN8: 10;

      then 1 <= i by XXREAL_0: 2;

      then [i, j] in ( Indices ( Gauge (C,n))) by A1, MATRIX_0: 30;

      hence thesis by A5, A2, A6, A3, Th11;

    end;

    theorem :: JORDAN1F:13

    (p `1 ) = ((( W-bound C) + ( E-bound C)) / 2) & (p `2 ) = ( lower_bound ( proj2 .: (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))))) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1)))))))) implies ex j st 1 <= j & j <= ( width ( Gauge (C,(i + 1)))) & p = (( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),j))

    proof

      assume that

       A1: (p `1 ) = ((( W-bound C) + ( E-bound C)) / 2) and

       A2: (p `2 ) = ( lower_bound ( proj2 .: (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))))) /\ ( Upper_Arc ( L~ ( Cage (C,(i + 1))))))));

      per cases by Th9;

        suppose

         A3: ( L~ ( Upper_Seq (C,(i + 1)))) = ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) & ( L~ ( Lower_Seq (C,(i + 1)))) = ( Lower_Arc ( L~ ( Cage (C,(i + 1)))));

        

         A4: 1 <= ( Center ( Gauge (C,1))) by JORDAN1B: 11;

        set k = ( width ( Gauge (C,(i + 1))));

        set l = ( Center ( Gauge (C,(i + 1))));

        set G = ( Gauge (C,(i + 1)));

        set f = ( Upper_Seq (C,(i + 1)));

        

         A5: 1 <= l by JORDAN1B: 11;

        

         A6: ( width ( Gauge (C,(i + 1)))) = ( len ( Gauge (C,(i + 1)))) by JORDAN8:def 1;

        then k >= 4 by JORDAN8: 10;

        then

         A7: 1 <= k by XXREAL_0: 2;

        then

         A8: l <= ( len G) by A6, JORDAN1B: 12;

        then

         A9: [l, 1] in ( Indices G) & [l, k] in ( Indices G) by A7, A5, MATRIX_0: 30;

        

         A10: ( width ( Gauge (C,1))) = ( len ( Gauge (C,1))) by JORDAN8:def 1;

        then ( width ( Gauge (C,1))) >= 4 by JORDAN8: 10;

        then

         A11: 1 <= ( width ( Gauge (C,1))) by XXREAL_0: 2;

        then

         A12: ( Center ( Gauge (C,1))) <= ( len ( Gauge (C,1))) by A10, JORDAN1B: 12;

        

         A13: (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))))) /\ ( L~ f)) c= (( LSeg ((G * (l,1)),(G * (l,k)))) /\ ( L~ f))

        proof

          let a be object;

          

           A14: ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) c= ( L~ ( Cage (C,(i + 1)))) by JORDAN6: 61;

          assume

           A15: a in (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))))) /\ ( L~ f));

          then

          reconsider a1 = a as Point of ( TOP-REAL 2);

          

           A16: a1 in ( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))))) by A15, XBOOLE_0:def 4;

          a1 in ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) by A3, A15, XBOOLE_0:def 4;

          then

           A17: (a1 `2 ) <= ( N-bound ( L~ ( Cage (C,(i + 1))))) by A14, PSCOMP_1: 24;

          ( Cage (C,(i + 1))) is_sequence_on G by JORDAN9:def 1;

          then ((G * (l,k)) `2 ) >= ( N-bound ( L~ ( Cage (C,(i + 1))))) by A6, A7, A5, JORDAN1A: 20, JORDAN1B: 12;

          then

           A18: (a1 `2 ) <= ((G * (l,k)) `2 ) by A17, XXREAL_0: 2;

          a1 in ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) by A3, A15, XBOOLE_0:def 4;

          then

           A19: (a1 `2 ) >= ( S-bound ( L~ ( Cage (C,(i + 1))))) by A14, PSCOMP_1: 24;

          ( Cage (C,(i + 1))) is_sequence_on G by JORDAN9:def 1;

          then ((G * (l,1)) `2 ) <= ( S-bound ( L~ ( Cage (C,(i + 1))))) by A6, A7, A5, JORDAN1A: 22, JORDAN1B: 12;

          then

           A20: (a1 `2 ) >= ((G * (l,1)) `2 ) by A19, XXREAL_0: 2;

          

           A21: a1 in ( L~ f) by A15, XBOOLE_0:def 4;

          ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)) `1 ) = ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))) `1 ) by A11, A12, A4, GOBOARD5: 2;

          

          then

           A22: (a1 `1 ) = ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)) `1 ) by A16, GOBOARD7: 5

          .= ((G * (l,1)) `1 ) by A6, A10, A7, A11, JORDAN1A: 36;

          then (a1 `1 ) = ((G * (l,k)) `1 ) by A7, A8, A5, GOBOARD5: 2;

          then a1 in ( LSeg ((G * (l,1)),(G * (l,k)))) by A22, A20, A18, GOBOARD7: 7;

          hence thesis by A21, XBOOLE_0:def 4;

        end;

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

        then (( LSeg ((G * (l,1)),(G * (l,k)))) /\ ( L~ f)) c= (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))))) /\ ( L~ f)) by A6, A10, JORDAN1A: 44, XBOOLE_1: 26;

        then

         A23: (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))))) /\ ( L~ f)) = (( LSeg ((G * (l,1)),(G * (l,k)))) /\ ( L~ f)) by A13, XBOOLE_0:def 10;

        ( LSeg ((G * (l,1)),(G * (l,k)))) meets ( L~ f) by A3, A6, A7, A5, JORDAN1B: 12, JORDAN1B: 29;

        then

        consider n such that

         A24: 1 <= n & n <= k and

         A25: ((G * (l,n)) `2 ) = ( lower_bound ( proj2 .: (( LSeg ((G * (l,1)),(G * (l,k)))) /\ ( L~ f)))) by A7, A9, Th1, Th10;

        take n;

        thus 1 <= n & n <= ( width ( Gauge (C,(i + 1)))) by A24;

        ( len ( Gauge (C,1))) >= 4 by JORDAN8: 10;

        then

         A26: 1 <= ( len ( Gauge (C,1))) by XXREAL_0: 2;

        

        then (p `1 ) = ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)) `1 ) by A1, JORDAN1A: 38

        .= ((( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),n)) `1 ) by A6, A24, A26, JORDAN1A: 36;

        hence thesis by A2, A3, A25, A23, TOPREAL3: 6;

      end;

        suppose

         A27: ( L~ ( Upper_Seq (C,(i + 1)))) = ( Lower_Arc ( L~ ( Cage (C,(i + 1))))) & ( L~ ( Lower_Seq (C,(i + 1)))) = ( Upper_Arc ( L~ ( Cage (C,(i + 1)))));

        

         A28: 1 <= ( Center ( Gauge (C,1))) by JORDAN1B: 11;

        set k = ( width ( Gauge (C,(i + 1))));

        set l = ( Center ( Gauge (C,(i + 1))));

        set G = ( Gauge (C,(i + 1)));

        set f = ( Lower_Seq (C,(i + 1)));

        

         A29: 1 <= l by JORDAN1B: 11;

        

         A30: ( width ( Gauge (C,(i + 1)))) = ( len ( Gauge (C,(i + 1)))) by JORDAN8:def 1;

        then k >= 4 by JORDAN8: 10;

        then

         A31: 1 <= k by XXREAL_0: 2;

        then

         A32: l <= ( len G) by A30, JORDAN1B: 12;

        then

         A33: [l, 1] in ( Indices G) & [l, k] in ( Indices G) by A31, A29, MATRIX_0: 30;

        

         A34: ( width ( Gauge (C,1))) = ( len ( Gauge (C,1))) by JORDAN8:def 1;

        then ( width ( Gauge (C,1))) >= 4 by JORDAN8: 10;

        then

         A35: 1 <= ( width ( Gauge (C,1))) by XXREAL_0: 2;

        then

         A36: ( Center ( Gauge (C,1))) <= ( len ( Gauge (C,1))) by A34, JORDAN1B: 12;

        

         A37: (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))))) /\ ( L~ f)) c= (( LSeg ((G * (l,1)),(G * (l,k)))) /\ ( L~ f))

        proof

          let a be object;

          

           A38: ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) c= ( L~ ( Cage (C,(i + 1)))) by JORDAN6: 61;

          assume

           A39: a in (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))))) /\ ( L~ f));

          then

          reconsider a1 = a as Point of ( TOP-REAL 2);

          

           A40: a1 in ( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))))) by A39, XBOOLE_0:def 4;

          a1 in ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) by A27, A39, XBOOLE_0:def 4;

          then

           A41: (a1 `2 ) <= ( N-bound ( L~ ( Cage (C,(i + 1))))) by A38, PSCOMP_1: 24;

          ( Cage (C,(i + 1))) is_sequence_on G by JORDAN9:def 1;

          then ((G * (l,k)) `2 ) >= ( N-bound ( L~ ( Cage (C,(i + 1))))) by A30, A31, A29, JORDAN1A: 20, JORDAN1B: 12;

          then

           A42: (a1 `2 ) <= ((G * (l,k)) `2 ) by A41, XXREAL_0: 2;

          a1 in ( Upper_Arc ( L~ ( Cage (C,(i + 1))))) by A27, A39, XBOOLE_0:def 4;

          then

           A43: (a1 `2 ) >= ( S-bound ( L~ ( Cage (C,(i + 1))))) by A38, PSCOMP_1: 24;

          ( Cage (C,(i + 1))) is_sequence_on G by JORDAN9:def 1;

          then ((G * (l,1)) `2 ) <= ( S-bound ( L~ ( Cage (C,(i + 1))))) by A30, A31, A29, JORDAN1A: 22, JORDAN1B: 12;

          then

           A44: (a1 `2 ) >= ((G * (l,1)) `2 ) by A43, XXREAL_0: 2;

          

           A45: a1 in ( L~ f) by A39, XBOOLE_0:def 4;

          ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)) `1 ) = ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))) `1 ) by A35, A36, A28, GOBOARD5: 2;

          

          then

           A46: (a1 `1 ) = ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)) `1 ) by A40, GOBOARD7: 5

          .= ((G * (l,1)) `1 ) by A30, A34, A31, A35, JORDAN1A: 36;

          then (a1 `1 ) = ((G * (l,k)) `1 ) by A31, A32, A29, GOBOARD5: 2;

          then a1 in ( LSeg ((G * (l,1)),(G * (l,k)))) by A46, A44, A42, GOBOARD7: 7;

          hence thesis by A45, XBOOLE_0:def 4;

        end;

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

        then (( LSeg ((G * (l,1)),(G * (l,k)))) /\ ( L~ f)) c= (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))))) /\ ( L~ f)) by A30, A34, JORDAN1A: 44, XBOOLE_1: 26;

        then

         A47: (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,1)) * (( Center ( Gauge (C,1))),( width ( Gauge (C,1))))))) /\ ( L~ f)) = (( LSeg ((G * (l,1)),(G * (l,k)))) /\ ( L~ f)) by A37, XBOOLE_0:def 10;

        ( LSeg ((G * (l,1)),(G * (l,k)))) meets ( L~ f) by A27, A30, A31, A29, JORDAN1B: 12, JORDAN1B: 29;

        then

        consider n such that

         A48: 1 <= n & n <= k and

         A49: ((G * (l,n)) `2 ) = ( lower_bound ( proj2 .: (( LSeg ((G * (l,1)),(G * (l,k)))) /\ ( L~ f)))) by A31, A33, Th1, Th12;

        take n;

        thus 1 <= n & n <= ( width ( Gauge (C,(i + 1)))) by A48;

        ( len ( Gauge (C,1))) >= 4 by JORDAN8: 10;

        then

         A50: 1 <= ( len ( Gauge (C,1))) by XXREAL_0: 2;

        

        then (p `1 ) = ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)) `1 ) by A1, JORDAN1A: 38

        .= ((( Gauge (C,(i + 1))) * (( Center ( Gauge (C,(i + 1)))),n)) `1 ) by A30, A48, A50, JORDAN1A: 36;

        hence thesis by A2, A27, A49, A47, TOPREAL3: 6;

      end;

    end;