jordan1d.miz



    begin

    reserve a,b,i,k,m,n for Nat,

r for Real,

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

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

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

    then

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

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

    then

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

    

     Lm3: for x,A,B,C,D be set holds x in (((A \/ B) \/ C) \/ D) iff x in A or x in B or x in C or x in D

    proof

      let x,A,B,C,D be set;

      hereby

        assume x in (((A \/ B) \/ C) \/ D);

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

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

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

      end;

      assume x in A or x in B or x in C or x in D;

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

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

      hence thesis by XBOOLE_0:def 3;

    end;

    

     Lm4: for A,B,C,D be set holds ( union {A, B, C, D}) = (((A \/ B) \/ C) \/ D)

    proof

      let A,B,C,D be set;

      

       A1: B in {A, B, C, D} by ENUMSET1:def 2;

      

       A2: D in {A, B, C, D} by ENUMSET1:def 2;

      hereby

        let x be object;

        assume x in ( union {A, B, C, D});

        then

        consider Z be set such that

         A3: x in Z and

         A4: Z in {A, B, C, D} by TARSKI:def 4;

        Z = A or Z = B or Z = C or Z = D by A4, ENUMSET1:def 2;

        hence x in (((A \/ B) \/ C) \/ D) by A3, Lm3;

      end;

      let x be object;

      

       A5: C in {A, B, C, D} by ENUMSET1:def 2;

      assume x in (((A \/ B) \/ C) \/ D);

      then

       A6: x in A or x in B or x in C or x in D by Lm3;

      A in {A, B, C, D} by ENUMSET1:def 2;

      hence thesis by A6, A1, A5, A2, TARSKI:def 4;

    end;

    theorem :: JORDAN1D:1

    

     Th1: for A,B be set st for x be set st x in A holds ex K be set st K c= B & x c= ( union K) holds ( union A) c= ( union B)

    proof

      let A,B be set such that

       A1: for x be set st x in A holds ex K be set st K c= B & x c= ( union K);

      let a be object;

      assume a in ( union A);

      then

      consider Z be set such that

       A2: a in Z and

       A3: Z in A by TARSKI:def 4;

      consider K be set such that

       A4: K c= B and

       A5: Z c= ( union K) by A1, A3;

      ex S be set st a in S & S in K by A2, A5, TARSKI:def 4;

      hence thesis by A4, TARSKI:def 4;

    end;

    registration

      let m be non zero Nat;

      cluster (2 |^ m) -> even;

      coherence

      proof

        defpred P[ Nat] means $1 is non empty implies (2 |^ $1) is even;

        

         A1: for k be Nat holds P[k] implies P[(k + 1)]

        proof

          let k be Nat;

          assume that P[k] and (k + 1) is non empty;

          (2 |^ (k + 1)) = (2 * (2 |^ k)) by NEWTON: 6;

          hence thesis;

        end;

        

         A2: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A2, A1);

        hence thesis;

      end;

    end

    registration

      let n be even Nat, m be non zero Nat;

      cluster (n |^ m) -> even;

      coherence

      proof

        defpred P[ Nat] means $1 is non empty implies (n |^ $1) is even;

        

         A1: P[k] implies P[(k + 1)]

        proof

          assume that P[k] and (k + 1) is non empty;

          (n |^ (k + 1)) = (n * (n |^ k)) by NEWTON: 6;

          hence thesis;

        end;

        

         A2: P[ 0 ];

         P[k] from NAT_1:sch 2( A2, A1);

        hence thesis;

      end;

    end

    theorem :: JORDAN1D:2

    

     Th2: r <> 0 implies ((1 / r) * (r |^ (i + 1))) = (r |^ i)

    proof

      assume

       A1: r <> 0 ;

      

      thus ((1 / r) * (r |^ (i + 1))) = ((1 / r) * ((r |^ i) * r)) by NEWTON: 6

      .= (((1 / r) * r) * (r |^ i))

      .= (1 * (r |^ i)) by A1, XCMPLX_1: 106

      .= (r |^ i);

    end;

     Lm5:

    now

      let m be Real;

      assume 2 <= m;

      then (2 * m) >= (2 * 2) by XREAL_1: 66;

      then ((2 * m) - 2) >= (4 - 2) by XREAL_1: 9;

      hence ((2 * m) - 2) >= 0 ;

    end;

     Lm6:

    now

      let m be Real;

      assume 1 <= m;

      then (2 * m) >= (2 * 1) by XREAL_1: 66;

      then ((2 * m) - 1) >= (2 - 1) by XREAL_1: 9;

      hence ((2 * m) - 1) >= 0 ;

    end;

    

     Lm7: for m st 2 <= m holds ((2 * m) - 2) = ((2 * m) -' 2) by Lm5, XREAL_0:def 2;

    

     Lm8: for m st 1 <= m holds ((2 * m) - 1) = ((2 * m) -' 1) by Lm6, XREAL_0:def 2;

     Lm9:

    now

      let m;

      assume

       A1: m >= 1;

      then (2 * m) >= (2 * 1) by XREAL_1: 64;

      then ((2 * m) - 1) >= (2 - 1) by XREAL_1: 9;

      then

       A2: ((2 * m) -' 1) >= 1 by A1, Lm8;

      

      thus (((2 * m) -' 2) + 1) = ((((2 * m) -' 1) -' 1) + 1) by NAT_D: 45

      .= ((2 * m) -' 1) by A2, XREAL_1: 235;

    end;

    

     Lm10: for x be Real st 2 <= m holds ((x / (2 |^ i)) * (m - 2)) = ((x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2))

    proof

      let x be Real;

      assume 2 <= m;

      then

       A1: ((2 * m) - 2) >= 0 by Lm5;

      

      thus ((x / (2 |^ i)) * (m - 2)) = (x / ((2 |^ i) / (m - 2))) by XCMPLX_1: 81

      .= (x / (((2 |^ i) * 2) / ((m - 2) * 2))) by XCMPLX_1: 91

      .= ((x / ((2 |^ i) * 2)) * ((m - 2) * 2)) by XCMPLX_1: 81

      .= ((x / (2 |^ (i + 1))) * (((2 * m) - 2) - 2)) by NEWTON: 6

      .= ((x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2)) by A1, XREAL_0:def 2;

    end;

    

     Lm11: 2 <= m implies 1 <= ((2 * m) -' 2)

    proof

      assume

       A1: 2 <= m;

      then (2 * 2) <= (2 * m) by XREAL_1: 66;

      then

       A2: (4 - 2) <= ((2 * m) - 2) by XREAL_1: 9;

      ((2 * m) -' 2) = ((2 * m) - 2) by A1, Lm7;

      hence thesis by A2, XXREAL_0: 2;

    end;

    

     Lm12: 1 <= m implies 1 <= ((2 * m) -' 1)

    proof

      assume

       A1: 1 <= m;

      then (2 * 1) <= (2 * m) by XREAL_1: 66;

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

      hence thesis by A1, Lm8;

    end;

    

     Lm13: m < ((2 |^ i) + 3) implies ((2 * m) -' 2) < ((2 |^ (i + 1)) + 3)

    proof

      per cases by NAT_1: 25;

        suppose m = 0 or m = 1;

        hence thesis by NAT_2: 8;

      end;

        suppose 1 < m;

        then

         A1: (1 + 1) <= m by NAT_1: 13;

        assume m < ((2 |^ i) + 3);

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

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

        then ((2 * m) + (2 * 1)) <= ((2 * (2 |^ i)) + (2 * 3));

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

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

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

        then

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

        ((2 |^ (i + 1)) + 2) < ((2 |^ (i + 1)) + 3) by XREAL_1: 6;

        hence thesis by A2, XXREAL_0: 2;

      end;

    end;

     Lm14:

    now

      let m;

      assume 2 <= m;

      

      hence ((((2 * m) -' 2) + 1) - 2) = ((((2 * m) - 2) + 1) - 2) by Lm7

      .= ((2 * m) - 3);

    end;

    begin

    theorem :: JORDAN1D:3

    

     Th3: 2 <= m & m < ( len ( Gauge (D,i))) & 1 <= a & a <= ( len ( Gauge (D,i))) & 1 <= b & b <= ( len ( Gauge (D,(i + 1)))) implies ((( Gauge (D,i)) * (m,a)) `1 ) = ((( Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1 )

    proof

      set I = ( Gauge (D,i)), J = ( Gauge (D,(i + 1))), z = ( N-bound D), e = ( E-bound D), s = ( S-bound D), w = ( W-bound D);

      assume that

       A1: 2 <= m and

       A2: m < ( len I) and

       A3: 1 <= a and

       A4: a <= ( len I) and

       A5: 1 <= b and

       A6: b <= ( len J);

      m < ((2 |^ i) + 3) by A2, JORDAN8:def 1;

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

      then

       A7: ((2 * m) -' 2) <= ( len J) by JORDAN8:def 1;

      

       A8: ( len J) = ( width J) by JORDAN8:def 1;

      1 <= ((2 * m) -' 2) by A1, Lm11;

      then

       A9: [((2 * m) -' 2), b] in ( Indices J) by A5, A6, A8, A7, MATRIX_0: 30;

      

       A10: ( len I) = ( width I) by JORDAN8:def 1;

      1 <= m by A1, XXREAL_0: 2;

      then [m, a] in ( Indices I) by A2, A3, A4, A10, MATRIX_0: 30;

      

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

      .= (w + (((e - w) / (2 |^ i)) * (m - 2))) by EUCLID: 52

      .= (w + (((e - w) / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2))) by A1, Lm10

      .= ( |[(w + (((e - w) / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2))), (s + (((z - s) / (2 |^ (i + 1))) * (b - 2)))]| `1 ) by EUCLID: 52

      .= ((J * (((2 * m) -' 2),b)) `1 ) by A9, JORDAN8:def 1;

    end;

    theorem :: JORDAN1D:4

    

     Th4: 2 <= n & n < ( len ( Gauge (D,i))) & 1 <= a & a <= ( len ( Gauge (D,i))) & 1 <= b & b <= ( len ( Gauge (D,(i + 1)))) implies ((( Gauge (D,i)) * (a,n)) `2 ) = ((( Gauge (D,(i + 1))) * (b,((2 * n) -' 2))) `2 )

    proof

      set I = ( Gauge (D,i)), J = ( Gauge (D,(i + 1))), z = ( N-bound D), e = ( E-bound D), s = ( S-bound D), w = ( W-bound D);

      assume that

       A1: 2 <= n and

       A2: n < ( len I) and

       A3: 1 <= a and

       A4: a <= ( len I) and

       A5: 1 <= b and

       A6: b <= ( len J);

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

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

      then

       A7: ((2 * n) -' 2) <= ( len J) by JORDAN8:def 1;

      

       A8: ( len J) = ( width J) by JORDAN8:def 1;

      1 <= ((2 * n) -' 2) by A1, Lm11;

      then

       A9: [b, ((2 * n) -' 2)] in ( Indices J) by A5, A6, A8, A7, MATRIX_0: 30;

      

       A10: ( len I) = ( width I) by JORDAN8:def 1;

      1 <= n by A1, XXREAL_0: 2;

      then [a, n] in ( Indices I) by A2, A3, A4, A10, MATRIX_0: 30;

      

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

      .= (s + (((z - s) / (2 |^ i)) * (n - 2))) by EUCLID: 52

      .= (s + (((z - s) / (2 |^ (i + 1))) * (((2 * n) -' 2) - 2))) by A1, Lm10

      .= ( |[(w + (((e - w) / (2 |^ (i + 1))) * (b - 2))), (s + (((z - s) / (2 |^ (i + 1))) * (((2 * n) -' 2) - 2)))]| `2 ) by EUCLID: 52

      .= ((J * (b,((2 * n) -' 2))) `2 ) by A9, JORDAN8:def 1;

    end;

    

     Lm15: (m + 1) < ( len ( Gauge (D,i))) implies ((2 * m) -' 1) < ( len ( Gauge (D,(i + 1))))

    proof

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

      then (m + 1) < ((2 |^ i) + 3) by JORDAN8:def 1;

      then ((2 * (m + 1)) -' 2) < ((2 |^ (i + 1)) + 3) by Lm13;

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

      then

       A1: (2 * m) < ((2 |^ (i + 1)) + 3) by NAT_D: 34;

      ((2 * m) -' 1) <= (2 * m) by NAT_D: 44;

      then ((2 * m) -' 1) < ((2 |^ (i + 1)) + 3) by A1, XXREAL_0: 2;

      hence thesis by JORDAN8:def 1;

    end;

    theorem :: JORDAN1D:5

    

     Th5: for D be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds 2 <= m & (m + 1) < ( len ( Gauge (D,i))) & 2 <= n & (n + 1) < ( len ( Gauge (D,i))) implies ( cell (( Gauge (D,i)),m,n)) = (((( cell (( Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ ( cell (( Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ ( cell (( Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ ( cell (( Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))))

    proof

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

      set I = ( Gauge (D,i)), J = ( Gauge (D,(i + 1))), z = ( N-bound D), e = ( E-bound D), s = ( S-bound D), w = ( W-bound D);

      assume that

       A1: 2 <= m and

       A2: (m + 1) < ( len I) and

       A3: 2 <= n and

       A4: (n + 1) < ( len I);

      

       A5: ( len J) = ( width J) by JORDAN8:def 1;

      

       A6: ((2 * n) - 3) < ((2 * n) - 2) by XREAL_1: 15;

      (z - s) >= 0 by SPRECT_1: 22, XREAL_1: 48;

      then (((z - s) / (2 |^ (i + 1))) * ((2 * n) - 3)) <= (((z - s) / (2 |^ (i + 1))) * ((2 * n) - 2)) by A6, XREAL_1: 64;

      then

       A7: (s + (((z - s) / (2 |^ (i + 1))) * ((2 * n) - 3))) <= (s + (((z - s) / (2 |^ (i + 1))) * ((2 * n) - 2))) by XREAL_1: 6;

      

       A8: m <= (m + 1) by NAT_1: 11;

      

       A9: (((2 * (n + 1)) -' 2) - 2) = ((((2 * n) + (2 * 1)) -' 2) - 2)

      .= ((2 * n) - 2) by NAT_D: 34;

      

       A10: 1 <= (((2 * m) -' 2) + 1) by NAT_1: 11;

      

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

      

       A12: 1 <= n by A3, XXREAL_0: 2;

      then

       A13: 1 <= ((2 * n) -' 1) by Lm12;

      ((2 * n) -' 1) <= (2 * n) by NAT_D: 35;

      then

       A14: 1 <= (2 * n) by A13, XXREAL_0: 2;

      

       A15: (((2 * n) -' 1) + 1) = (2 * n) by A12, Lm12, NAT_D: 43;

      

       A16: ((2 * n) -' 1) < ( len J) by A4, Lm15;

      then (((2 * n) -' 1) + 1) <= ( len J) by NAT_1: 13;

      then [1, (2 * n)] in ( Indices J) by A5, A15, A11, A14, MATRIX_0: 30;

      

      then

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

      .= (s + (((z - s) / (2 |^ (i + 1))) * ((2 * n) - 2))) by EUCLID: 52;

      

       A18: ((2 * m) -' 1) = ((2 * m) - 1) by A1, Lm8, XXREAL_0: 2;

      

       A19: ((((2 * m) -' 2) + 1) - 2) = ((2 * m) - 3) by A1, Lm14;

      

       A20: 1 <= (((2 * n) -' 2) + 1) by NAT_1: 11;

      

       A21: ((2 * m) -' 1) < ( len J) by A2, Lm15;

      

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

      

       A23: (((2 * n) -' 2) + 1) = ((2 * n) -' 1) by A3, Lm9, XXREAL_0: 2;

      

       A24: (((2 * (m + 1)) -' 2) - 2) = ((((2 * m) + (2 * 1)) -' 2) - 2)

      .= ((2 * m) - 2) by NAT_D: 34;

      

       A25: m < ( len I) by A2, NAT_1: 13;

      then m < ((2 |^ i) + 3) by JORDAN8:def 1;

      then ((2 * m) -' 2) < ((2 |^ (i + 1)) + 3) by Lm13;

      then

       A26: ((2 * m) -' 2) < ( len J) by JORDAN8:def 1;

      then (((2 * m) -' 2) + 1) <= ( len J) by NAT_1: 13;

      then [(((2 * m) -' 2) + 1), 1] in ( Indices J) by A5, A11, A10, MATRIX_0: 30;

      

      then

       A27: ((J * ((((2 * m) -' 2) + 1),1)) `1 ) = ( |[(w + (((e - w) / (2 |^ (i + 1))) * ((((2 * m) -' 2) + 1) - 2))), (s + (((z - s) / (2 |^ (i + 1))) * (1 - 2)))]| `1 ) by JORDAN8:def 1

      .= (w + (((e - w) / (2 |^ (i + 1))) * ((((2 * m) -' 2) + 1) - 2))) by EUCLID: 52;

      

       A28: 1 <= m by A1, XXREAL_0: 2;

      then

       A29: 1 < ( len I) by A25, XXREAL_0: 2;

      then

       A30: ((I * (m,1)) `1 ) = ((J * (((2 * m) -' 2),1)) `1 ) by A1, A25, A11, Th3;

      

       A31: ( len I) = ( width I) by JORDAN8:def 1;

      then

       A32: n < ( width I) by A4, NAT_1: 13;

      then

       A33: ((I * (1,n)) `2 ) = ((J * (1,((2 * n) -' 2))) `2 ) by A3, A31, A29, A11, Th4;

      

       A34: 1 <= ((2 * m) -' 2) by A1, Lm11;

      then

       A35: ( cell (J,((2 * m) -' 2),((2 * n) -' 1))) = { |[r, q]| where r,q be Real : ((J * (((2 * m) -' 2),1)) `1 ) <= r & r <= ((J * ((((2 * m) -' 2) + 1),1)) `1 ) & ((J * (1,((2 * n) -' 1))) `2 ) <= q & q <= ((J * (1,(((2 * n) -' 1) + 1))) `2 ) } by A5, A13, A26, A16, GOBRD11: 32;

      ((2 * m) -' 2) = ((2 * m) - 2) by A1, Lm7;

      then ((2 * m) -' 2) < ((2 * m) -' 1) by A18, XREAL_1: 15;

      then

       A36: ((J * (((2 * m) -' 2),1)) `1 ) < ((J * (((2 * m) -' 1),1)) `1 ) by A5, A11, A34, A21, GOBOARD5: 3;

      

       A37: ((2 * n) -' 1) = ((2 * n) - 1) by A3, Lm8, XXREAL_0: 2;

      

       A38: ((((2 * n) -' 2) + 1) - 2) = ((2 * n) - 3) by A3, Lm14;

      n < ((2 |^ i) + 3) by A31, A32, JORDAN8:def 1;

      then ((2 * n) -' 2) < ((2 |^ (i + 1)) + 3) by Lm13;

      then

       A39: ((2 * n) -' 2) < ( width J) by A5, JORDAN8:def 1;

      then (((2 * n) -' 2) + 1) <= ( len J) by A5, NAT_1: 13;

      then [1, (((2 * n) -' 2) + 1)] in ( Indices J) by A5, A11, A20, MATRIX_0: 30;

      

      then

       A40: ((J * (1,(((2 * n) -' 2) + 1))) `2 ) = ( |[(w + (((e - w) / (2 |^ (i + 1))) * (1 - 2))), (s + (((z - s) / (2 |^ (i + 1))) * ((((2 * n) -' 2) + 1) - 2)))]| `2 ) by JORDAN8:def 1

      .= (s + (((z - s) / (2 |^ (i + 1))) * ((((2 * n) -' 2) + 1) - 2))) by EUCLID: 52;

      

       A41: 1 <= ((2 * n) -' 2) by A3, Lm11;

      then

       A42: ( cell (J,((2 * m) -' 2),((2 * n) -' 2))) = { |[r, q]| where r,q be Real : ((J * (((2 * m) -' 2),1)) `1 ) <= r & r <= ((J * ((((2 * m) -' 2) + 1),1)) `1 ) & ((J * (1,((2 * n) -' 2))) `2 ) <= q & q <= ((J * (1,(((2 * n) -' 2) + 1))) `2 ) } by A34, A26, A39, GOBRD11: 32;

      

       A43: 1 <= ((2 * m) -' 1) by A28, Lm12;

      then

       A44: ( cell (J,((2 * m) -' 1),((2 * n) -' 2))) = { |[r, q]| where r,q be Real : ((J * (((2 * m) -' 1),1)) `1 ) <= r & r <= ((J * ((((2 * m) -' 1) + 1),1)) `1 ) & ((J * (1,((2 * n) -' 2))) `2 ) <= q & q <= ((J * (1,(((2 * n) -' 2) + 1))) `2 ) } by A41, A39, A21, GOBRD11: 32;

      

       A45: ( cell (J,((2 * m) -' 1),((2 * n) -' 1))) = { |[r, q]| where r,q be Real : ((J * (((2 * m) -' 1),1)) `1 ) <= r & r <= ((J * ((((2 * m) -' 1) + 1),1)) `1 ) & ((J * (1,((2 * n) -' 1))) `2 ) <= q & q <= ((J * (1,(((2 * n) -' 1) + 1))) `2 ) } by A5, A13, A43, A16, A21, GOBRD11: 32;

      

       A46: ( cell (I,m,n)) = { |[r, q]| where r,q be Real : ((I * (m,1)) `1 ) <= r & r <= ((I * ((m + 1),1)) `1 ) & ((I * (1,n)) `2 ) <= q & q <= ((I * (1,(n + 1))) `2 ) } by A28, A12, A25, A32, GOBRD11: 32;

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

      then [1, (n + 1)] in ( Indices I) by A4, A31, A29, MATRIX_0: 30;

      

      then

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

      .= (s + (((z - s) / (2 |^ i)) * ((n + 1) - 2))) by EUCLID: 52

      .= (s + (((z - s) / (2 |^ (i + 1))) * (((2 * (n + 1)) -' 2) - 2))) by A3, A22, Lm10, XXREAL_0: 2;

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

      then [(m + 1), 1] in ( Indices I) by A2, A31, A29, MATRIX_0: 30;

      

      then

       A48: ((I * ((m + 1),1)) `1 ) = ( |[(w + (((e - w) / (2 |^ i)) * ((m + 1) - 2))), (s + (((z - s) / (2 |^ i)) * (1 - 2)))]| `1 ) by JORDAN8:def 1

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

      .= (w + (((e - w) / (2 |^ (i + 1))) * (((2 * (m + 1)) -' 2) - 2))) by A1, A8, Lm10, XXREAL_0: 2;

      ((2 * n) -' 2) = ((2 * n) - 2) by A3, Lm7;

      then ((2 * n) -' 2) < ((2 * n) -' 1) by A37, XREAL_1: 15;

      then

       A49: ((J * (1,((2 * n) -' 2))) `2 ) < ((J * (1,((2 * n) -' 1))) `2 ) by A5, A11, A41, A16, GOBOARD5: 4;

      

       A50: (((2 * m) -' 1) + 1) = (2 * m) by A28, Lm12, NAT_D: 43;

      ((2 * m) -' 1) <= (2 * m) by NAT_D: 35;

      then

       A51: 1 <= (2 * m) by A43, XXREAL_0: 2;

      (((2 * m) -' 1) + 1) <= ( len J) by A21, NAT_1: 13;

      then [(2 * m), 1] in ( Indices J) by A5, A50, A11, A51, MATRIX_0: 30;

      

      then

       A52: ((J * ((2 * m),1)) `1 ) = ( |[(w + (((e - w) / (2 |^ (i + 1))) * ((2 * m) - 2))), (s + (((z - s) / (2 |^ (i + 1))) * (1 - 2)))]| `1 ) by JORDAN8:def 1

      .= (w + (((e - w) / (2 |^ (i + 1))) * ((2 * m) - 2))) by EUCLID: 52;

      

       A53: (((2 * m) -' 2) + 1) = ((2 * m) -' 1) by A1, Lm9, XXREAL_0: 2;

      thus ( cell (( Gauge (D,i)),m,n)) c= (((( cell (( Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ ( cell (( Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ ( cell (( Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ ( cell (( Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))))

      proof

        let x be object;

        assume x in ( cell (I,m,n));

        then

        consider r,q be Real such that

         A54: x = |[r, q]| and

         A55: ((I * (m,1)) `1 ) <= r and

         A56: r <= ((I * ((m + 1),1)) `1 ) and

         A57: ((I * (1,n)) `2 ) <= q and

         A58: q <= ((I * (1,(n + 1))) `2 ) by A46;

        r <= ((J * (((2 * m) -' 1),1)) `1 ) & q <= ((J * (1,((2 * n) -' 1))) `2 ) or r >= ((J * (((2 * m) -' 1),1)) `1 ) & q <= ((J * (1,((2 * n) -' 1))) `2 ) or r <= ((J * (((2 * m) -' 1),1)) `1 ) & q >= ((J * (1,((2 * n) -' 1))) `2 ) or r >= ((J * (((2 * m) -' 1),1)) `1 ) & q >= ((J * (1,((2 * n) -' 1))) `2 );

        then |[r, q]| in ( cell (J,((2 * m) -' 2),((2 * n) -' 2))) or |[r, q]| in ( cell (J,((2 * m) -' 1),((2 * n) -' 2))) or |[r, q]| in ( cell (J,((2 * m) -' 2),((2 * n) -' 1))) or |[r, q]| in ( cell (J,((2 * m) -' 1),((2 * n) -' 1))) by A53, A23, A24, A9, A50, A15, A42, A44, A35, A45, A52, A17, A48, A47, A30, A33, A55, A56, A57, A58;

        hence thesis by A54, Lm3;

      end;

      let x be object;

      

       A59: ((2 * m) - 3) < ((2 * m) - 2) by XREAL_1: 15;

      (e - w) >= 0 by SPRECT_1: 21, XREAL_1: 48;

      then (((e - w) / (2 |^ (i + 1))) * ((2 * m) - 3)) <= (((e - w) / (2 |^ (i + 1))) * ((2 * m) - 2)) by A59, XREAL_1: 64;

      then

       A60: (w + (((e - w) / (2 |^ (i + 1))) * ((2 * m) - 3))) <= (w + (((e - w) / (2 |^ (i + 1))) * ((2 * m) - 2))) by XREAL_1: 6;

      assume

       A61: x in (((( cell (( Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ ( cell (( Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ ( cell (( Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ ( cell (( Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))));

      per cases by A61, Lm3;

        suppose x in ( cell (( Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2)));

        then

        consider r,q be Real such that

         A62: x = |[r, q]| and

         A63: ((J * (((2 * m) -' 2),1)) `1 ) <= r and

         A64: r <= ((J * ((((2 * m) -' 2) + 1),1)) `1 ) and

         A65: ((J * (1,((2 * n) -' 2))) `2 ) <= q and

         A66: q <= ((J * (1,(((2 * n) -' 2) + 1))) `2 ) by A42;

        

         A67: q <= ((I * (1,(n + 1))) `2 ) by A38, A9, A7, A40, A47, A66, XXREAL_0: 2;

        r <= ((I * ((m + 1),1)) `1 ) by A19, A24, A60, A27, A48, A64, XXREAL_0: 2;

        hence thesis by A46, A30, A33, A62, A63, A65, A67;

      end;

        suppose x in ( cell (( Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)));

        then

        consider r,q be Real such that

         A68: x = |[r, q]| and

         A69: ((J * (((2 * m) -' 1),1)) `1 ) <= r and

         A70: r <= ((J * ((((2 * m) -' 1) + 1),1)) `1 ) and

         A71: ((J * (1,((2 * n) -' 2))) `2 ) <= q and

         A72: q <= ((J * (1,(((2 * n) -' 2) + 1))) `2 ) by A44;

        

         A73: ((I * (m,1)) `1 ) <= r by A30, A36, A69, XXREAL_0: 2;

        q <= ((I * (1,(n + 1))) `2 ) by A38, A9, A7, A40, A47, A72, XXREAL_0: 2;

        hence thesis by A24, A50, A46, A52, A48, A33, A68, A70, A71, A73;

      end;

        suppose x in ( cell (( Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)));

        then

        consider r,q be Real such that

         A74: x = |[r, q]| and

         A75: ((J * (((2 * m) -' 2),1)) `1 ) <= r and

         A76: r <= ((J * ((((2 * m) -' 2) + 1),1)) `1 ) and

         A77: ((J * (1,((2 * n) -' 1))) `2 ) <= q and

         A78: q <= ((J * (1,(((2 * n) -' 1) + 1))) `2 ) by A35;

        

         A79: ((I * (1,n)) `2 ) <= q by A33, A49, A77, XXREAL_0: 2;

        r <= ((I * ((m + 1),1)) `1 ) by A19, A24, A60, A27, A48, A76, XXREAL_0: 2;

        hence thesis by A9, A15, A46, A17, A47, A30, A74, A75, A78, A79;

      end;

        suppose x in ( cell (( Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)));

        then

        consider r,q be Real such that

         A80: x = |[r, q]| and

         A81: ((J * (((2 * m) -' 1),1)) `1 ) <= r and

         A82: r <= ((J * ((((2 * m) -' 1) + 1),1)) `1 ) and

         A83: ((J * (1,((2 * n) -' 1))) `2 ) <= q and

         A84: q <= ((J * (1,(((2 * n) -' 1) + 1))) `2 ) by A45;

        

         A85: ((I * (1,n)) `2 ) <= q by A33, A49, A83, XXREAL_0: 2;

        ((I * (m,1)) `1 ) <= r by A30, A36, A81, XXREAL_0: 2;

        hence thesis by A24, A9, A50, A15, A46, A52, A17, A48, A47, A80, A82, A84, A85;

      end;

    end;

    theorem :: JORDAN1D:6

    for D be compact non vertical non horizontal Subset of ( TOP-REAL 2), k be Nat holds 2 <= m & (m + 1) < ( len ( Gauge (D,i))) & 2 <= n & (n + 1) < ( len ( Gauge (D,i))) implies ( cell (( Gauge (D,i)),m,n)) = ( union { ( cell (( Gauge (D,(i + k))),a,b)) where a,b be Nat : ((((2 |^ k) * m) - (2 |^ (k + 1))) + 2) <= a & a <= ((((2 |^ k) * m) - (2 |^ k)) + 1) & ((((2 |^ k) * n) - (2 |^ (k + 1))) + 2) <= b & b <= ((((2 |^ k) * n) - (2 |^ k)) + 1) })

    proof

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

      let k be Nat;

      assume that

       A1: 2 <= m and

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

       A3: 2 <= n and

       A4: (n + 1) < ( len ( Gauge (D,i)));

      deffunc F( Nat) = { ( cell (( Gauge (D,(i + $1))),a,b)) where a,b be Nat : ((((2 |^ $1) * m) - (2 |^ ($1 + 1))) + 2) <= a & a <= ((((2 |^ $1) * m) - (2 |^ $1)) + 1) & ((((2 |^ $1) * n) - (2 |^ ($1 + 1))) + 2) <= b & b <= ((((2 |^ $1) * n) - (2 |^ $1)) + 1) };

      defpred P[ Nat] means ( cell (( Gauge (D,i)),m,n)) = ( union F($1));

      

       A5: for w be Nat st P[w] holds P[(w + 1)]

      proof

        let w be Nat such that

         A6: P[w];

        

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

        

         A8: ((i + w) + 1) = (i + (w + 1));

         F(+) is_finer_than F(w)

        proof

           A9:

          now

            let a be odd Nat;

            consider e be Nat such that

             A10: a = ((2 * e) + 1) by ABIAN: 9;

            

             A11: ((2 * e) mod 2) = 0 by NAT_D: 13;

            

            thus (2 * ((a div 2) + 1)) = ((2 * (a div 2)) + (2 * 1))

            .= ((2 * (((2 * e) div 2) + (1 div 2))) + 2) by A10, A11, NAT_D: 19

            .= ((2 * (e + 0 )) + (1 + 1)) by Lm1, NAT_D: 18

            .= (a + 1) by A10;

          end;

           A12:

          now

            let m;

            

            thus (2 * ((((2 |^ w) * m) - (2 |^ w)) + 1)) = (((2 * ((2 |^ w) * m)) - (2 * (2 |^ w))) + (1 + 1))

            .= ((((2 * (2 |^ w)) * m) - (2 |^ (w + 1))) + (1 + 1)) by NEWTON: 6

            .= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + (1 + 1)) by NEWTON: 6

            .= (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1);

          end;

           A13:

          now

            let m;

            let a be odd Nat;

            assume a <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1);

            then

             A14: (a + 1) <= (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1) by XREAL_1: 6;

            (2 * ((((2 |^ w) * m) - (2 |^ w)) + 1)) = (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1) by A12;

            then (2 * ((a div 2) + 1)) <= (2 * ((((2 |^ w) * m) - (2 |^ w)) + 1)) by A9, A14;

            hence ((a div 2) + 1) <= ((((2 |^ w) * m) - (2 |^ w)) + 1) by XREAL_1: 68;

          end;

           A15:

          now

            let a be even Nat;

            

             A16: ex e be Nat st a = (2 * e) by ABIAN:def 2;

            

            thus (2 * ((a div 2) + 1)) = ((2 * (a div 2)) + (2 * 1))

            .= (a + 2) by A16, NAT_D: 18;

          end;

           A17:

          now

            let m;

            let a be even Nat;

            assume a <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1);

            then a < ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) by XXREAL_0: 1;

            then (a + 1) <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) by INT_1: 7;

            then ((a + 1) + 1) <= (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1) by XREAL_1: 6;

            then

             A18: (a + (1 + 1)) <= (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1);

            (2 * ((((2 |^ w) * m) - (2 |^ w)) + 1)) = (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1) by A12;

            then (2 * ((a div 2) + 1)) <= (2 * ((((2 |^ w) * m) - (2 |^ w)) + 1)) by A15, A18;

            hence ((a div 2) + 1) <= ((((2 |^ w) * m) - (2 |^ w)) + 1) by XREAL_1: 68;

          end;

          let X be set;

          assume X in F(+);

          then

          consider a,b be Nat such that

           A19: X = ( cell (( Gauge (D,(i + (w + 1)))),a,b)) and

           A20: ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) <= a and

           A21: a <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) and

           A22: ((((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2) <= b and

           A23: b <= ((((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1);

          take Y = ( cell (( Gauge (D,(i + w))),((a div 2) + 1),((b div 2) + 1)));

          deffunc G( Nat, Nat) = ( cell (( Gauge (D,((i + w) + 1))),((2 * ((a div 2) + 1)) -' $1),((2 * ((b div 2) + 1)) -' $2)));

           A24:

          now

            let a, m;

            

             A25: (2 |^ ((w + 1) + 1)) = ((2 |^ (w + 1)) * (2 |^ 1)) by NEWTON: 8

            .= ((2 |^ (w + 1)) * 2);

            assume 2 <= m;

            then ((2 |^ (w + 1)) * m) >= (2 |^ ((w + 1) + 1)) by A25, XREAL_1: 64;

            then 0 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) by XREAL_1: 48;

            hence ( 0 + 2) <= ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) by XREAL_1: 6;

          end;

          then 2 <= ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) by A1;

          then 2 <= a by A20, XXREAL_0: 2;

          then (2 div 2) <= (a div 2) by NAT_2: 24;

          then

           A26: (1 + 1) <= ((a div 2) + 1) by Lm2, XREAL_1: 6;

           A27:

          now

            let a, m;

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

            then (m + 1) < ((2 |^ i) + 3) by JORDAN8:def 1;

            then ((2 * (m + 1)) -' 2) < ((2 |^ (i + 1)) + 3) by Lm13;

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

            then (2 * m) < ((2 |^ (i + 1)) + 3) by NAT_D: 34;

            then ((1 / 2) * (2 * m)) < ((1 / 2) * ((2 |^ (i + 1)) + 3)) by XREAL_1: 68;

            then m < (((1 / 2) * (2 |^ (i + 1))) + ((1 / 2) * 3));

            then

             A28: m < ((2 |^ i) + ((1 / 2) * 3)) by Th2;

            ((2 |^ i) + (3 / 2)) < ((2 |^ i) + 2) by XREAL_1: 6;

            then m < ((2 |^ i) + 2) by A28, XXREAL_0: 2;

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

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

            then ((2 |^ (w + 1)) * (m - 1)) <= ((2 |^ (w + 1)) * (2 |^ i)) by XREAL_1: 64;

            then (((2 |^ (w + 1)) * (m - 1)) + 5) < (((2 |^ (w + 1)) * (2 |^ i)) + 6) by XREAL_1: 8;

            then

             A29: (((2 |^ (w + 1)) * (m - 1)) + 5) < ((2 |^ ((w + 1) + i)) + 6) by NEWTON: 8;

            then

             A30: ((((2 |^ (w + 1)) * (m - 1)) + 1) + (3 + 1)) < ((2 * (2 |^ (i + w))) + 6) by A8, NEWTON: 6;

            

             A31: (((((2 |^ (w + 1)) * (m - 1)) + 1) + 3) + 1) < ((2 * (2 |^ (i + w))) + (2 * 3)) by A8, A29, NEWTON: 6;

            assume a <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1);

            then (a + 3) <= (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3) by XREAL_1: 6;

            then

             A32: ((a + 3) + 0 ) < ((((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3) + 1) by XREAL_1: 8;

            then

             A33: ((a + 3) + 1) <= ((((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3) + 1) by INT_1: 7;

            now

              per cases ;

                suppose

                 A34: a is odd;

                (2 * (((a div 2) + 1) + 1)) = ((2 * ((a div 2) + 1)) + (2 * 1))

                .= ((a + 1) + 2) by A9, A34

                .= (a + (1 + 2));

                hence (2 * (((a div 2) + 1) + 1)) < (2 * ((2 |^ (i + w)) + 3)) by A32, A30, XXREAL_0: 2;

              end;

                suppose

                 A35: a is even;

                (2 * (((a div 2) + 1) + 1)) = ((2 * ((a div 2) + 1)) + (2 * 1))

                .= ((a + 2) + 2) by A15, A35

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

                hence (2 * (((a div 2) + 1) + 1)) < (2 * ((2 |^ (i + w)) + 3)) by A33, A31, XXREAL_0: 2;

              end;

            end;

            hence (((a div 2) + 1) + 1) < ( len ( Gauge (D,(i + w)))) by A7, XREAL_1: 64;

          end;

          then

           A36: (((b div 2) + 1) + 1) < ( len ( Gauge (D,(i + w)))) by A4, A23;

          2 <= ((((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2) by A3, A24;

          then 2 <= b by A22, XXREAL_0: 2;

          then (2 div 2) <= (b div 2) by NAT_2: 24;

          then

           A37: (1 + 1) <= ((b div 2) + 1) by Lm2, XREAL_1: 6;

          (((a div 2) + 1) + 1) < ( len ( Gauge (D,(i + w)))) by A2, A21, A27;

          then

           A38: Y = ((( G(,) \/ G(,)) \/ G(,)) \/ G(,)) by A26, A37, A36, Th5;

           A39:

          now

            let m;

            

            thus (2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2)) = (((2 * ((2 |^ w) * m)) - (2 * (2 |^ (w + 1)))) + (2 + 2))

            .= ((((2 * (2 |^ w)) * m) - (2 |^ ((w + 1) + 1))) + (2 + 2)) by NEWTON: 6

            .= ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (2 + 2)) by NEWTON: 6

            .= (((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2);

          end;

           A40:

          now

            let m;

            let a be even Nat;

            assume ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) <= a;

            then

             A41: (((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2) <= (a + 2) by XREAL_1: 6;

            (2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2)) = (((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2) by A39;

            then (2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2)) <= (2 * ((a div 2) + 1)) by A15, A41;

            hence ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= ((a div 2) + 1) by XREAL_1: 68;

          end;

           A42:

          now

            let m;

            let a be odd Nat;

            assume ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) <= a;

            then ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) < a by XXREAL_0: 1;

            then (((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 1) < (a + 1) by XREAL_1: 6;

            then

             A43: ((((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 1) + 1) <= (a + 1) by INT_1: 7;

            (2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2)) = (((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2) by A39;

            then (2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2)) <= (2 * ((a div 2) + 1)) by A9, A43;

            hence ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= ((a div 2) + 1) by XREAL_1: 68;

          end;

          per cases ;

            suppose

             A44: a is odd & b is odd;

            then

             A45: ((((2 |^ w) * n) - (2 |^ (w + 1))) + 2) <= ((b div 2) + 1) by A22, A42;

            

             A46: ((a div 2) + 1) <= ((((2 |^ w) * m) - (2 |^ w)) + 1) by A21, A13, A44;

            

             A47: ((b div 2) + 1) <= ((((2 |^ w) * n) - (2 |^ w)) + 1) by A23, A13, A44;

            ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= ((a div 2) + 1) by A20, A42, A44;

            hence Y in F(w) by A46, A45, A47;

            

             A48: ((2 * ((b div 2) + 1)) -' 1) = ((b + 1) -' 1) by A9, A44

            .= b by NAT_D: 34;

            ((2 * ((a div 2) + 1)) -' 1) = ((a + 1) -' 1) by A9, A44

            .= a by NAT_D: 34;

            hence thesis by A19, A38, A48, XBOOLE_1: 7;

          end;

            suppose

             A49: a is odd & b is even;

            then

             A50: ((((2 |^ w) * n) - (2 |^ (w + 1))) + 2) <= ((b div 2) + 1) by A22, A40;

            

             A51: ((a div 2) + 1) <= ((((2 |^ w) * m) - (2 |^ w)) + 1) by A21, A13, A49;

            

             A52: ((b div 2) + 1) <= ((((2 |^ w) * n) - (2 |^ w)) + 1) by A23, A17, A49;

            ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= ((a div 2) + 1) by A20, A42, A49;

            hence Y in F(w) by A51, A50, A52;

            

             A53: ( G(,) \/ G(,)) c= (( G(,) \/ G(,)) \/ G(,)) by XBOOLE_1: 7;

             G(,) c= ( G(,) \/ G(,)) by XBOOLE_1: 7;

            then

             A54: G(,) c= (( G(,) \/ G(,)) \/ G(,)) by A53;

            

             A55: (( G(,) \/ G(,)) \/ G(,)) c= Y by A38, XBOOLE_1: 7;

            

             A56: ((2 * ((b div 2) + 1)) -' 2) = ((b + 2) -' 2) by A15, A49

            .= b by NAT_D: 34;

            ((2 * ((a div 2) + 1)) -' 1) = ((a + 1) -' 1) by A9, A49

            .= a by NAT_D: 34;

            hence thesis by A19, A56, A54, A55;

          end;

            suppose

             A57: a is even & b is odd;

            then

             A58: ((((2 |^ w) * n) - (2 |^ (w + 1))) + 2) <= ((b div 2) + 1) by A22, A42;

            

             A59: ((a div 2) + 1) <= ((((2 |^ w) * m) - (2 |^ w)) + 1) by A21, A17, A57;

            

             A60: ((b div 2) + 1) <= ((((2 |^ w) * n) - (2 |^ w)) + 1) by A23, A13, A57;

            ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= ((a div 2) + 1) by A20, A40, A57;

            hence Y in F(w) by A59, A58, A60;

            

             A61: G(,) c= (( G(,) \/ G(,)) \/ G(,)) by XBOOLE_1: 7;

            

             A62: (( G(,) \/ G(,)) \/ G(,)) c= Y by A38, XBOOLE_1: 7;

            

             A63: ((2 * ((b div 2) + 1)) -' 1) = ((b + 1) -' 1) by A9, A57

            .= b by NAT_D: 34;

            ((2 * ((a div 2) + 1)) -' 2) = ((a + 2) -' 2) by A15, A57

            .= a by NAT_D: 34;

            hence thesis by A19, A63, A61, A62;

          end;

            suppose

             A64: a is even & b is even;

            then

             A65: ((((2 |^ w) * n) - (2 |^ (w + 1))) + 2) <= ((b div 2) + 1) by A22, A40;

            

             A66: ((a div 2) + 1) <= ((((2 |^ w) * m) - (2 |^ w)) + 1) by A21, A17, A64;

            

             A67: ((b div 2) + 1) <= ((((2 |^ w) * n) - (2 |^ w)) + 1) by A23, A17, A64;

            ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= ((a div 2) + 1) by A20, A40, A64;

            hence Y in F(w) by A66, A65, A67;

            

             A68: ((2 * ((b div 2) + 1)) -' 2) = ((b + 2) -' 2) by A15, A64

            .= b by NAT_D: 34;

            ((2 * ((a div 2) + 1)) -' 2) = ((a + 2) -' 2) by A15, A64

            .= a by NAT_D: 34;

            then X c= ( G(,) \/ (( G(,) \/ G(,)) \/ G(,))) by A19, A68, XBOOLE_1: 7;

            then X c= (( G(,) \/ ( G(,) \/ G(,))) \/ G(,)) by XBOOLE_1: 4;

            hence thesis by A38, XBOOLE_1: 4;

          end;

        end;

        then

         A69: ( union F(+)) c= ( union F(w)) by SETFAM_1: 13;

        

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

        for x be set st x in F(w) holds ex K be set st K c= F(+) & x c= ( union K)

        proof

          let x be set;

          assume x in F(w);

          then

          consider a, b such that

           A71: x = ( cell (( Gauge (D,(i + w))),a,b)) and

           A72: ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= a and

           A73: a <= ((((2 |^ w) * m) - (2 |^ w)) + 1) and

           A74: ((((2 |^ w) * n) - (2 |^ (w + 1))) + 2) <= b and

           A75: b <= ((((2 |^ w) * n) - (2 |^ w)) + 1);

          take K = {( cell (( Gauge (D,((i + w) + 1))),((2 * a) -' 2),((2 * b) -' 2))), ( cell (( Gauge (D,((i + w) + 1))),((2 * a) -' 1),((2 * b) -' 2))), ( cell (( Gauge (D,((i + w) + 1))),((2 * a) -' 2),((2 * b) -' 1))), ( cell (( Gauge (D,((i + w) + 1))),((2 * a) -' 1),((2 * b) -' 1)))};

           A76:

          now

            let m;

            assume 2 <= m;

            then ((2 |^ w) * m) >= ((2 |^ w) * 2) by XREAL_1: 64;

            then ((2 |^ w) * m) >= (2 |^ (w + 1)) by NEWTON: 6;

            then 0 <= (((2 |^ w) * m) - (2 |^ (w + 1))) by XREAL_1: 48;

            hence ( 0 + 2) <= ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) by XREAL_1: 6;

          end;

          then

           A77: 2 <= ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) by A1;

          then

           A78: 2 <= a by A72, XXREAL_0: 2;

          

           A79: ((2 * a) -' 2) = ((2 * a) - 2) by A72, A77, Lm7, XXREAL_0: 2;

          

           A80: 2 <= ((((2 |^ w) * n) - (2 |^ (w + 1))) + 2) by A3, A76;

          then

           A81: 2 <= b by A74, XXREAL_0: 2;

          

           A82: ((2 * b) -' 2) = ((2 * b) - 2) by A74, A80, Lm7, XXREAL_0: 2;

          ((2 * b) -' 1) = ((2 * b) - 1) by A81, Lm8, XXREAL_0: 2;

          then

           A83: ((2 * b) -' 2) < ((2 * b) -' 1) by A82, XREAL_1: 15;

          ((2 * a) -' 1) = ((2 * a) - 1) by A78, Lm8, XXREAL_0: 2;

          then

           A84: ((2 * a) -' 2) < ((2 * a) -' 1) by A79, XREAL_1: 15;

          hereby

             A85:

            now

              let a, m;

              assume

               A86: 2 <= a;

              assume a <= ((((2 |^ w) * m) - (2 |^ w)) + 1);

              then (2 * a) <= (2 * ((((2 |^ w) * m) - (2 |^ w)) + 1)) by XREAL_1: 64;

              then (2 * a) <= ((((2 * (2 |^ w)) * m) - (2 * (2 |^ w))) + 2);

              then (2 * a) <= ((((2 |^ (w + 1)) * m) - (2 * (2 |^ w))) + 2) by NEWTON: 6;

              then (2 * a) <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2) by NEWTON: 6;

              then ((2 * a) - 2) <= (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2) - 2) by XREAL_1: 9;

              then

               A87: ((2 * a) -' 2) <= (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2) - 2) by A86, Lm7;

              ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 0 ) < ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) by XREAL_1: 6;

              hence ((2 * a) -' 2) < ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) by A87, XXREAL_0: 2;

            end;

            then

             A88: ((2 * a) -' 2) < ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) by A73, A78;

            then (((2 * a) -' 2) + 1) <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) by INT_1: 7;

            then

             A89: ((2 * a) -' 1) <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) by A78, Lm9, XXREAL_0: 2;

             A90:

            now

              let a, m;

              assume

               A91: 2 <= a;

              assume ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= a;

              then (2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2)) <= (2 * a) by XREAL_1: 64;

              then ((((2 * (2 |^ w)) * m) - (2 * (2 |^ (w + 1)))) + 4) <= (2 * a);

              then ((((2 |^ (w + 1)) * m) - (2 * (2 |^ (w + 1)))) + 4) <= (2 * a) by NEWTON: 6;

              then ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 4) <= (2 * a) by NEWTON: 6;

              then (((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 4) - 2) <= ((2 * a) - 2) by XREAL_1: 9;

              hence ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2)) <= ((2 * a) -' 2) by A91, Lm7;

            end;

            then

             A92: ((((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2) <= ((2 * b) -' 2) by A74, A81;

            then

             A93: ((((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2) <= ((2 * b) -' 1) by A83, XXREAL_0: 2;

            let q be object;

            assume q in K;

            then

             A94: q = ( cell (( Gauge (D,(i + (w + 1)))),((2 * a) -' 2),((2 * b) -' 2))) or q = ( cell (( Gauge (D,(i + (w + 1)))),((2 * a) -' 1),((2 * b) -' 2))) or q = ( cell (( Gauge (D,(i + (w + 1)))),((2 * a) -' 2),((2 * b) -' 1))) or q = ( cell (( Gauge (D,(i + (w + 1)))),((2 * a) -' 1),((2 * b) -' 1))) by ENUMSET1:def 2;

            

             A95: ((2 * b) -' 2) < ((((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1) by A75, A81, A85;

            then (((2 * b) -' 2) + 1) <= ((((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1) by INT_1: 7;

            then

             A96: ((2 * b) -' 1) <= ((((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1) by A81, Lm9, XXREAL_0: 2;

            

             A97: ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) <= ((2 * a) -' 2) by A72, A78, A90;

            then ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) <= ((2 * a) -' 1) by A84, XXREAL_0: 2;

            hence q in F(+) by A97, A88, A89, A92, A95, A96, A93, A94;

          end;

           A98:

          now

            let a, m;

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

            then ((m + 1) - 2) < (((2 |^ i) + 3) - 2) by A70, XREAL_1: 9;

            then (m - 1) < ((2 |^ i) + (3 - 2));

            then (m - 1) <= ((2 |^ i) + 0 ) by INT_1: 7;

            then ((2 |^ w) * (m - 1)) <= ((2 |^ w) * (2 |^ i)) by XREAL_1: 64;

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

            then

             A99: (((2 |^ w) * (m - 1)) + 3) <= ((2 |^ (w + i)) + 3) by XREAL_1: 6;

            assume a <= ((((2 |^ w) * m) - (2 |^ w)) + 1);

            then (a + 1) <= (((((2 |^ w) * m) - (2 |^ w)) + 1) + 1) by XREAL_1: 6;

            then (a + 1) < ((((((2 |^ w) * m) - (2 |^ w)) + 1) + 1) + 1) by XREAL_1: 145;

            hence (a + 1) < ( len ( Gauge (D,(i + w)))) by A7, A99, XXREAL_0: 2;

          end;

          then

           A100: (b + 1) < ( len ( Gauge (D,(i + w)))) by A4, A75;

          (a + 1) < ( len ( Gauge (D,(i + w)))) by A2, A73, A98;

          then ( cell (( Gauge (D,(i + w))),a,b)) = (((( cell (( Gauge (D,((i + w) + 1))),((2 * a) -' 2),((2 * b) -' 2))) \/ ( cell (( Gauge (D,((i + w) + 1))),((2 * a) -' 1),((2 * b) -' 2)))) \/ ( cell (( Gauge (D,((i + w) + 1))),((2 * a) -' 2),((2 * b) -' 1)))) \/ ( cell (( Gauge (D,((i + w) + 1))),((2 * a) -' 1),((2 * b) -' 1)))) by A78, A81, A100, Th5;

          hence thesis by A71, Lm4;

        end;

        hence ( cell (( Gauge (D,i)),m,n)) c= ( union F(+)) by A6, Th1;

        let d be object;

        assume d in ( union F(+));

        hence thesis by A6, A69;

      end;

       A101:

      now

        let m;

        

         A102: ((2 |^ 0 ) * m) = (1 * m) by NEWTON: 4;

        

        hence ((((2 |^ 0 ) * m) - (2 |^ ( 0 + 1))) + 2) = ((m - 2) + 2)

        .= m;

        

        thus ((((2 |^ 0 ) * m) - (2 |^ 0 )) + 1) = ((m - 1) + 1) by A102, NEWTON: 4

        .= m;

      end;

       F(0) = {( cell (( Gauge (D,i)),m,n))}

      proof

        hereby

          let x be object;

          assume x in F(0);

          then

          consider a, b such that

           A103: x = ( cell (( Gauge (D,(i + 0 ))),a,b)) and

           A104: ((((2 |^ 0 ) * m) - (2 |^ ( 0 + 1))) + 2) <= a and

           A105: a <= ((((2 |^ 0 ) * m) - (2 |^ 0 )) + 1) and

           A106: ((((2 |^ 0 ) * n) - (2 |^ ( 0 + 1))) + 2) <= b and

           A107: b <= ((((2 |^ 0 ) * n) - (2 |^ 0 )) + 1);

           A108:

          now

            let a, m;

            assume that

             A109: ((((2 |^ 0 ) * m) - (2 |^ ( 0 + 1))) + 2) <= a and

             A110: a <= ((((2 |^ 0 ) * m) - (2 |^ 0 )) + 1);

            

             A111: ((((2 |^ 0 ) * m) - (2 |^ 0 )) + 1) = m by A101;

            ((((2 |^ 0 ) * m) - (2 |^ ( 0 + 1))) + 2) = m by A101;

            hence a = m by A109, A110, A111, XXREAL_0: 1;

          end;

          then

           A112: b = n by A106, A107;

          a = m by A104, A105, A108;

          hence x in {( cell (( Gauge (D,i)),m,n))} by A103, A112, TARSKI:def 1;

        end;

        let x be object;

        assume x in {( cell (( Gauge (D,i)),m,n))};

        then

         A113: x = ( cell (( Gauge (D,(i + 0 ))),m,n)) by TARSKI:def 1;

        

         A114: m <= ((((2 |^ 0 ) * m) - (2 |^ 0 )) + 1) by A101;

        

         A115: n <= ((((2 |^ 0 ) * n) - (2 |^ 0 )) + 1) by A101;

        

         A116: ((((2 |^ 0 ) * n) - (2 |^ ( 0 + 1))) + 2) <= n by A101;

        ((((2 |^ 0 ) * m) - (2 |^ ( 0 + 1))) + 2) <= m by A101;

        hence thesis by A113, A114, A116, A115;

      end;

      then

       A117: P[ 0 ] by ZFMISC_1: 25;

      for w be Nat holds P[w] from NAT_1:sch 2( A117, A5);

      hence thesis;

    end;

    theorem :: JORDAN1D:7

    

     Th7: ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( N-max C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n))))

    proof

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

       A1: (( north_halfline ( N-max C)) /\ ( L~ ( Cage (C,n)))) = {p} by JORDAN1A: 86, PSCOMP_1: 42;

      

       A2: p in (( north_halfline ( N-max C)) /\ ( L~ ( Cage (C,n)))) by A1, TARSKI:def 1;

      then

       A3: p in ( north_halfline ( N-max C)) by XBOOLE_0:def 4;

      p in ( L~ ( Cage (C,n))) by A2, XBOOLE_0:def 4;

      then

      consider i be Nat such that

       A4: 1 <= i and

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

       A6: p in ( LSeg (( Cage (C,n)),i)) by SPPOL_2: 13;

      take i;

      

       A7: ( LSeg (( Cage (C,n)),i)) = ( LSeg ((( Cage (C,n)) /. i),(( Cage (C,n)) /. (i + 1)))) by A4, A5, TOPREAL1:def 3;

      

       A8: ( len ( Gauge (C,n))) >= 4 by JORDAN8: 10;

      then

       A9: 1 < ( len ( Gauge (C,n))) by XXREAL_0: 2;

      

       A10: ((( len ( Gauge (C,n))) -' 1) + 1) = ( len ( Gauge (C,n))) by A8, XREAL_1: 235, XXREAL_0: 2;

      then

       A11: (( len ( Gauge (C,n))) -' 1) < ( len ( Gauge (C,n))) by NAT_1: 13;

      

       A12: ( N-max C) = |[(( N-max C) `1 ), (( N-max C) `2 )]| by EUCLID: 53;

      

       A13: (( len ( Gauge (C,n))) -' 1) <= ( len ( Gauge (C,n))) by NAT_D: 44;

      

       A14: (( N-max C) `2 ) = ( N-bound C) by EUCLID: 52

      .= ((( Gauge (C,n)) * (1,(( len ( Gauge (C,n))) -' 1))) `2 ) by A9, JORDAN8: 14;

      

       A15: ( N-max C) in ( N-most C) by PSCOMP_1: 42;

      

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

      thus

       A17: 1 <= i & i < ( len ( Cage (C,n))) by A4, A5, NAT_1: 13;

      then

       A18: ((( Cage (C,n)) /. i) `2 ) = (p `2 ) by A3, A6, A15, A7, JORDAN1A: 78, SPPOL_1: 40;

      

       A19: ((( Cage (C,n)) /. (i + 1)) `2 ) = (p `2 ) by A3, A6, A17, A15, A7, JORDAN1A: 78, SPPOL_1: 40;

      

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

      then

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

       A21: [i1, j1] in ( Indices ( Gauge (C,n))) and

       A22: (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (i1,j1)) and

       A23: [i2, j2] in ( Indices ( Gauge (C,n))) and

       A24: (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (i2,j2)) and

       A25: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A4, A5, JORDAN8: 3;

      

       A26: 1 <= i1 by A21, MATRIX_0: 32;

      

       A27: j2 <= ( width ( Gauge (C,n))) by A23, MATRIX_0: 32;

      

       A28: i1 <= ( len ( Gauge (C,n))) by A21, MATRIX_0: 32;

      

       A29: 1 <= j1 by A21, MATRIX_0: 32;

      (p `2 ) = ( N-bound ( L~ ( Cage (C,n)))) by A2, JORDAN1A: 82, PSCOMP_1: 42;

      then ((( Gauge (C,n)) * (i1,j1)) `2 ) = ((( Gauge (C,n)) * (i1,( len ( Gauge (C,n))))) `2 ) by A22, A18, A26, A28, JORDAN1A: 70;

      then

       A30: ( len ( Gauge (C,n))) <= j1 by A16, A26, A28, A29, GOBOARD5: 4;

      

       A31: j1 <= ( width ( Gauge (C,n))) by A21, MATRIX_0: 32;

      then

       A32: j1 = ( len ( Gauge (C,n))) by A16, A30, XXREAL_0: 1;

      

       A33: 1 <= j2 by A23, MATRIX_0: 32;

      

       A34: j1 = j2

      proof

        assume j1 <> j2;

        then j1 < j2 or j2 < j1 by XXREAL_0: 1;

        hence contradiction by A22, A24, A25, A18, A19, A26, A28, A29, A27, A33, A31, GOBOARD5: 4;

      end;

      

       A35: 1 <= i2 by A23, MATRIX_0: 32;

      

       A36: i2 <= ( len ( Gauge (C,n))) by A23, MATRIX_0: 32;

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

      then

       A37: ((( Cage (C,n)) /. i) `1 ) <= ((( Cage (C,n)) /. (i + 1)) `1 ) by A4, A5, A21, A22, A23, A24, A25, A16, A26, A36, A29, A27, A34, A30, JORDAN10: 4, JORDAN1A: 18;

      then (p `1 ) <= ((( Cage (C,n)) /. (i + 1)) `1 ) by A6, A7, TOPREAL1: 3;

      then (( N-max C) `1 ) <= ((( Gauge (C,n)) * ((i1 + 1),( len ( Gauge (C,n))))) `1 ) by A3, A4, A5, A21, A22, A23, A24, A25, A16, A34, A32, JORDAN10: 4, TOPREAL1:def 10;

      then

       A38: (( N-max C) `1 ) <= ((( Gauge (C,n)) * ((i1 + 1),1)) `1 ) by A4, A5, A21, A22, A23, A24, A25, A16, A35, A36, A34, A30, A9, GOBOARD5: 2, JORDAN10: 4;

      ((( Cage (C,n)) /. i) `1 ) <= (p `1 ) by A6, A7, A37, TOPREAL1: 3;

      then ((( Gauge (C,n)) * (i1,( len ( Gauge (C,n))))) `1 ) <= (( N-max C) `1 ) by A3, A22, A32, TOPREAL1:def 10;

      then

       A39: ((( Gauge (C,n)) * (i1,1)) `1 ) <= (( N-max C) `1 ) by A16, A26, A28, A9, GOBOARD5: 2;

      ( len ( Gauge (C,n))) >= (1 + 1) by A8, XXREAL_0: 2;

      then

       A40: (( len ( Gauge (C,n))) - 1) >= 1 by XREAL_1: 19;

      then (( len ( Gauge (C,n))) -' 1) >= 1 by XREAL_0:def 2;

      then ((( Gauge (C,n)) * (1,j1)) `2 ) >= (( N-max C) `2 ) by A16, A32, A9, A14, A13, SPRECT_3: 12;

      then

       A41: ( N-max C) in { |[r, s]| where r,s be Real : ((( Gauge (C,n)) * (i1,1)) `1 ) <= r & r <= ((( Gauge (C,n)) * ((i1 + 1),1)) `1 ) & ((( Gauge (C,n)) * (1,(j1 -' 1))) `2 ) <= s & s <= ((( Gauge (C,n)) * (1,j1)) `2 ) } by A32, A14, A39, A38, A12;

      

       A42: 1 <= i1 by A21, MATRIX_0: 32;

      i1 < ( len ( Gauge (C,n))) by A4, A5, A21, A22, A23, A24, A25, A16, A36, A34, A30, JORDAN10: 4, NAT_1: 13;

      then ( N-max C) in ( cell (( Gauge (C,n)),i1,(j1 -' 1))) by A16, A32, A42, A40, A10, A11, A41, GOBRD11: 32;

      hence thesis by A4, A5, A20, A21, A22, A23, A24, A25, A16, A34, A30, GOBRD13: 24, JORDAN10: 4;

    end;

    theorem :: JORDAN1D:8

    ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( N-max C) in ( right_cell (( Cage (C,n)),i))

    proof

      

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

      consider i be Nat such that

       A2: 1 <= i and

       A3: i < ( len ( Cage (C,n))) and

       A4: ( N-max C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) by Th7;

      take i;

      thus 1 <= i & i < ( len ( Cage (C,n))) by A2, A3;

      (i + 1) <= ( len ( Cage (C,n))) by A3, NAT_1: 13;

      then ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) c= ( right_cell (( Cage (C,n)),i)) by A2, A1, GOBRD13: 33;

      hence thesis by A4;

    end;

    theorem :: JORDAN1D:9

    

     Th9: ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( E-min C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n))))

    proof

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

       A1: (( east_halfline ( E-min C)) /\ ( L~ ( Cage (C,n)))) = {p} by JORDAN1A: 87, PSCOMP_1: 50;

      

       A2: p in (( east_halfline ( E-min C)) /\ ( L~ ( Cage (C,n)))) by A1, TARSKI:def 1;

      then

       A3: p in ( east_halfline ( E-min C)) by XBOOLE_0:def 4;

      ( len ( Gauge (C,n))) < (( len ( Gauge (C,n))) + 1) by NAT_1: 13;

      then

       A4: (( len ( Gauge (C,n))) - 1) < ( len ( Gauge (C,n))) by XREAL_1: 19;

      

       A5: (( len ( Gauge (C,n))) -' 1) <= ( len ( Gauge (C,n))) by NAT_D: 44;

      

       A6: ( E-min C) = |[(( E-min C) `1 ), (( E-min C) `2 )]| by EUCLID: 53;

      

       A7: ( len ( Gauge (C,n))) >= 4 by JORDAN8: 10;

      then

       A8: 1 < ( len ( Gauge (C,n))) by XXREAL_0: 2;

      

       A9: ((( len ( Gauge (C,n))) -' 1) + 1) = ( len ( Gauge (C,n))) by A7, XREAL_1: 235, XXREAL_0: 2;

      

       A10: (( E-min C) `1 ) = ( E-bound C) by EUCLID: 52

      .= ((( Gauge (C,n)) * ((( len ( Gauge (C,n))) -' 1),1)) `1 ) by A8, JORDAN8: 12;

      

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

      

       A12: ( E-min C) in ( E-most C) by PSCOMP_1: 50;

      p in ( L~ ( Cage (C,n))) by A2, XBOOLE_0:def 4;

      then

      consider i be Nat such that

       A13: 1 <= i and

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

       A15: p in ( LSeg (( Cage (C,n)),i)) by SPPOL_2: 13;

      take i;

      

       A16: ( LSeg (( Cage (C,n)),i)) = ( LSeg ((( Cage (C,n)) /. i),(( Cage (C,n)) /. (i + 1)))) by A13, A14, TOPREAL1:def 3;

      thus

       A17: 1 <= i & i < ( len ( Cage (C,n))) by A13, A14, NAT_1: 13;

      then

       A18: ((( Cage (C,n)) /. i) `1 ) = (p `1 ) by A3, A15, A12, A16, JORDAN1A: 79, SPPOL_1: 41;

      

       A19: ((( Cage (C,n)) /. (i + 1)) `1 ) = (p `1 ) by A3, A15, A17, A12, A16, JORDAN1A: 79, SPPOL_1: 41;

      

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

      then

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

       A21: [i1, j1] in ( Indices ( Gauge (C,n))) and

       A22: (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (i1,j1)) and

       A23: [i2, j2] in ( Indices ( Gauge (C,n))) and

       A24: (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (i2,j2)) and

       A25: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A13, A14, JORDAN8: 3;

      

       A26: 1 <= i1 by A21, MATRIX_0: 32;

      

       A27: j1 <= ( width ( Gauge (C,n))) by A21, MATRIX_0: 32;

      

       A28: j2 <= ( width ( Gauge (C,n))) by A23, MATRIX_0: 32;

      

       A29: 1 <= i2 by A23, MATRIX_0: 32;

      

       A30: 1 <= j1 by A21, MATRIX_0: 32;

      (p `1 ) = ( E-bound ( L~ ( Cage (C,n)))) by A2, JORDAN1A: 83, PSCOMP_1: 50;

      then ((( Gauge (C,n)) * (i1,j1)) `1 ) = ((( Gauge (C,n)) * (( len ( Gauge (C,n))),j1)) `1 ) by A22, A18, A11, A30, A27, JORDAN1A: 71;

      then

       A31: ( len ( Gauge (C,n))) <= i1 by A26, A30, A27, GOBOARD5: 3;

      

       A32: i1 <= ( len ( Gauge (C,n))) by A21, MATRIX_0: 32;

      then

       A33: i1 = ( len ( Gauge (C,n))) by A31, XXREAL_0: 1;

      

       A34: i2 <= ( len ( Gauge (C,n))) by A23, MATRIX_0: 32;

      

       A35: i1 = i2

      proof

        assume i1 <> i2;

        then i1 < i2 or i2 < i1 by XXREAL_0: 1;

        hence contradiction by A22, A24, A25, A18, A19, A26, A32, A29, A34, A30, A28, GOBOARD5: 3;

      end;

      then

       A36: j2 < ( width ( Gauge (C,n))) by A13, A14, A21, A22, A23, A24, A25, A27, A31, JORDAN10: 1, NAT_1: 13;

      

       A37: 1 <= j2 by A23, MATRIX_0: 32;

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

      then

       A38: ((( Cage (C,n)) /. i) `2 ) >= ((( Cage (C,n)) /. (i + 1)) `2 ) by A13, A14, A21, A22, A23, A24, A25, A26, A32, A37, A27, A35, A31, JORDAN10: 1, JORDAN1A: 19;

      then (p `2 ) <= ((( Cage (C,n)) /. i) `2 ) by A15, A16, TOPREAL1: 4;

      then (( E-min C) `2 ) <= ((( Gauge (C,n)) * (( len ( Gauge (C,n))),(j2 + 1))) `2 ) by A3, A13, A14, A21, A22, A23, A24, A25, A35, A33, JORDAN10: 1, TOPREAL1:def 11;

      then

       A39: (( E-min C) `2 ) <= ((( Gauge (C,n)) * (1,(j2 + 1))) `2 ) by A13, A14, A21, A22, A23, A24, A25, A29, A30, A27, A35, A33, GOBOARD5: 1, JORDAN10: 1;

      ((( Cage (C,n)) /. (i + 1)) `2 ) <= (p `2 ) by A15, A16, A38, TOPREAL1: 4;

      then ((( Gauge (C,n)) * (( len ( Gauge (C,n))),j2)) `2 ) <= (( E-min C) `2 ) by A3, A24, A35, A33, TOPREAL1:def 11;

      then

       A40: ((( Gauge (C,n)) * (1,j2)) `2 ) <= (( E-min C) `2 ) by A29, A28, A37, A35, A33, GOBOARD5: 1;

      ( len ( Gauge (C,n))) >= (1 + 1) by A7, XXREAL_0: 2;

      then

       A41: (( len ( Gauge (C,n))) - 1) >= 1 by XREAL_1: 19;

      then (( len ( Gauge (C,n))) -' 1) >= 1 by XREAL_0:def 2;

      then ((( Gauge (C,n)) * (i1,1)) `1 ) >= (( E-min C) `1 ) by A11, A33, A8, A10, A5, SPRECT_3: 13;

      then ( E-min C) in { |[r, s]| where r,s be Real : ((( Gauge (C,n)) * ((( len ( Gauge (C,n))) -' 1),1)) `1 ) <= r & r <= ((( Gauge (C,n)) * (( len ( Gauge (C,n))),1)) `1 ) & ((( Gauge (C,n)) * (1,j2)) `2 ) <= s & s <= ((( Gauge (C,n)) * (1,(j2 + 1))) `2 ) } by A33, A10, A40, A39, A6;

      then ( E-min C) in ( cell (( Gauge (C,n)),(i2 -' 1),j2)) by A37, A35, A33, A36, A41, A4, A9, GOBRD11: 32;

      hence thesis by A13, A14, A20, A21, A22, A23, A24, A25, A35, A31, GOBRD13: 28, JORDAN10: 1;

    end;

    theorem :: JORDAN1D:10

    ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( E-min C) in ( right_cell (( Cage (C,n)),i))

    proof

      

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

      consider i be Nat such that

       A2: 1 <= i and

       A3: i < ( len ( Cage (C,n))) and

       A4: ( E-min C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) by Th9;

      take i;

      thus 1 <= i & i < ( len ( Cage (C,n))) by A2, A3;

      (i + 1) <= ( len ( Cage (C,n))) by A3, NAT_1: 13;

      then ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) c= ( right_cell (( Cage (C,n)),i)) by A2, A1, GOBRD13: 33;

      hence thesis by A4;

    end;

    theorem :: JORDAN1D:11

    

     Th11: ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( E-max C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n))))

    proof

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

       A1: (( east_halfline ( E-max C)) /\ ( L~ ( Cage (C,n)))) = {p} by JORDAN1A: 87, PSCOMP_1: 50;

      

       A2: p in (( east_halfline ( E-max C)) /\ ( L~ ( Cage (C,n)))) by A1, TARSKI:def 1;

      then

       A3: p in ( east_halfline ( E-max C)) by XBOOLE_0:def 4;

      ( len ( Gauge (C,n))) < (( len ( Gauge (C,n))) + 1) by NAT_1: 13;

      then

       A4: (( len ( Gauge (C,n))) - 1) < ( len ( Gauge (C,n))) by XREAL_1: 19;

      

       A5: (( len ( Gauge (C,n))) -' 1) <= ( len ( Gauge (C,n))) by NAT_D: 44;

      

       A6: ( len ( Gauge (C,n))) >= 4 by JORDAN8: 10;

      then

       A7: 1 < ( len ( Gauge (C,n))) by XXREAL_0: 2;

      

       A8: ((( len ( Gauge (C,n))) -' 1) + 1) = ( len ( Gauge (C,n))) by A6, XREAL_1: 235, XXREAL_0: 2;

      

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

      .= ((( Gauge (C,n)) * ((( len ( Gauge (C,n))) -' 1),1)) `1 ) by A7, JORDAN8: 12;

      

       A10: ( E-max C) = |[(( E-max C) `1 ), (( E-max C) `2 )]| by EUCLID: 53;

      

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

      

       A12: ( E-max C) in ( E-most C) by PSCOMP_1: 50;

      p in ( L~ ( Cage (C,n))) by A2, XBOOLE_0:def 4;

      then

      consider i be Nat such that

       A13: 1 <= i and

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

       A15: p in ( LSeg (( Cage (C,n)),i)) by SPPOL_2: 13;

      take i;

      

       A16: ( LSeg (( Cage (C,n)),i)) = ( LSeg ((( Cage (C,n)) /. i),(( Cage (C,n)) /. (i + 1)))) by A13, A14, TOPREAL1:def 3;

      thus

       A17: 1 <= i & i < ( len ( Cage (C,n))) by A13, A14, NAT_1: 13;

      then

       A18: ((( Cage (C,n)) /. i) `1 ) = (p `1 ) by A3, A15, A12, A16, JORDAN1A: 79, SPPOL_1: 41;

      

       A19: ((( Cage (C,n)) /. (i + 1)) `1 ) = (p `1 ) by A3, A15, A17, A12, A16, JORDAN1A: 79, SPPOL_1: 41;

      

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

      then

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

       A21: [i1, j1] in ( Indices ( Gauge (C,n))) and

       A22: (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (i1,j1)) and

       A23: [i2, j2] in ( Indices ( Gauge (C,n))) and

       A24: (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (i2,j2)) and

       A25: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A13, A14, JORDAN8: 3;

      

       A26: 1 <= i1 by A21, MATRIX_0: 32;

      

       A27: j1 <= ( width ( Gauge (C,n))) by A21, MATRIX_0: 32;

      

       A28: i2 <= ( len ( Gauge (C,n))) by A23, MATRIX_0: 32;

      

       A29: j2 <= ( width ( Gauge (C,n))) by A23, MATRIX_0: 32;

      

       A30: 1 <= j1 by A21, MATRIX_0: 32;

      (p `1 ) = ( E-bound ( L~ ( Cage (C,n)))) by A2, JORDAN1A: 83, PSCOMP_1: 50;

      then ((( Gauge (C,n)) * (i1,j1)) `1 ) = ((( Gauge (C,n)) * (( len ( Gauge (C,n))),j1)) `1 ) by A22, A18, A11, A30, A27, JORDAN1A: 71;

      then

       A31: ( len ( Gauge (C,n))) <= i1 by A26, A30, A27, GOBOARD5: 3;

      

       A32: i1 <= ( len ( Gauge (C,n))) by A21, MATRIX_0: 32;

      then

       A33: i1 = ( len ( Gauge (C,n))) by A31, XXREAL_0: 1;

      

       A34: 1 <= i2 by A23, MATRIX_0: 32;

      

       A35: i1 = i2

      proof

        assume i1 <> i2;

        then i1 < i2 or i2 < i1 by XXREAL_0: 1;

        hence contradiction by A22, A24, A25, A18, A19, A26, A32, A34, A28, A30, A29, GOBOARD5: 3;

      end;

      then

       A36: j2 < ( width ( Gauge (C,n))) by A13, A14, A21, A22, A23, A24, A25, A27, A31, JORDAN10: 1, NAT_1: 13;

      

       A37: 1 <= j2 by A23, MATRIX_0: 32;

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

      then

       A38: ((( Cage (C,n)) /. i) `2 ) >= ((( Cage (C,n)) /. (i + 1)) `2 ) by A13, A14, A21, A22, A23, A24, A25, A26, A32, A37, A27, A35, A31, JORDAN10: 1, JORDAN1A: 19;

      then (p `2 ) <= ((( Cage (C,n)) /. i) `2 ) by A15, A16, TOPREAL1: 4;

      then (( E-max C) `2 ) <= ((( Gauge (C,n)) * (( len ( Gauge (C,n))),(j2 + 1))) `2 ) by A3, A13, A14, A21, A22, A23, A24, A25, A35, A33, JORDAN10: 1, TOPREAL1:def 11;

      then

       A39: (( E-max C) `2 ) <= ((( Gauge (C,n)) * (1,(j2 + 1))) `2 ) by A13, A14, A21, A22, A23, A24, A25, A30, A27, A35, A31, A7, GOBOARD5: 1, JORDAN10: 1;

      ((( Cage (C,n)) /. (i + 1)) `2 ) <= (p `2 ) by A15, A16, A38, TOPREAL1: 4;

      then ((( Gauge (C,n)) * (( len ( Gauge (C,n))),j2)) `2 ) <= (( E-max C) `2 ) by A3, A24, A35, A33, TOPREAL1:def 11;

      then

       A40: ((( Gauge (C,n)) * (1,j2)) `2 ) <= (( E-max C) `2 ) by A29, A37, A7, GOBOARD5: 1;

      ( len ( Gauge (C,n))) >= (1 + 1) by A6, XXREAL_0: 2;

      then

       A41: (( len ( Gauge (C,n))) - 1) >= 1 by XREAL_1: 19;

      then (( len ( Gauge (C,n))) -' 1) >= 1 by XREAL_0:def 2;

      then ((( Gauge (C,n)) * (i1,1)) `1 ) >= (( E-max C) `1 ) by A11, A33, A7, A9, A5, SPRECT_3: 13;

      then ( E-max C) in { |[r, s]| where r,s be Real : ((( Gauge (C,n)) * ((( len ( Gauge (C,n))) -' 1),1)) `1 ) <= r & r <= ((( Gauge (C,n)) * (( len ( Gauge (C,n))),1)) `1 ) & ((( Gauge (C,n)) * (1,j2)) `2 ) <= s & s <= ((( Gauge (C,n)) * (1,(j2 + 1))) `2 ) } by A33, A9, A40, A39, A10;

      then ( E-max C) in ( cell (( Gauge (C,n)),(i2 -' 1),j2)) by A37, A35, A33, A36, A41, A4, A8, GOBRD11: 32;

      hence thesis by A13, A14, A20, A21, A22, A23, A24, A25, A35, A31, GOBRD13: 28, JORDAN10: 1;

    end;

    theorem :: JORDAN1D:12

    ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( E-max C) in ( right_cell (( Cage (C,n)),i))

    proof

      

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

      consider i be Nat such that

       A2: 1 <= i and

       A3: i < ( len ( Cage (C,n))) and

       A4: ( E-max C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) by Th11;

      take i;

      thus 1 <= i & i < ( len ( Cage (C,n))) by A2, A3;

      (i + 1) <= ( len ( Cage (C,n))) by A3, NAT_1: 13;

      then ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) c= ( right_cell (( Cage (C,n)),i)) by A2, A1, GOBRD13: 33;

      hence thesis by A4;

    end;

    theorem :: JORDAN1D:13

    

     Th13: ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( S-min C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n))))

    proof

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

       A1: (( south_halfline ( S-min C)) /\ ( L~ ( Cage (C,n)))) = {p} by JORDAN1A: 88, PSCOMP_1: 58;

      

       A2: p in (( south_halfline ( S-min C)) /\ ( L~ ( Cage (C,n)))) by A1, TARSKI:def 1;

      then

       A3: p in ( south_halfline ( S-min C)) by XBOOLE_0:def 4;

      

       A4: ( S-min C) = |[(( S-min C) `1 ), (( S-min C) `2 )]| by EUCLID: 53;

      

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

      

       A6: ( len ( Gauge (C,n))) >= 4 by JORDAN8: 10;

      then

       A7: 1 < ( len ( Gauge (C,n))) by XXREAL_0: 2;

      p in ( L~ ( Cage (C,n))) by A2, XBOOLE_0:def 4;

      then

      consider i be Nat such that

       A8: 1 <= i and

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

       A10: p in ( LSeg (( Cage (C,n)),i)) by SPPOL_2: 13;

      take i;

      

       A11: ( LSeg (( Cage (C,n)),i)) = ( LSeg ((( Cage (C,n)) /. i),(( Cage (C,n)) /. (i + 1)))) by A8, A9, TOPREAL1:def 3;

      

       A12: (( S-min C) `2 ) = ( S-bound C) by EUCLID: 52

      .= ((( Gauge (C,n)) * (1,2)) `2 ) by A7, JORDAN8: 13;

      

       A13: ( S-min C) in ( S-most C) by PSCOMP_1: 58;

      thus

       A14: 1 <= i & i < ( len ( Cage (C,n))) by A8, A9, NAT_1: 13;

      then

       A15: ((( Cage (C,n)) /. i) `2 ) = (p `2 ) by A3, A10, A13, A11, JORDAN1A: 80, SPPOL_1: 40;

      

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

      then

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

       A17: [i1, j1] in ( Indices ( Gauge (C,n))) and

       A18: (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (i1,j1)) and

       A19: [i2, j2] in ( Indices ( Gauge (C,n))) and

       A20: (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (i2,j2)) and

       A21: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A8, A9, JORDAN8: 3;

      

       A22: 1 <= i1 by A17, MATRIX_0: 32;

      

       A23: 1 <= j2 by A19, MATRIX_0: 32;

      

       A24: i2 <= (i2 + 1) by NAT_1: 11;

      

       A25: j2 <= ( width ( Gauge (C,n))) by A19, MATRIX_0: 32;

      

       A26: i1 <= ( len ( Gauge (C,n))) by A17, MATRIX_0: 32;

      

       A27: j1 <= ( width ( Gauge (C,n))) by A17, MATRIX_0: 32;

      (p `2 ) = ( S-bound ( L~ ( Cage (C,n)))) by A2, JORDAN1A: 84, PSCOMP_1: 58;

      then ((( Gauge (C,n)) * (i1,j1)) `2 ) = ((( Gauge (C,n)) * (i1,1)) `2 ) by A18, A15, A22, A26, JORDAN1A: 72;

      then

       A28: 1 >= j1 by A22, A26, A27, GOBOARD5: 4;

      

       A29: 1 <= j1 by A17, MATRIX_0: 32;

      then

       A30: j1 = 1 by A28, XXREAL_0: 1;

      

       A31: ((( Cage (C,n)) /. (i + 1)) `2 ) = (p `2 ) by A3, A10, A14, A13, A11, JORDAN1A: 80, SPPOL_1: 40;

      

       A32: j1 = j2

      proof

        assume j1 <> j2;

        then j1 < j2 or j2 < j1 by XXREAL_0: 1;

        hence contradiction by A18, A20, A21, A15, A31, A22, A26, A29, A25, A23, A27, GOBOARD5: 4;

      end;

      then

       A33: i2 < ( len ( Gauge (C,n))) by A8, A9, A17, A18, A19, A20, A21, A26, A28, JORDAN10: 3, NAT_1: 13;

      1 <= i2 by A19, MATRIX_0: 32;

      then

       A34: ((( Cage (C,n)) /. i) `1 ) >= ((( Cage (C,n)) /. (i + 1)) `1 ) by A8, A9, A17, A18, A19, A20, A21, A26, A29, A25, A23, A27, A28, A24, JORDAN10: 3, JORDAN1A: 18;

      then (p `1 ) <= ((( Cage (C,n)) /. i) `1 ) by A10, A11, TOPREAL1: 3;

      then

       A35: (( S-min C) `1 ) <= ((( Gauge (C,n)) * ((i2 + 1),1)) `1 ) by A3, A8, A9, A17, A18, A19, A20, A21, A32, A30, JORDAN10: 3, TOPREAL1:def 12;

      ((( Cage (C,n)) /. (i + 1)) `1 ) <= (p `1 ) by A10, A11, A34, TOPREAL1: 3;

      then

       A36: ((( Gauge (C,n)) * (i2,1)) `1 ) <= (( S-min C) `1 ) by A3, A20, A32, A30, TOPREAL1:def 12;

      

       A37: 1 <= i2 by A19, MATRIX_0: 32;

      (1 + 1) <= ( len ( Gauge (C,n))) by A6, XXREAL_0: 2;

      then ((( Gauge (C,n)) * (1,j1)) `2 ) <= (( S-min C) `2 ) by A5, A30, A7, A12, SPRECT_3: 12;

      then ( S-min C) in { |[r, s]| where r,s be Real : ((( Gauge (C,n)) * (i2,1)) `1 ) <= r & r <= ((( Gauge (C,n)) * ((i2 + 1),1)) `1 ) & ((( Gauge (C,n)) * (1,j1)) `2 ) <= s & s <= ((( Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A30, A12, A36, A35, A4;

      then ( S-min C) in ( cell (( Gauge (C,n)),i2,j1)) by A5, A30, A37, A33, A7, GOBRD11: 32;

      hence thesis by A8, A9, A16, A17, A18, A19, A20, A21, A32, A28, GOBRD13: 26, JORDAN10: 3;

    end;

    theorem :: JORDAN1D:14

    ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( S-min C) in ( right_cell (( Cage (C,n)),i))

    proof

      

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

      consider i be Nat such that

       A2: 1 <= i and

       A3: i < ( len ( Cage (C,n))) and

       A4: ( S-min C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) by Th13;

      take i;

      thus 1 <= i & i < ( len ( Cage (C,n))) by A2, A3;

      (i + 1) <= ( len ( Cage (C,n))) by A3, NAT_1: 13;

      then ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) c= ( right_cell (( Cage (C,n)),i)) by A2, A1, GOBRD13: 33;

      hence thesis by A4;

    end;

    theorem :: JORDAN1D:15

    

     Th15: ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( S-max C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n))))

    proof

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

       A1: (( south_halfline ( S-max C)) /\ ( L~ ( Cage (C,n)))) = {p} by JORDAN1A: 88, PSCOMP_1: 58;

      

       A2: p in (( south_halfline ( S-max C)) /\ ( L~ ( Cage (C,n)))) by A1, TARSKI:def 1;

      then

       A3: p in ( south_halfline ( S-max C)) by XBOOLE_0:def 4;

      

       A4: ( S-max C) = |[(( S-max C) `1 ), (( S-max C) `2 )]| by EUCLID: 53;

      

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

      

       A6: ( len ( Gauge (C,n))) >= 4 by JORDAN8: 10;

      then

       A7: 1 < ( len ( Gauge (C,n))) by XXREAL_0: 2;

      p in ( L~ ( Cage (C,n))) by A2, XBOOLE_0:def 4;

      then

      consider i be Nat such that

       A8: 1 <= i and

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

       A10: p in ( LSeg (( Cage (C,n)),i)) by SPPOL_2: 13;

      take i;

      

       A11: ( LSeg (( Cage (C,n)),i)) = ( LSeg ((( Cage (C,n)) /. i),(( Cage (C,n)) /. (i + 1)))) by A8, A9, TOPREAL1:def 3;

      

       A12: (( S-max C) `2 ) = ( S-bound C) by EUCLID: 52

      .= ((( Gauge (C,n)) * (1,2)) `2 ) by A7, JORDAN8: 13;

      

       A13: ( S-max C) in ( S-most C) by PSCOMP_1: 58;

      thus

       A14: 1 <= i & i < ( len ( Cage (C,n))) by A8, A9, NAT_1: 13;

      then

       A15: ((( Cage (C,n)) /. i) `2 ) = (p `2 ) by A3, A10, A13, A11, JORDAN1A: 80, SPPOL_1: 40;

      

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

      then

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

       A17: [i1, j1] in ( Indices ( Gauge (C,n))) and

       A18: (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (i1,j1)) and

       A19: [i2, j2] in ( Indices ( Gauge (C,n))) and

       A20: (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (i2,j2)) and

       A21: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A8, A9, JORDAN8: 3;

      

       A22: 1 <= i1 by A17, MATRIX_0: 32;

      

       A23: 1 <= j2 by A19, MATRIX_0: 32;

      

       A24: i2 <= (i2 + 1) by NAT_1: 11;

      

       A25: j2 <= ( width ( Gauge (C,n))) by A19, MATRIX_0: 32;

      

       A26: i1 <= ( len ( Gauge (C,n))) by A17, MATRIX_0: 32;

      

       A27: j1 <= ( width ( Gauge (C,n))) by A17, MATRIX_0: 32;

      (p `2 ) = ( S-bound ( L~ ( Cage (C,n)))) by A2, JORDAN1A: 84, PSCOMP_1: 58;

      then ((( Gauge (C,n)) * (i1,j1)) `2 ) = ((( Gauge (C,n)) * (i1,1)) `2 ) by A18, A15, A22, A26, JORDAN1A: 72;

      then

       A28: 1 >= j1 by A22, A26, A27, GOBOARD5: 4;

      

       A29: 1 <= j1 by A17, MATRIX_0: 32;

      then

       A30: j1 = 1 by A28, XXREAL_0: 1;

      

       A31: ((( Cage (C,n)) /. (i + 1)) `2 ) = (p `2 ) by A3, A10, A14, A13, A11, JORDAN1A: 80, SPPOL_1: 40;

      

       A32: j1 = j2

      proof

        assume j1 <> j2;

        then j1 < j2 or j2 < j1 by XXREAL_0: 1;

        hence contradiction by A18, A20, A21, A15, A31, A22, A26, A29, A25, A23, A27, GOBOARD5: 4;

      end;

      then

       A33: i2 < ( len ( Gauge (C,n))) by A8, A9, A17, A18, A19, A20, A21, A26, A28, JORDAN10: 3, NAT_1: 13;

      1 <= i2 by A19, MATRIX_0: 32;

      then

       A34: ((( Cage (C,n)) /. i) `1 ) >= ((( Cage (C,n)) /. (i + 1)) `1 ) by A8, A9, A17, A18, A19, A20, A21, A26, A29, A25, A23, A27, A28, A24, JORDAN10: 3, JORDAN1A: 18;

      then (p `1 ) <= ((( Cage (C,n)) /. i) `1 ) by A10, A11, TOPREAL1: 3;

      then

       A35: (( S-max C) `1 ) <= ((( Gauge (C,n)) * ((i2 + 1),1)) `1 ) by A3, A8, A9, A17, A18, A19, A20, A21, A32, A30, JORDAN10: 3, TOPREAL1:def 12;

      ((( Cage (C,n)) /. (i + 1)) `1 ) <= (p `1 ) by A10, A11, A34, TOPREAL1: 3;

      then

       A36: ((( Gauge (C,n)) * (i2,1)) `1 ) <= (( S-max C) `1 ) by A3, A20, A32, A30, TOPREAL1:def 12;

      

       A37: 1 <= i2 by A19, MATRIX_0: 32;

      (1 + 1) <= ( len ( Gauge (C,n))) by A6, XXREAL_0: 2;

      then ((( Gauge (C,n)) * (1,j1)) `2 ) <= (( S-max C) `2 ) by A5, A30, A7, A12, SPRECT_3: 12;

      then ( S-max C) in { |[r, s]| where r,s be Real : ((( Gauge (C,n)) * (i2,1)) `1 ) <= r & r <= ((( Gauge (C,n)) * ((i2 + 1),1)) `1 ) & ((( Gauge (C,n)) * (1,j1)) `2 ) <= s & s <= ((( Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A30, A12, A36, A35, A4;

      then ( S-max C) in ( cell (( Gauge (C,n)),i2,j1)) by A5, A30, A37, A33, A7, GOBRD11: 32;

      hence thesis by A8, A9, A16, A17, A18, A19, A20, A21, A32, A28, GOBRD13: 26, JORDAN10: 3;

    end;

    theorem :: JORDAN1D:16

    ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( S-max C) in ( right_cell (( Cage (C,n)),i))

    proof

      

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

      consider i be Nat such that

       A2: 1 <= i and

       A3: i < ( len ( Cage (C,n))) and

       A4: ( S-max C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) by Th15;

      take i;

      thus 1 <= i & i < ( len ( Cage (C,n))) by A2, A3;

      (i + 1) <= ( len ( Cage (C,n))) by A3, NAT_1: 13;

      then ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) c= ( right_cell (( Cage (C,n)),i)) by A2, A1, GOBRD13: 33;

      hence thesis by A4;

    end;

    theorem :: JORDAN1D:17

    

     Th17: ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( W-min C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n))))

    proof

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

       A1: (( west_halfline ( W-min C)) /\ ( L~ ( Cage (C,n)))) = {p} by JORDAN1A: 89, PSCOMP_1: 34;

      

       A2: p in (( west_halfline ( W-min C)) /\ ( L~ ( Cage (C,n)))) by A1, TARSKI:def 1;

      then

       A3: p in ( west_halfline ( W-min C)) by XBOOLE_0:def 4;

      

       A4: ( W-min C) = |[(( W-min C) `1 ), (( W-min C) `2 )]| by EUCLID: 53;

      

       A5: ( len ( Gauge (C,n))) >= 4 by JORDAN8: 10;

      then

       A6: 1 < ( len ( Gauge (C,n))) by XXREAL_0: 2;

      

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

      .= ((( Gauge (C,n)) * (2,1)) `1 ) by A6, JORDAN8: 11;

      

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

      

       A9: ( W-min C) in ( W-most C) by PSCOMP_1: 34;

      p in ( L~ ( Cage (C,n))) by A2, XBOOLE_0:def 4;

      then

      consider i be Nat such that

       A10: 1 <= i and

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

       A12: p in ( LSeg (( Cage (C,n)),i)) by SPPOL_2: 13;

      take i;

      

       A13: ( LSeg (( Cage (C,n)),i)) = ( LSeg ((( Cage (C,n)) /. i),(( Cage (C,n)) /. (i + 1)))) by A10, A11, TOPREAL1:def 3;

      thus

       A14: 1 <= i & i < ( len ( Cage (C,n))) by A10, A11, NAT_1: 13;

      then

       A15: ((( Cage (C,n)) /. i) `1 ) = (p `1 ) by A3, A12, A9, A13, JORDAN1A: 81, SPPOL_1: 41;

      

       A16: ((( Cage (C,n)) /. (i + 1)) `1 ) = (p `1 ) by A3, A12, A14, A9, A13, JORDAN1A: 81, SPPOL_1: 41;

      

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

      then

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

       A18: [i1, j1] in ( Indices ( Gauge (C,n))) and

       A19: (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (i1,j1)) and

       A20: [i2, j2] in ( Indices ( Gauge (C,n))) and

       A21: (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (i2,j2)) and

       A22: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A10, A11, JORDAN8: 3;

      

       A23: i1 <= ( len ( Gauge (C,n))) by A18, MATRIX_0: 32;

      

       A24: i2 <= ( len ( Gauge (C,n))) by A20, MATRIX_0: 32;

      

       A25: j2 <= ( width ( Gauge (C,n))) by A20, MATRIX_0: 32;

      

       A26: j1 <= ( width ( Gauge (C,n))) by A18, MATRIX_0: 32;

      

       A27: 1 <= j1 by A18, MATRIX_0: 32;

      (p `1 ) = ( W-bound ( L~ ( Cage (C,n)))) by A2, JORDAN1A: 85, PSCOMP_1: 34;

      then ((( Gauge (C,n)) * (i1,j1)) `1 ) = ((( Gauge (C,n)) * (1,j1)) `1 ) by A19, A15, A8, A27, A26, JORDAN1A: 73;

      then

       A28: 1 >= i1 by A23, A27, A26, GOBOARD5: 3;

      

       A29: 1 <= i1 by A18, MATRIX_0: 32;

      then

       A30: i1 = 1 by A28, XXREAL_0: 1;

      

       A31: 1 <= i2 by A20, MATRIX_0: 32;

      

       A32: i1 = i2

      proof

        assume i1 <> i2;

        then i1 < i2 or i2 < i1 by XXREAL_0: 1;

        hence contradiction by A19, A21, A22, A15, A16, A29, A23, A31, A24, A27, A25, GOBOARD5: 3;

      end;

      then

       A33: j1 < ( width ( Gauge (C,n))) by A10, A11, A18, A19, A20, A21, A22, A25, A28, JORDAN10: 2, NAT_1: 13;

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

      then

       A34: ((( Cage (C,n)) /. i) `2 ) <= ((( Cage (C,n)) /. (i + 1)) `2 ) by A10, A11, A18, A19, A20, A21, A22, A29, A23, A27, A25, A32, A28, JORDAN10: 2, JORDAN1A: 19;

      then (p `2 ) <= ((( Cage (C,n)) /. (i + 1)) `2 ) by A12, A13, TOPREAL1: 4;

      then

       A35: (( W-min C) `2 ) <= ((( Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A3, A10, A11, A18, A19, A20, A21, A22, A32, A30, JORDAN10: 2, TOPREAL1:def 13;

      ((( Cage (C,n)) /. i) `2 ) <= (p `2 ) by A12, A13, A34, TOPREAL1: 4;

      then

       A36: ((( Gauge (C,n)) * (1,j1)) `2 ) <= (( W-min C) `2 ) by A3, A19, A30, TOPREAL1:def 13;

      (1 + 1) <= ( len ( Gauge (C,n))) by A5, XXREAL_0: 2;

      then ((( Gauge (C,n)) * (i1,1)) `1 ) <= (( W-min C) `1 ) by A8, A30, A6, A7, SPRECT_3: 13;

      then ( W-min C) in { |[r, s]| where r,s be Real : ((( Gauge (C,n)) * (i1,1)) `1 ) <= r & r <= ((( Gauge (C,n)) * ((i1 + 1),1)) `1 ) & ((( Gauge (C,n)) * (1,j1)) `2 ) <= s & s <= ((( Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A30, A7, A36, A35, A4;

      then ( W-min C) in ( cell (( Gauge (C,n)),i1,j1)) by A27, A30, A33, A6, GOBRD11: 32;

      hence thesis by A10, A11, A17, A18, A19, A20, A21, A22, A32, A28, GOBRD13: 22, JORDAN10: 2;

    end;

    theorem :: JORDAN1D:18

    ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( W-min C) in ( right_cell (( Cage (C,n)),i))

    proof

      

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

      consider i be Nat such that

       A2: 1 <= i and

       A3: i < ( len ( Cage (C,n))) and

       A4: ( W-min C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) by Th17;

      take i;

      thus 1 <= i & i < ( len ( Cage (C,n))) by A2, A3;

      (i + 1) <= ( len ( Cage (C,n))) by A3, NAT_1: 13;

      then ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) c= ( right_cell (( Cage (C,n)),i)) by A2, A1, GOBRD13: 33;

      hence thesis by A4;

    end;

    theorem :: JORDAN1D:19

    

     Th19: ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( W-max C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n))))

    proof

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

       A1: (( west_halfline ( W-max C)) /\ ( L~ ( Cage (C,n)))) = {p} by JORDAN1A: 89, PSCOMP_1: 34;

      

       A2: p in (( west_halfline ( W-max C)) /\ ( L~ ( Cage (C,n)))) by A1, TARSKI:def 1;

      then

       A3: p in ( west_halfline ( W-max C)) by XBOOLE_0:def 4;

      

       A4: ( W-max C) = |[(( W-max C) `1 ), (( W-max C) `2 )]| by EUCLID: 53;

      

       A5: ( len ( Gauge (C,n))) >= 4 by JORDAN8: 10;

      then

       A6: 1 < ( len ( Gauge (C,n))) by XXREAL_0: 2;

      

       A7: (( W-max C) `1 ) = ( W-bound C) by EUCLID: 52

      .= ((( Gauge (C,n)) * (2,1)) `1 ) by A6, JORDAN8: 11;

      

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

      

       A9: ( W-max C) in ( W-most C) by PSCOMP_1: 34;

      p in ( L~ ( Cage (C,n))) by A2, XBOOLE_0:def 4;

      then

      consider i be Nat such that

       A10: 1 <= i and

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

       A12: p in ( LSeg (( Cage (C,n)),i)) by SPPOL_2: 13;

      take i;

      

       A13: ( LSeg (( Cage (C,n)),i)) = ( LSeg ((( Cage (C,n)) /. i),(( Cage (C,n)) /. (i + 1)))) by A10, A11, TOPREAL1:def 3;

      thus

       A14: 1 <= i & i < ( len ( Cage (C,n))) by A10, A11, NAT_1: 13;

      then

       A15: ((( Cage (C,n)) /. i) `1 ) = (p `1 ) by A3, A12, A9, A13, JORDAN1A: 81, SPPOL_1: 41;

      

       A16: ((( Cage (C,n)) /. (i + 1)) `1 ) = (p `1 ) by A3, A12, A14, A9, A13, JORDAN1A: 81, SPPOL_1: 41;

      

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

      then

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

       A18: [i1, j1] in ( Indices ( Gauge (C,n))) and

       A19: (( Cage (C,n)) /. i) = (( Gauge (C,n)) * (i1,j1)) and

       A20: [i2, j2] in ( Indices ( Gauge (C,n))) and

       A21: (( Cage (C,n)) /. (i + 1)) = (( Gauge (C,n)) * (i2,j2)) and

       A22: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A10, A11, JORDAN8: 3;

      

       A23: i1 <= ( len ( Gauge (C,n))) by A18, MATRIX_0: 32;

      

       A24: i2 <= ( len ( Gauge (C,n))) by A20, MATRIX_0: 32;

      

       A25: j2 <= ( width ( Gauge (C,n))) by A20, MATRIX_0: 32;

      

       A26: j1 <= ( width ( Gauge (C,n))) by A18, MATRIX_0: 32;

      

       A27: 1 <= j1 by A18, MATRIX_0: 32;

      (p `1 ) = ( W-bound ( L~ ( Cage (C,n)))) by A2, JORDAN1A: 85, PSCOMP_1: 34;

      then ((( Gauge (C,n)) * (i1,j1)) `1 ) = ((( Gauge (C,n)) * (1,j1)) `1 ) by A19, A15, A8, A27, A26, JORDAN1A: 73;

      then

       A28: 1 >= i1 by A23, A27, A26, GOBOARD5: 3;

      

       A29: 1 <= i1 by A18, MATRIX_0: 32;

      then

       A30: i1 = 1 by A28, XXREAL_0: 1;

      

       A31: 1 <= i2 by A20, MATRIX_0: 32;

      

       A32: i1 = i2

      proof

        assume i1 <> i2;

        then i1 < i2 or i2 < i1 by XXREAL_0: 1;

        hence contradiction by A19, A21, A22, A15, A16, A29, A23, A31, A24, A27, A25, GOBOARD5: 3;

      end;

      then

       A33: j1 < ( width ( Gauge (C,n))) by A10, A11, A18, A19, A20, A21, A22, A25, A28, JORDAN10: 2, NAT_1: 13;

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

      then

       A34: ((( Cage (C,n)) /. i) `2 ) <= ((( Cage (C,n)) /. (i + 1)) `2 ) by A10, A11, A18, A19, A20, A21, A22, A29, A23, A27, A25, A32, A28, JORDAN10: 2, JORDAN1A: 19;

      then (p `2 ) <= ((( Cage (C,n)) /. (i + 1)) `2 ) by A12, A13, TOPREAL1: 4;

      then

       A35: (( W-max C) `2 ) <= ((( Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A3, A10, A11, A18, A19, A20, A21, A22, A32, A30, JORDAN10: 2, TOPREAL1:def 13;

      ((( Cage (C,n)) /. i) `2 ) <= (p `2 ) by A12, A13, A34, TOPREAL1: 4;

      then

       A36: ((( Gauge (C,n)) * (1,j1)) `2 ) <= (( W-max C) `2 ) by A3, A19, A30, TOPREAL1:def 13;

      (1 + 1) <= ( len ( Gauge (C,n))) by A5, XXREAL_0: 2;

      then ((( Gauge (C,n)) * (i1,1)) `1 ) <= (( W-max C) `1 ) by A8, A30, A6, A7, SPRECT_3: 13;

      then ( W-max C) in { |[r, s]| where r,s be Real : ((( Gauge (C,n)) * (i1,1)) `1 ) <= r & r <= ((( Gauge (C,n)) * ((i1 + 1),1)) `1 ) & ((( Gauge (C,n)) * (1,j1)) `2 ) <= s & s <= ((( Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A30, A7, A36, A35, A4;

      then ( W-max C) in ( cell (( Gauge (C,n)),i1,j1)) by A27, A30, A33, A6, GOBRD11: 32;

      hence thesis by A10, A11, A17, A18, A19, A20, A21, A22, A32, A28, GOBRD13: 22, JORDAN10: 2;

    end;

    theorem :: JORDAN1D:20

    ex i be Nat st 1 <= i & i < ( len ( Cage (C,n))) & ( W-max C) in ( right_cell (( Cage (C,n)),i))

    proof

      

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

      consider i be Nat such that

       A2: 1 <= i and

       A3: i < ( len ( Cage (C,n))) and

       A4: ( W-max C) in ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) by Th19;

      take i;

      thus 1 <= i & i < ( len ( Cage (C,n))) by A2, A3;

      (i + 1) <= ( len ( Cage (C,n))) by A3, NAT_1: 13;

      then ( right_cell (( Cage (C,n)),i,( Gauge (C,n)))) c= ( right_cell (( Cage (C,n)),i)) by A2, A1, GOBRD13: 33;

      hence thesis by A4;

    end;

    theorem :: JORDAN1D:21

    

     Th21: ex i be Nat st 1 <= i & i <= ( len ( Gauge (C,n))) & ( N-min ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (i,( width ( Gauge (C,n)))))

    proof

      

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

      ( N-min ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 39;

      then

      consider m be Nat such that

       A2: m in ( dom ( Cage (C,n))) and

       A3: (( Cage (C,n)) . m) = ( N-min ( L~ ( Cage (C,n)))) by FINSEQ_2: 10;

      

       A4: (( Cage (C,n)) /. m) = ( N-min ( L~ ( Cage (C,n)))) by A2, A3, PARTFUN1:def 6;

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

      then

      consider i,j be Nat such that

       A5: [i, j] in ( Indices ( Gauge (C,n))) and

       A6: (( Cage (C,n)) /. m) = (( Gauge (C,n)) * (i,j)) by A2, GOBOARD1:def 9;

      take i;

      thus

       A7: 1 <= i & i <= ( len ( Gauge (C,n))) by A5, MATRIX_0: 32;

      

       A8: 1 <= j by A5, MATRIX_0: 32;

       A9:

      now

        assume j < ( width ( Gauge (C,n)));

        then (( N-min ( L~ ( Cage (C,n)))) `2 ) < ((( Gauge (C,n)) * (i,( width ( Gauge (C,n))))) `2 ) by A4, A6, A7, A8, GOBOARD5: 4;

        then ( N-bound ( L~ ( Cage (C,n)))) < ((( Gauge (C,n)) * (i,( width ( Gauge (C,n))))) `2 ) by EUCLID: 52;

        hence contradiction by A7, A1, JORDAN1A: 70;

      end;

      j <= ( width ( Gauge (C,n))) by A5, MATRIX_0: 32;

      hence thesis by A4, A6, A9, XXREAL_0: 1;

    end;

    theorem :: JORDAN1D:22

    ex i be Nat st 1 <= i & i <= ( len ( Gauge (C,n))) & ( N-max ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (i,( width ( Gauge (C,n)))))

    proof

      

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

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

      then

      consider m be Nat such that

       A2: m in ( dom ( Cage (C,n))) and

       A3: (( Cage (C,n)) . m) = ( N-max ( L~ ( Cage (C,n)))) by FINSEQ_2: 10;

      

       A4: (( Cage (C,n)) /. m) = ( N-max ( L~ ( Cage (C,n)))) by A2, A3, PARTFUN1:def 6;

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

      then

      consider i,j be Nat such that

       A5: [i, j] in ( Indices ( Gauge (C,n))) and

       A6: (( Cage (C,n)) /. m) = (( Gauge (C,n)) * (i,j)) by A2, GOBOARD1:def 9;

      take i;

      thus

       A7: 1 <= i & i <= ( len ( Gauge (C,n))) by A5, MATRIX_0: 32;

      

       A8: 1 <= j by A5, MATRIX_0: 32;

       A9:

      now

        assume j < ( width ( Gauge (C,n)));

        then (( N-max ( L~ ( Cage (C,n)))) `2 ) < ((( Gauge (C,n)) * (i,( width ( Gauge (C,n))))) `2 ) by A4, A6, A7, A8, GOBOARD5: 4;

        then ( N-bound ( L~ ( Cage (C,n)))) < ((( Gauge (C,n)) * (i,( width ( Gauge (C,n))))) `2 ) by EUCLID: 52;

        hence contradiction by A7, A1, JORDAN1A: 70;

      end;

      j <= ( width ( Gauge (C,n))) by A5, MATRIX_0: 32;

      hence thesis by A4, A6, A9, XXREAL_0: 1;

    end;

    theorem :: JORDAN1D:23

    ex i be Nat st 1 <= i & i <= ( len ( Gauge (C,n))) & (( Gauge (C,n)) * (i,( width ( Gauge (C,n))))) in ( rng ( Cage (C,n)))

    proof

      consider i be Nat such that

       A1: 1 <= i and

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

       A3: ( N-min ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (i,( width ( Gauge (C,n))))) by Th21;

      take i;

      thus thesis by A1, A2, A3, SPRECT_2: 39;

    end;

    theorem :: JORDAN1D:24

    

     Th24: ex j be Nat st 1 <= j & j <= ( width ( Gauge (C,n))) & ( E-min ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (( len ( Gauge (C,n))),j))

    proof

      

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

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

      then

      consider m be Nat such that

       A2: m in ( dom ( Cage (C,n))) and

       A3: (( Cage (C,n)) . m) = ( E-min ( L~ ( Cage (C,n)))) by FINSEQ_2: 10;

      

       A4: (( Cage (C,n)) /. m) = ( E-min ( L~ ( Cage (C,n)))) by A2, A3, PARTFUN1:def 6;

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

      then

      consider i,j be Nat such that

       A5: [i, j] in ( Indices ( Gauge (C,n))) and

       A6: (( Cage (C,n)) /. m) = (( Gauge (C,n)) * (i,j)) by A2, GOBOARD1:def 9;

      take j;

      thus

       A7: 1 <= j & j <= ( width ( Gauge (C,n))) by A5, MATRIX_0: 32;

      

       A8: 1 <= i by A5, MATRIX_0: 32;

       A9:

      now

        assume i < ( len ( Gauge (C,n)));

        then (( E-min ( L~ ( Cage (C,n)))) `1 ) < ((( Gauge (C,n)) * (( len ( Gauge (C,n))),j)) `1 ) by A4, A6, A7, A8, GOBOARD5: 3;

        then ( E-bound ( L~ ( Cage (C,n)))) < ((( Gauge (C,n)) * (( len ( Gauge (C,n))),j)) `1 ) by EUCLID: 52;

        hence contradiction by A7, A1, JORDAN1A: 71;

      end;

      i <= ( len ( Gauge (C,n))) by A5, MATRIX_0: 32;

      hence thesis by A4, A6, A9, XXREAL_0: 1;

    end;

    theorem :: JORDAN1D:25

    ex j be Nat st 1 <= j & j <= ( width ( Gauge (C,n))) & ( E-max ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (( len ( Gauge (C,n))),j))

    proof

      

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

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

      then

      consider m be Nat such that

       A2: m in ( dom ( Cage (C,n))) and

       A3: (( Cage (C,n)) . m) = ( E-max ( L~ ( Cage (C,n)))) by FINSEQ_2: 10;

      

       A4: (( Cage (C,n)) /. m) = ( E-max ( L~ ( Cage (C,n)))) by A2, A3, PARTFUN1:def 6;

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

      then

      consider i,j be Nat such that

       A5: [i, j] in ( Indices ( Gauge (C,n))) and

       A6: (( Cage (C,n)) /. m) = (( Gauge (C,n)) * (i,j)) by A2, GOBOARD1:def 9;

      take j;

      thus

       A7: 1 <= j & j <= ( width ( Gauge (C,n))) by A5, MATRIX_0: 32;

      

       A8: 1 <= i by A5, MATRIX_0: 32;

       A9:

      now

        assume i < ( len ( Gauge (C,n)));

        then (( E-max ( L~ ( Cage (C,n)))) `1 ) < ((( Gauge (C,n)) * (( len ( Gauge (C,n))),j)) `1 ) by A4, A6, A7, A8, GOBOARD5: 3;

        then ( E-bound ( L~ ( Cage (C,n)))) < ((( Gauge (C,n)) * (( len ( Gauge (C,n))),j)) `1 ) by EUCLID: 52;

        hence contradiction by A7, A1, JORDAN1A: 71;

      end;

      i <= ( len ( Gauge (C,n))) by A5, MATRIX_0: 32;

      hence thesis by A4, A6, A9, XXREAL_0: 1;

    end;

    theorem :: JORDAN1D:26

    ex j be Nat st 1 <= j & j <= ( width ( Gauge (C,n))) & (( Gauge (C,n)) * (( len ( Gauge (C,n))),j)) in ( rng ( Cage (C,n)))

    proof

      consider j be Nat such that

       A1: 1 <= j and

       A2: j <= ( width ( Gauge (C,n))) and

       A3: ( E-min ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (( len ( Gauge (C,n))),j)) by Th24;

      take j;

      thus thesis by A1, A2, A3, SPRECT_2: 45;

    end;

    theorem :: JORDAN1D:27

    

     Th27: ex i be Nat st 1 <= i & i <= ( len ( Gauge (C,n))) & ( S-min ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (i,1))

    proof

      ( S-min ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 41;

      then

      consider m be Nat such that

       A1: m in ( dom ( Cage (C,n))) and

       A2: (( Cage (C,n)) . m) = ( S-min ( L~ ( Cage (C,n)))) by FINSEQ_2: 10;

      

       A3: (( Cage (C,n)) /. m) = ( S-min ( L~ ( Cage (C,n)))) by A1, A2, PARTFUN1:def 6;

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

      then

      consider i,j be Nat such that

       A4: [i, j] in ( Indices ( Gauge (C,n))) and

       A5: (( Cage (C,n)) /. m) = (( Gauge (C,n)) * (i,j)) by A1, GOBOARD1:def 9;

      take i;

      thus

       A6: 1 <= i & i <= ( len ( Gauge (C,n))) by A4, MATRIX_0: 32;

      

       A7: j <= ( width ( Gauge (C,n))) by A4, MATRIX_0: 32;

       A8:

      now

        assume j > 1;

        then (( S-min ( L~ ( Cage (C,n)))) `2 ) > ((( Gauge (C,n)) * (i,1)) `2 ) by A3, A5, A6, A7, GOBOARD5: 4;

        then ( S-bound ( L~ ( Cage (C,n)))) > ((( Gauge (C,n)) * (i,1)) `2 ) by EUCLID: 52;

        hence contradiction by A6, JORDAN1A: 72;

      end;

      1 <= j by A4, MATRIX_0: 32;

      hence thesis by A3, A5, A8, XXREAL_0: 1;

    end;

    theorem :: JORDAN1D:28

    ex i be Nat st 1 <= i & i <= ( len ( Gauge (C,n))) & ( S-max ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (i,1))

    proof

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

      then

      consider m be Nat such that

       A1: m in ( dom ( Cage (C,n))) and

       A2: (( Cage (C,n)) . m) = ( S-max ( L~ ( Cage (C,n)))) by FINSEQ_2: 10;

      

       A3: (( Cage (C,n)) /. m) = ( S-max ( L~ ( Cage (C,n)))) by A1, A2, PARTFUN1:def 6;

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

      then

      consider i,j be Nat such that

       A4: [i, j] in ( Indices ( Gauge (C,n))) and

       A5: (( Cage (C,n)) /. m) = (( Gauge (C,n)) * (i,j)) by A1, GOBOARD1:def 9;

      take i;

      thus

       A6: 1 <= i & i <= ( len ( Gauge (C,n))) by A4, MATRIX_0: 32;

      

       A7: j <= ( width ( Gauge (C,n))) by A4, MATRIX_0: 32;

       A8:

      now

        assume j > 1;

        then (( S-max ( L~ ( Cage (C,n)))) `2 ) > ((( Gauge (C,n)) * (i,1)) `2 ) by A3, A5, A6, A7, GOBOARD5: 4;

        then ( S-bound ( L~ ( Cage (C,n)))) > ((( Gauge (C,n)) * (i,1)) `2 ) by EUCLID: 52;

        hence contradiction by A6, JORDAN1A: 72;

      end;

      1 <= j by A4, MATRIX_0: 32;

      hence thesis by A3, A5, A8, XXREAL_0: 1;

    end;

    theorem :: JORDAN1D:29

    ex i be Nat st 1 <= i & i <= ( len ( Gauge (C,n))) & (( Gauge (C,n)) * (i,1)) in ( rng ( Cage (C,n)))

    proof

      consider i be Nat such that

       A1: 1 <= i and

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

       A3: ( S-min ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (i,1)) by Th27;

      take i;

      thus thesis by A1, A2, A3, SPRECT_2: 41;

    end;

    theorem :: JORDAN1D:30

    

     Th30: ex j be Nat st 1 <= j & j <= ( width ( Gauge (C,n))) & ( W-min ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (1,j))

    proof

      

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

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

      then

      consider m be Nat such that

       A2: m in ( dom ( Cage (C,n))) and

       A3: (( Cage (C,n)) . m) = ( W-min ( L~ ( Cage (C,n)))) by FINSEQ_2: 10;

      

       A4: (( Cage (C,n)) /. m) = ( W-min ( L~ ( Cage (C,n)))) by A2, A3, PARTFUN1:def 6;

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

      then

      consider i,j be Nat such that

       A5: [i, j] in ( Indices ( Gauge (C,n))) and

       A6: (( Cage (C,n)) /. m) = (( Gauge (C,n)) * (i,j)) by A2, GOBOARD1:def 9;

      take j;

      thus

       A7: 1 <= j & j <= ( width ( Gauge (C,n))) by A5, MATRIX_0: 32;

      

       A8: i <= ( len ( Gauge (C,n))) by A5, MATRIX_0: 32;

       A9:

      now

        assume i > 1;

        then (( W-min ( L~ ( Cage (C,n)))) `1 ) > ((( Gauge (C,n)) * (1,j)) `1 ) by A4, A6, A7, A8, GOBOARD5: 3;

        then ( W-bound ( L~ ( Cage (C,n)))) > ((( Gauge (C,n)) * (1,j)) `1 ) by EUCLID: 52;

        hence contradiction by A7, A1, JORDAN1A: 73;

      end;

      1 <= i by A5, MATRIX_0: 32;

      hence thesis by A4, A6, A9, XXREAL_0: 1;

    end;

    theorem :: JORDAN1D:31

    ex j be Nat st 1 <= j & j <= ( width ( Gauge (C,n))) & ( W-max ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (1,j))

    proof

      

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

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

      then

      consider m be Nat such that

       A2: m in ( dom ( Cage (C,n))) and

       A3: (( Cage (C,n)) . m) = ( W-max ( L~ ( Cage (C,n)))) by FINSEQ_2: 10;

      

       A4: (( Cage (C,n)) /. m) = ( W-max ( L~ ( Cage (C,n)))) by A2, A3, PARTFUN1:def 6;

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

      then

      consider i,j be Nat such that

       A5: [i, j] in ( Indices ( Gauge (C,n))) and

       A6: (( Cage (C,n)) /. m) = (( Gauge (C,n)) * (i,j)) by A2, GOBOARD1:def 9;

      take j;

      thus

       A7: 1 <= j & j <= ( width ( Gauge (C,n))) by A5, MATRIX_0: 32;

      

       A8: i <= ( len ( Gauge (C,n))) by A5, MATRIX_0: 32;

       A9:

      now

        assume i > 1;

        then (( W-max ( L~ ( Cage (C,n)))) `1 ) > ((( Gauge (C,n)) * (1,j)) `1 ) by A4, A6, A7, A8, GOBOARD5: 3;

        then ( W-bound ( L~ ( Cage (C,n)))) > ((( Gauge (C,n)) * (1,j)) `1 ) by EUCLID: 52;

        hence contradiction by A7, A1, JORDAN1A: 73;

      end;

      1 <= i by A5, MATRIX_0: 32;

      hence thesis by A4, A6, A9, XXREAL_0: 1;

    end;

    theorem :: JORDAN1D:32

    ex j be Nat st 1 <= j & j <= ( width ( Gauge (C,n))) & (( Gauge (C,n)) * (1,j)) in ( rng ( Cage (C,n)))

    proof

      consider j be Nat such that

       A1: 1 <= j and

       A2: j <= ( width ( Gauge (C,n))) and

       A3: ( W-min ( L~ ( Cage (C,n)))) = (( Gauge (C,n)) * (1,j)) by Th30;

      take j;

      thus thesis by A1, A2, A3, SPRECT_2: 43;

    end;