jordan8.miz



    begin

    reserve i,i1,i2,i9,i19,j,j1,j2,j9,j19,k,l,m,n for Nat;

    reserve r,s,r9,s9 for Real;

    reserve D for set,

f for FinSequence of D,

G for Matrix of D;

    theorem :: JORDAN8:1

    ( <*> D) is_sequence_on G;

    theorem :: JORDAN8:2

    for D be non empty set, f be FinSequence of D, G be Matrix of D st f is_sequence_on G holds (f /^ m) is_sequence_on G

    proof

      let D be non empty set, f be FinSequence of D, G be Matrix of D such that

       A1: for n st n in ( dom f) holds ex i, j st [i, j] in ( Indices G) & (f /. n) = (G * (i,j)) and

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

      set g = (f /^ m);

      hereby

        let n;

        assume

         A3: n in ( dom g);

        then

        consider i, j such that

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

         A5: (f /. (n + m)) = (G * (i,j)) by A1, FINSEQ_5: 26;

        take i, j;

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

        thus (g /. n) = (G * (i,j)) by A3, A5, FINSEQ_5: 27;

      end;

      let n such that

       A6: n in ( dom g) and

       A7: (n + 1) in ( dom g);

      let i1, j1, i2, j2 such that

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

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

       A10: (g /. n) = (G * (i1,j1)) and

       A11: (g /. (n + 1)) = (G * (i2,j2));

      

       A12: (n + m) in ( dom f) by A6, FINSEQ_5: 26;

      

       A13: ((n + 1) + m) = ((n + m) + 1);

      then

       A14: ((n + m) + 1) in ( dom f) by A7, FINSEQ_5: 26;

      

       A15: (f /. (n + m)) = (g /. n) by A6, FINSEQ_5: 27;

      (f /. ((n + m) + 1)) = (g /. (n + 1)) by A7, A13, FINSEQ_5: 27;

      hence thesis by A2, A8, A9, A10, A11, A12, A14, A15;

    end;

    theorem :: JORDAN8:3

    

     Th3: 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G implies ex i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices G) & (f /. k) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & (f /. (k + 1)) = (G * (i2,j2)) & (i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1))

    proof

      assume that

       A1: 1 <= k and

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

       A3: f is_sequence_on G;

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

      then k <= ( len f) by A2, XXREAL_0: 2;

      then

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

      then

      consider i1,j1 be Nat such that

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

       A6: (f /. k) = (G * (i1,j1)) by A3;

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

      then

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

      then

      consider i2,j2 be Nat such that

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

       A9: (f /. (k + 1)) = (G * (i2,j2)) by A3;

      

       A10: ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A3, A4, A5, A6, A7, A8, A9;

      now

        per cases by A10, SEQM_3: 42;

          case that

           A11: |.(i1 - i2).| = 1 and

           A12: j1 = j2;

          (i1 - i2) = 1 or ( - (i1 - i2)) = 1 by A11, ABSVALUE:def 1;

          hence i1 = (i2 + 1) or (i1 + 1) = i2;

          thus j1 = j2 by A12;

        end;

          case that

           A13: i1 = i2 and

           A14: |.(j1 - j2).| = 1;

          (j1 - j2) = 1 or ( - (j1 - j2)) = 1 by A14, ABSVALUE:def 1;

          hence j1 = (j2 + 1) or (j1 + 1) = j2;

          thus i1 = i2 by A13;

        end;

      end;

      hence thesis by A5, A6, A8, A9;

    end;

    reserve G for Go-board,

p for Point of ( TOP-REAL 2);

    theorem :: JORDAN8:4

    for f be non empty FinSequence of ( TOP-REAL 2) st f is_sequence_on G holds f is standard special

    proof

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

       A1: f is_sequence_on G;

      thus f is_sequence_on ( GoB f)

      proof

        set F = ( GoB f);

        thus for n st n in ( dom f) holds ex i, j st [i, j] in ( Indices ( GoB f)) & (f /. n) = (( GoB f) * (i,j)) by GOBOARD2: 14;

        let n such that

         A2: n in ( dom f) and

         A3: (n + 1) in ( dom f);

        let m, k, i, j such that

         A4: [m, k] in ( Indices ( GoB f)) and

         A5: [i, j] in ( Indices ( GoB f)) and

         A6: (f /. n) = (( GoB f) * (m,k)) and

         A7: (f /. (n + 1)) = (( GoB f) * (i,j));

        

         A8: 1 <= m by A4, MATRIX_0: 32;

        

         A9: m <= ( len F) by A4, MATRIX_0: 32;

        

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

        

         A11: k <= ( width F) by A4, MATRIX_0: 32;

        

         A12: 1 <= i by A5, MATRIX_0: 32;

        

         A13: i <= ( len F) by A5, MATRIX_0: 32;

        

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

        

         A15: j <= ( width F) by A5, MATRIX_0: 32;

        then

         A16: ((F * (i,j)) `1 ) = ((F * (i,1)) `1 ) by A12, A13, A14, GOBOARD5: 2;

        

         A17: ((F * (i,k)) `1 ) = ((F * (i,1)) `1 ) by A10, A11, A12, A13, GOBOARD5: 2;

        

         A18: ((F * (i,j)) `2 ) = ((F * (1,j)) `2 ) by A12, A13, A14, A15, GOBOARD5: 1;

        

         A19: ((F * (m,j)) `2 ) = ((F * (1,j)) `2 ) by A8, A9, A14, A15, GOBOARD5: 1;

        

         A20: 1 <= n by A2, FINSEQ_3: 25;

        (n + 1) <= ( len f) by A3, FINSEQ_3: 25;

        then

        consider i1, j1, i2, j2 such that

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

         A22: (f /. n) = (G * (i1,j1)) and

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

         A24: (f /. (n + 1)) = (G * (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 A1, A20, Th3;

        

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

        

         A27: i1 <= ( len G) by A21, MATRIX_0: 32;

        

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

        

         A29: j1 <= ( width G) by A21, MATRIX_0: 32;

        

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

        

         A31: i2 <= ( len G) by A23, MATRIX_0: 32;

        

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

        

         A33: j2 <= ( width G) by A23, MATRIX_0: 32;

        

         A34: ((G * (i1,j1)) `1 ) = ((G * (i1,1)) `1 ) by A26, A27, A28, A29, GOBOARD5: 2;

        

         A35: ((G * (i2,j2)) `1 ) = ((G * (i2,1)) `1 ) by A30, A31, A32, A33, GOBOARD5: 2;

        

         A36: ((G * (i1,j1)) `2 ) = ((G * (1,j1)) `2 ) by A26, A27, A28, A29, GOBOARD5: 1;

        

         A37: ((G * (i2,j1)) `2 ) = ((G * (1,j1)) `2 ) by A28, A29, A30, A31, GOBOARD5: 1;

        

         A38: (k + 1) >= 1 by NAT_1: 12;

        

         A39: (j + 1) >= 1 by NAT_1: 12;

        

         A40: (m + 1) >= 1 by NAT_1: 12;

        

         A41: (i + 1) >= 1 by NAT_1: 12;

        

         A42: (k + 1) > k by NAT_1: 13;

        

         A43: (j + 1) > j by NAT_1: 13;

        

         A44: (m + 1) > m by NAT_1: 13;

        

         A45: (i + 1) > i by NAT_1: 13;

        per cases by A25;

          suppose

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

          now

            assume m <> i;

            then m < i or m > i by XXREAL_0: 1;

            hence contradiction by A6, A7, A8, A9, A10, A11, A12, A13, A16, A17, A22, A24, A34, A35, A46, GOBOARD5: 3;

          end;

          then

           A47: |.(m - i).| = 0 by ABSVALUE: 2;

          now

            assume j <= k;

            then

             A48: ((F * (i,j)) `2 ) <= ((F * (m,k)) `2 ) by A8, A9, A11, A14, A18, A19, SPRECT_3: 12;

            j1 < j2 by A46, NAT_1: 13;

            hence contradiction by A6, A7, A22, A24, A28, A30, A31, A33, A36, A37, A48, GOBOARD5: 4;

          end;

          then

           A49: (k + 1) <= j by NAT_1: 13;

          now

            assume

             A50: (k + 1) < j;

            then

             A51: (k + 1) < ( width F) by A15, XXREAL_0: 2;

            then

            consider l, i9 such that

             A52: l in ( dom f) and

             A53: [i9, (k + 1)] in ( Indices F) and

             A54: (f /. l) = (F * (i9,(k + 1))) by JORDAN5D: 8, NAT_1: 12;

            

             A55: 1 <= i9 by A53, MATRIX_0: 32;

            i9 <= ( len F) by A53, MATRIX_0: 32;

            then

             A56: ((F * (i9,(k + 1))) `2 ) = ((F * (1,(k + 1))) `2 ) by A38, A51, A55, GOBOARD5: 1;

            

             A57: ((F * (m,(k + 1))) `2 ) = ((F * (1,(k + 1))) `2 ) by A8, A9, A38, A51, GOBOARD5: 1;

            consider i19, j19 such that

             A58: [i19, j19] in ( Indices G) and

             A59: (f /. l) = (G * (i19,j19)) by A1, A52;

            

             A60: 1 <= i19 by A58, MATRIX_0: 32;

            

             A61: i19 <= ( len G) by A58, MATRIX_0: 32;

            

             A62: 1 <= j19 by A58, MATRIX_0: 32;

            

             A63: j19 <= ( width G) by A58, MATRIX_0: 32;

            

             A64: ((G * (i19,j1)) `2 ) = ((G * (1,j1)) `2 ) by A28, A29, A60, A61, GOBOARD5: 1;

            

             A65: ((G * (i2,j2)) `2 ) = ((G * (1,j2)) `2 ) by A30, A31, A32, A33, GOBOARD5: 1;

            

             A66: ((G * (i19,j2)) `2 ) = ((G * (1,j2)) `2 ) by A32, A33, A60, A61, GOBOARD5: 1;

             A67:

            now

              assume j1 >= j19;

              then ((G * (i19,j19)) `2 ) <= ((G * (i1,j1)) `2 ) by A29, A36, A60, A61, A62, A64, SPRECT_3: 12;

              hence contradiction by A6, A8, A9, A10, A22, A42, A51, A54, A56, A57, A59, GOBOARD5: 4;

            end;

            now

              assume j2 <= j19;

              then ((G * (i2,j2)) `2 ) <= ((G * (i19,j19)) `2 ) by A32, A60, A61, A63, A65, A66, SPRECT_3: 12;

              hence contradiction by A7, A8, A9, A15, A18, A19, A24, A38, A50, A54, A56, A57, A59, GOBOARD5: 4;

            end;

            hence contradiction by A46, A67, NAT_1: 13;

          end;

          then (k + 1) = j by A49, XXREAL_0: 1;

          then |.(j - k).| = 1 by ABSVALUE:def 1;

          hence thesis by A47, UNIFORM1: 11;

        end;

          suppose

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

          now

            assume k <> j;

            then k < j or k > j by XXREAL_0: 1;

            hence contradiction by A6, A7, A8, A9, A10, A11, A14, A15, A18, A19, A22, A24, A36, A37, A68, GOBOARD5: 4;

          end;

          then

           A69: |.(k - j).| = 0 by ABSVALUE: 2;

          now

            assume i <= m;

            then

             A70: ((F * (i,j)) `1 ) <= ((F * (m,k)) `1 ) by A9, A10, A11, A12, A16, A17, SPRECT_3: 13;

            i1 < i2 by A68, NAT_1: 13;

            hence contradiction by A6, A7, A22, A24, A26, A28, A29, A31, A68, A70, GOBOARD5: 3;

          end;

          then

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

          now

            assume

             A72: (m + 1) < i;

            then

             A73: (m + 1) < ( len F) by A13, XXREAL_0: 2;

            then

            consider l, j9 such that

             A74: l in ( dom f) and

             A75: [(m + 1), j9] in ( Indices F) and

             A76: (f /. l) = (F * ((m + 1),j9)) by JORDAN5D: 7, NAT_1: 12;

            

             A77: 1 <= j9 by A75, MATRIX_0: 32;

            j9 <= ( width F) by A75, MATRIX_0: 32;

            then

             A78: ((F * ((m + 1),j9)) `1 ) = ((F * ((m + 1),1)) `1 ) by A40, A73, A77, GOBOARD5: 2;

            

             A79: ((F * ((m + 1),k)) `1 ) = ((F * ((m + 1),1)) `1 ) by A10, A11, A40, A73, GOBOARD5: 2;

            consider i19, j19 such that

             A80: [i19, j19] in ( Indices G) and

             A81: (f /. l) = (G * (i19,j19)) by A1, A74;

            

             A82: 1 <= i19 by A80, MATRIX_0: 32;

            

             A83: i19 <= ( len G) by A80, MATRIX_0: 32;

            

             A84: 1 <= j19 by A80, MATRIX_0: 32;

            

             A85: j19 <= ( width G) by A80, MATRIX_0: 32;

            then

             A86: ((G * (i1,j19)) `1 ) = ((G * (i1,1)) `1 ) by A26, A27, A84, GOBOARD5: 2;

            

             A87: ((G * (i2,j2)) `1 ) = ((G * (i2,1)) `1 ) by A30, A31, A32, A33, GOBOARD5: 2;

            

             A88: ((G * (i2,j19)) `1 ) = ((G * (i2,1)) `1 ) by A30, A31, A84, A85, GOBOARD5: 2;

             A89:

            now

              assume i1 >= i19;

              then ((G * (i19,j19)) `1 ) <= ((G * (i1,j1)) `1 ) by A27, A34, A82, A84, A85, A86, SPRECT_3: 13;

              hence contradiction by A6, A8, A10, A11, A22, A44, A73, A76, A78, A79, A81, GOBOARD5: 3;

            end;

            now

              assume i2 <= i19;

              then ((G * (i2,j2)) `1 ) <= ((G * (i19,j19)) `1 ) by A30, A83, A84, A85, A87, A88, SPRECT_3: 13;

              hence contradiction by A7, A10, A11, A13, A16, A17, A24, A40, A72, A76, A78, A79, A81, GOBOARD5: 3;

            end;

            hence contradiction by A68, A89, NAT_1: 13;

          end;

          then (m + 1) = i by A71, XXREAL_0: 1;

          then |.(i - m).| = 1 by ABSVALUE:def 1;

          hence thesis by A69, UNIFORM1: 11;

        end;

          suppose

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

          now

            assume k <> j;

            then k < j or k > j by XXREAL_0: 1;

            hence contradiction by A6, A7, A8, A9, A10, A11, A14, A15, A18, A19, A22, A24, A36, A37, A90, GOBOARD5: 4;

          end;

          then

           A91: |.(k - j).| = 0 by ABSVALUE: 2;

          now

            assume m <= i;

            then

             A92: ((F * (i,j)) `1 ) >= ((F * (m,k)) `1 ) by A8, A10, A11, A13, A16, A17, SPRECT_3: 13;

            i1 > i2 by A90, NAT_1: 13;

            hence contradiction by A6, A7, A22, A24, A27, A28, A29, A30, A90, A92, GOBOARD5: 3;

          end;

          then

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

          now

            assume

             A94: (i + 1) < m;

            then

             A95: (i + 1) < ( len F) by A9, XXREAL_0: 2;

            then

            consider l, j9 such that

             A96: l in ( dom f) and

             A97: [(i + 1), j9] in ( Indices F) and

             A98: (f /. l) = (F * ((i + 1),j9)) by JORDAN5D: 7, NAT_1: 12;

            

             A99: 1 <= j9 by A97, MATRIX_0: 32;

            j9 <= ( width F) by A97, MATRIX_0: 32;

            then

             A100: ((F * ((i + 1),j9)) `1 ) = ((F * ((i + 1),1)) `1 ) by A41, A95, A99, GOBOARD5: 2;

            

             A101: ((F * ((i + 1),k)) `1 ) = ((F * ((i + 1),1)) `1 ) by A10, A11, A41, A95, GOBOARD5: 2;

            

             A102: ((F * ((i + 1),j)) `1 ) = ((F * ((i + 1),1)) `1 ) by A14, A15, A41, A95, GOBOARD5: 2;

            consider i19, j19 such that

             A103: [i19, j19] in ( Indices G) and

             A104: (f /. l) = (G * (i19,j19)) by A1, A96;

            

             A105: 1 <= i19 by A103, MATRIX_0: 32;

            

             A106: i19 <= ( len G) by A103, MATRIX_0: 32;

            

             A107: 1 <= j19 by A103, MATRIX_0: 32;

            

             A108: j19 <= ( width G) by A103, MATRIX_0: 32;

            then

             A109: ((G * (i1,j19)) `1 ) = ((G * (i1,1)) `1 ) by A26, A27, A107, GOBOARD5: 2;

            

             A110: ((G * (i2,j2)) `1 ) = ((G * (i2,1)) `1 ) by A30, A31, A32, A33, GOBOARD5: 2;

            

             A111: ((G * (i2,j19)) `1 ) = ((G * (i2,1)) `1 ) by A30, A31, A107, A108, GOBOARD5: 2;

             A112:

            now

              assume i2 >= i19;

              then ((G * (i19,j19)) `1 ) <= ((G * (i2,j2)) `1 ) by A31, A105, A107, A108, A110, A111, SPRECT_3: 13;

              hence contradiction by A7, A12, A14, A15, A24, A45, A95, A98, A100, A102, A104, GOBOARD5: 3;

            end;

            now

              assume i1 <= i19;

              then ((G * (i1,j1)) `1 ) <= ((G * (i19,j19)) `1 ) by A26, A34, A106, A107, A108, A109, SPRECT_3: 13;

              hence contradiction by A6, A9, A10, A11, A22, A41, A94, A98, A100, A101, A104, GOBOARD5: 3;

            end;

            hence contradiction by A90, A112, NAT_1: 13;

          end;

          then (i + 1) = m by A93, XXREAL_0: 1;

          hence thesis by A91, ABSVALUE:def 1;

        end;

          suppose

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

          now

            assume m <> i;

            then m < i or m > i by XXREAL_0: 1;

            hence contradiction by A6, A7, A8, A9, A10, A11, A12, A13, A16, A17, A22, A24, A34, A35, A113, GOBOARD5: 3;

          end;

          then

           A114: |.(m - i).| = 0 by ABSVALUE: 2;

          now

            assume j >= k;

            then

             A115: ((F * (i,j)) `2 ) >= ((F * (m,k)) `2 ) by A8, A9, A10, A15, A18, A19, SPRECT_3: 12;

            j1 > j2 by A113, NAT_1: 13;

            hence contradiction by A6, A7, A22, A24, A29, A30, A31, A32, A36, A37, A115, GOBOARD5: 4;

          end;

          then

           A116: (j + 1) <= k by NAT_1: 13;

          now

            assume

             A117: (j + 1) < k;

            then

             A118: (j + 1) < ( width F) by A11, XXREAL_0: 2;

            then

            consider l, i9 such that

             A119: l in ( dom f) and

             A120: [i9, (j + 1)] in ( Indices F) and

             A121: (f /. l) = (F * (i9,(j + 1))) by JORDAN5D: 8, NAT_1: 12;

            

             A122: 1 <= i9 by A120, MATRIX_0: 32;

            i9 <= ( len F) by A120, MATRIX_0: 32;

            then

             A123: ((F * (i9,(j + 1))) `2 ) = ((F * (1,(j + 1))) `2 ) by A39, A118, A122, GOBOARD5: 1;

            

             A124: ((F * (i,(j + 1))) `2 ) = ((F * (1,(j + 1))) `2 ) by A12, A13, A39, A118, GOBOARD5: 1;

            

             A125: ((F * (m,(j + 1))) `2 ) = ((F * (1,(j + 1))) `2 ) by A8, A9, A39, A118, GOBOARD5: 1;

            consider i19, j19 such that

             A126: [i19, j19] in ( Indices G) and

             A127: (f /. l) = (G * (i19,j19)) by A1, A119;

            

             A128: 1 <= i19 by A126, MATRIX_0: 32;

            

             A129: i19 <= ( len G) by A126, MATRIX_0: 32;

            

             A130: 1 <= j19 by A126, MATRIX_0: 32;

            

             A131: j19 <= ( width G) by A126, MATRIX_0: 32;

            

             A132: ((G * (i19,j1)) `2 ) = ((G * (1,j1)) `2 ) by A28, A29, A128, A129, GOBOARD5: 1;

            

             A133: ((G * (i2,j2)) `2 ) = ((G * (1,j2)) `2 ) by A30, A31, A32, A33, GOBOARD5: 1;

            

             A134: ((G * (i19,j2)) `2 ) = ((G * (1,j2)) `2 ) by A32, A33, A128, A129, GOBOARD5: 1;

             A135:

            now

              assume j2 >= j19;

              then ((G * (i19,j19)) `2 ) <= ((G * (i2,j2)) `2 ) by A33, A128, A129, A130, A133, A134, SPRECT_3: 12;

              hence contradiction by A7, A12, A13, A14, A24, A43, A118, A121, A123, A124, A127, GOBOARD5: 4;

            end;

            now

              assume j1 <= j19;

              then ((G * (i1,j1)) `2 ) <= ((G * (i19,j19)) `2 ) by A28, A36, A128, A129, A131, A132, SPRECT_3: 12;

              hence contradiction by A6, A8, A9, A11, A22, A39, A117, A121, A123, A125, A127, GOBOARD5: 4;

            end;

            hence contradiction by A113, A135, NAT_1: 13;

          end;

          then (j + 1) = k by A116, XXREAL_0: 1;

          hence thesis by A114, ABSVALUE:def 1;

        end;

      end;

      thus f is special

      proof

        let i be Nat;

        assume that

         A136: 1 <= i and

         A137: (i + 1) <= ( len f);

        consider i1, j1, i2, j2 such that

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

         A139: (f /. i) = (G * (i1,j1)) and

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

         A141: (f /. (i + 1)) = (G * (i2,j2)) and

         A142: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A1, A136, A137, Th3;

        

         A143: 1 <= i1 by A138, MATRIX_0: 32;

        

         A144: i1 <= ( len G) by A138, MATRIX_0: 32;

        

         A145: 1 <= j1 by A138, MATRIX_0: 32;

        

         A146: j1 <= ( width G) by A138, MATRIX_0: 32;

        

         A147: 1 <= i2 by A140, MATRIX_0: 32;

        

         A148: i2 <= ( len G) by A140, MATRIX_0: 32;

        

         A149: 1 <= j2 by A140, MATRIX_0: 32;

        

         A150: j2 <= ( width G) by A140, MATRIX_0: 32;

        

         A151: ((G * (i1,j1)) `2 ) = ((G * (1,j1)) `2 ) by A143, A144, A145, A146, GOBOARD5: 1;

        ((G * (i1,j1)) `1 ) = ((G * (i1,1)) `1 ) by A143, A144, A145, A146, GOBOARD5: 2;

        hence thesis by A139, A141, A142, A147, A148, A149, A150, A151, GOBOARD5: 1, GOBOARD5: 2;

      end;

    end;

    theorem :: JORDAN8:5

    for f be non empty FinSequence of ( TOP-REAL 2) st ( len f) >= 2 & f is_sequence_on G holds f is non constant

    proof

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

       A1: ( len f) >= 2 and

       A2: f is_sequence_on G;

      assume

       A3: for n, m st n in ( dom f) & m in ( dom f) holds (f . n) = (f . m);

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

      then

       A4: 1 in ( dom f) by FINSEQ_3: 25;

      then

      consider i1, j1 such that

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

       A6: (f /. 1) = (G * (i1,j1)) by A2;

      

       A7: (1 + 1) in ( dom f) by A1, FINSEQ_3: 25;

      then

      consider i2, j2 such that

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

       A9: (f /. 2) = (G * (i2,j2)) by A2;

      

       A10: (f /. 1) = (f . 1) by A4, PARTFUN1:def 6

      .= (f . 2) by A3, A4, A7

      .= (f /. 2) by A7, PARTFUN1:def 6;

      then

       A11: i1 = i2 by A5, A6, A8, A9, GOBOARD1: 5;

      

       A12: j1 = j2 by A5, A6, A8, A9, A10, GOBOARD1: 5;

      

       A13: |.(i1 - i2).| = 0 by A11, ABSVALUE: 2;

      ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A2, A4, A5, A6, A7, A8, A9;

      hence contradiction by A12, A13;

    end;

    theorem :: JORDAN8:6

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

    proof

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

       A1: f is_sequence_on G and

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

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

      

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

       A5:

      now

        let n;

        assume that

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

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

        

         A8: 1 <= n by A6, FINSEQ_3: 25;

        

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

        

         A10: (1 + 1) <= (n + 1) by A8, XREAL_1: 6;

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

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

      end;

      now

        let m, k, i, j such that

         A11: [m, k] in ( Indices G) and

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

         A13: (f /. ( len f)) = (G * (m,k)) and

         A14: ( <*p*> /. 1) = (G * (i,j)) and ( len f) in ( dom f) and 1 in ( dom <*p*>);

        ( <*p*> /. 1) = p by FINSEQ_4: 16;

        then ( |.(i - m).| + |.(j - k).|) = 1 by A3, A11, A12, A13, A14;

        

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

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

      end;

      then

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

      now

        let n such that

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

        per cases by A16, FINSEQ_1: 25;

          suppose

           A17: n in ( dom f);

          then

          consider i, j such that

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

           A19: (f /. n) = (G * (i,j)) by A1;

          take i, j;

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

          thus ((f ^ <*p*>) /. n) = (G * (i,j)) by A17, A19, FINSEQ_4: 68;

        end;

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

          then

          consider l be Nat such that

           A20: l in ( dom <*p*>) and

           A21: n = (( len f) + l);

          consider i, j such that

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

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

          take i, j;

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

          

           A24: l <= ( len <*p*>) by A20, FINSEQ_3: 25;

          

           A25: 1 <= l by A20, FINSEQ_3: 25;

          l <= 1 by A24, FINSEQ_1: 39;

          then l = 1 by A25, XXREAL_0: 1;

          then ( <*p*> /. l) = p by FINSEQ_4: 16;

          hence ((f ^ <*p*>) /. n) = (G * (i,j)) by A20, A21, A23, FINSEQ_4: 69;

        end;

      end;

      hence thesis by A15;

    end;

    theorem :: JORDAN8:7

    (i + k) < ( len G) & 1 <= j & j < ( width G) & ( cell (G,i,j)) meets ( cell (G,(i + k),j)) implies k <= 1

    proof

      assume that

       A1: (i + k) < ( len G) and

       A2: 1 <= j and

       A3: j < ( width G) and

       A4: ( cell (G,i,j)) meets ( cell (G,(i + k),j)) and

       A5: k > 1;

      (( cell (G,i,j)) /\ ( cell (G,(i + k),j))) <> {} by A4;

      then

      consider p such that

       A6: p in (( cell (G,i,j)) /\ ( cell (G,(i + k),j))) by SUBSET_1: 4;

      

       A7: p in ( cell (G,i,j)) by A6, XBOOLE_0:def 4;

      

       A8: p in ( cell (G,(i + k),j)) by A6, XBOOLE_0:def 4;

      (i + k) >= 1 by A5, NAT_1: 12;

      then ( cell (G,(i + k),j)) = { |[r9, s9]| : ((G * ((i + k),1)) `1 ) <= r9 & r9 <= ((G * (((i + k) + 1),1)) `1 ) & ((G * (1,j)) `2 ) <= s9 & s9 <= ((G * (1,(j + 1))) `2 ) } by A1, A2, A3, GOBRD11: 32;

      then

      consider r9, s9 such that

       A9: p = |[r9, s9]| and

       A10: ((G * ((i + k),1)) `1 ) <= r9 and r9 <= ((G * (((i + k) + 1),1)) `1 ) and ((G * (1,j)) `2 ) <= s9 and s9 <= ((G * (1,(j + 1))) `2 ) by A8;

      

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

      

       A12: i = 0 or i >= (1 + 0 ) by NAT_1: 9;

      per cases by A12;

        suppose

         A13: i = 0 ;

        then ( cell (G,i,j)) = { |[r, s]| : r <= ((G * (1,1)) `1 ) & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } by A2, A3, GOBRD11: 26;

        then

        consider r, s such that

         A14: p = |[r, s]| and

         A15: r <= ((G * (1,1)) `1 ) and ((G * (1,j)) `2 ) <= s and s <= ((G * (1,(j + 1))) `2 ) by A7;

        

         A16: k <= ( len G) by A1, NAT_1: 12;

        

         A17: (p `1 ) = r by A14, EUCLID: 52;

        (p `1 ) = r9 by A9, EUCLID: 52;

        then ((G * (k,1)) `1 ) <= ((G * (1,1)) `1 ) by A10, A13, A15, A17, XXREAL_0: 2;

        hence contradiction by A5, A11, A16, GOBOARD5: 3;

      end;

        suppose

         A18: i >= 1;

        i < ( len G) by A1, NAT_1: 12;

        then ( cell (G,i,j)) = { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } by A2, A3, A18, GOBRD11: 32;

        then

        consider r, s such that

         A19: p = |[r, s]| and ((G * (i,1)) `1 ) <= r and

         A20: r <= ((G * ((i + 1),1)) `1 ) and ((G * (1,j)) `2 ) <= s and s <= ((G * (1,(j + 1))) `2 ) by A7;

        

         A21: 1 <= (i + 1) by NAT_1: 12;

        

         A22: (i + 1) < (k + i) by A5, XREAL_1: 6;

        

         A23: (p `1 ) = r by A19, EUCLID: 52;

        (p `1 ) = r9 by A9, EUCLID: 52;

        then ((G * ((i + k),1)) `1 ) <= ((G * ((i + 1),1)) `1 ) by A10, A20, A23, XXREAL_0: 2;

        hence contradiction by A1, A11, A21, A22, GOBOARD5: 3;

      end;

    end;

    theorem :: JORDAN8:8

    

     Th8: for C be non empty compact Subset of ( TOP-REAL 2) holds C is vertical iff ( E-bound C) <= ( W-bound C)

    proof

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

      

       A1: ( E-bound C) >= ( W-bound C) by SPRECT_1: 21;

      C is vertical iff ( W-bound C) = ( E-bound C) by SPRECT_1: 15;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: JORDAN8:9

    

     Th9: for C be non empty compact Subset of ( TOP-REAL 2) holds C is horizontal iff ( N-bound C) <= ( S-bound C)

    proof

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

      

       A1: ( N-bound C) >= ( S-bound C) by SPRECT_1: 22;

      C is horizontal iff ( N-bound C) = ( S-bound C) by SPRECT_1: 16;

      hence thesis by A1, XXREAL_0: 1;

    end;

    definition

      let C be Subset of ( TOP-REAL 2), n be natural Number;

      deffunc f( natural Number, natural Number) = |[(( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ n)) * ($1 - 2))), (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ n)) * ($2 - 2)))]|;

      :: JORDAN8:def1

      func Gauge (C,n) -> Matrix of ( TOP-REAL 2) means

      : Def1: ( len it ) = ((2 |^ n) + 3) & ( len it ) = ( width it ) & for i,j be Nat st [i, j] in ( Indices it ) holds (it * (i,j)) = |[(( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ n)) * (i - 2))), (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ n)) * (j - 2)))]|;

      existence

      proof

        consider M be Matrix of ((2 |^ n) + 3), ((2 |^ n) + 3), the carrier of ( TOP-REAL 2) such that

         A1: for i,j be Nat st [i, j] in ( Indices M) holds (M * (i,j)) = f(i,j) from MATRIX_0:sch 1;

        take M;

        thus ( len M) = ((2 |^ n) + 3) by MATRIX_0:def 2;

        hence ( len M) = ( width M) by MATRIX_0: 23;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of ( TOP-REAL 2) such that

         A2: ( len M1) = ((2 |^ n) + 3) and

         A3: ( len M1) = ( width M1) and

         A4: for i,j be Nat st [i, j] in ( Indices M1) holds (M1 * (i,j)) = f(i,j) and

         A5: ( len M2) = ((2 |^ n) + 3) and

         A6: ( len M2) = ( width M2) and

         A7: for i,j be Nat st [i, j] in ( Indices M2) holds (M2 * (i,j)) = f(i,j);

        now

          let i,j be Nat;

          assume

           A8: [i, j] in ( Indices M1);

          

           A9: M1 is Matrix of ((2 |^ n) + 3), ((2 |^ n) + 3), the carrier of ( TOP-REAL 2) by A2, A3, MATRIX_0: 20;

          M2 is Matrix of ((2 |^ n) + 3), ((2 |^ n) + 3), the carrier of ( TOP-REAL 2) by A5, A6, MATRIX_0: 20;

          then

           A10: [i, j] in ( Indices M2) by A8, A9, MATRIX_0: 26;

          

          thus (M1 * (i,j)) = f(i,j) by A4, A8

          .= (M2 * (i,j)) by A7, A10;

        end;

        hence thesis by A2, A3, A5, A6, MATRIX_0: 21;

      end;

    end

    registration

      let C be non empty Subset of ( TOP-REAL 2), n be Nat;

      cluster ( Gauge (C,n)) -> non empty-yielding X_equal-in-line Y_equal-in-column;

      coherence

      proof

        set M = ( Gauge (C,n));

        

         A1: ( len M) = ((2 |^ n) + 3) by Def1;

        ( len M) = ( width M) by Def1;

        hence M is non empty-yielding by A1, MATRIX_0:def 10;

        

         A2: ( Indices M) = [:( dom M), ( Seg ( width M)):] by MATRIX_0:def 4;

        thus M is X_equal-in-line

        proof

          let i;

          assume

           A3: i in ( dom M);

          set l = ( Line (M,i)), f = ( X_axis l);

          let j1, j2 such that

           A4: j1 in ( dom f) and

           A5: j2 in ( dom f);

          ( len l) = ( width M) by MATRIX_0:def 7;

          then

           A6: ( dom l) = ( Seg ( width M)) by FINSEQ_1:def 3;

          

           A7: ( dom f) = ( dom l) by SPRECT_2: 15;

          

          then

           A8: (l /. j1) = (l . j1) by A4, PARTFUN1:def 6

          .= (M * (i,j1)) by A4, A6, A7, MATRIX_0:def 7;

          

           A9: [i, j1] in ( Indices M) by A2, A3, A4, A6, A7, ZFMISC_1: 87;

          

           A10: (l /. j2) = (l . j2) by A5, A7, PARTFUN1:def 6

          .= (M * (i,j2)) by A5, A6, A7, MATRIX_0:def 7;

          

           A11: [i, j2] in ( Indices M) by A2, A3, A5, A6, A7, ZFMISC_1: 87;

          set x = (( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ n)) * (i - 2)));

          set d = ((( N-bound C) - ( S-bound C)) / (2 |^ n));

          

          thus (f . j1) = ((l /. j1) `1 ) by A4, GOBOARD1:def 1

          .= ( |[x, (( S-bound C) + (d * (j1 - 2)))]| `1 ) by A8, A9, Def1

          .= x by EUCLID: 52

          .= ( |[x, (( S-bound C) + (d * (j2 - 2)))]| `1 ) by EUCLID: 52

          .= ((l /. j2) `1 ) by A10, A11, Def1

          .= (f . j2) by A5, GOBOARD1:def 1;

        end;

        thus M is Y_equal-in-column

        proof

          let j;

          assume

           A12: j in ( Seg ( width M));

          set c = ( Col (M,j)), f = ( Y_axis c);

          let i1, i2 such that

           A13: i1 in ( dom f) and

           A14: i2 in ( dom f);

          ( len c) = ( len M) by MATRIX_0:def 8;

          then

           A15: ( dom c) = ( dom M) by FINSEQ_3: 29;

          

           A16: ( dom f) = ( dom c) by SPRECT_2: 16;

          

          then

           A17: (c /. i1) = (c . i1) by A13, PARTFUN1:def 6

          .= (M * (i1,j)) by A13, A15, A16, MATRIX_0:def 8;

          

           A18: [i1, j] in ( Indices M) by A2, A12, A13, A15, A16, ZFMISC_1: 87;

          

           A19: (c /. i2) = (c . i2) by A14, A16, PARTFUN1:def 6

          .= (M * (i2,j)) by A14, A15, A16, MATRIX_0:def 8;

          

           A20: [i2, j] in ( Indices M) by A2, A12, A14, A15, A16, ZFMISC_1: 87;

          set y = (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ n)) * (j - 2)));

          set d = ((( E-bound C) - ( W-bound C)) / (2 |^ n));

          

          thus (f . i1) = ((c /. i1) `2 ) by A13, GOBOARD1:def 2

          .= ( |[(( W-bound C) + (d * (i1 - 2))), y]| `2 ) by A17, A18, Def1

          .= y by EUCLID: 52

          .= ( |[(( W-bound C) + (d * (i2 - 2))), y]| `2 ) by EUCLID: 52

          .= ((c /. i2) `2 ) by A19, A20, Def1

          .= (f . i2) by A14, GOBOARD1:def 2;

        end;

      end;

    end

    registration

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

      cluster ( Gauge (C,n)) -> Y_increasing-in-line X_increasing-in-column;

      coherence

      proof

        set M = ( Gauge (C,n));

        

         A1: ( Indices M) = [:( dom M), ( Seg ( width M)):] by MATRIX_0:def 4;

        thus M is Y_increasing-in-line

        proof

          let i;

          assume

           A2: i in ( dom M);

          set l = ( Line (M,i)), f = ( Y_axis l);

          let j1,j2 be Nat such that

           A3: j1 in ( dom f) and

           A4: j2 in ( dom f) and

           A5: j1 < j2;

          ( len l) = ( width M) by MATRIX_0:def 7;

          then

           A6: ( dom l) = ( Seg ( width M)) by FINSEQ_1:def 3;

          

           A7: ( dom f) = ( dom l) by SPRECT_2: 16;

          

          then

           A8: (l /. j1) = (l . j1) by A3, PARTFUN1:def 6

          .= (M * (i,j1)) by A3, A6, A7, MATRIX_0:def 7;

          

           A9: [i, j1] in ( Indices M) by A1, A2, A3, A6, A7, ZFMISC_1: 87;

          

           A10: (l /. j2) = (l . j2) by A4, A7, PARTFUN1:def 6

          .= (M * (i,j2)) by A4, A6, A7, MATRIX_0:def 7;

          

           A11: [i, j2] in ( Indices M) by A1, A2, A4, A6, A7, ZFMISC_1: 87;

          set x = (( W-bound C) + (((( E-bound C) - ( W-bound C)) / (2 |^ n)) * (i - 2)));

          set d = ((( N-bound C) - ( S-bound C)) / (2 |^ n));

          

           A12: (f . j1) = ((l /. j1) `2 ) by A3, GOBOARD1:def 2

          .= ( |[x, (( S-bound C) + (d * (j1 - 2)))]| `2 ) by A8, A9, Def1

          .= (( S-bound C) + (d * (j1 - 2))) by EUCLID: 52;

          

           A13: (f . j2) = ((l /. j2) `2 ) by A4, GOBOARD1:def 2

          .= ( |[x, (( S-bound C) + (d * (j2 - 2)))]| `2 ) by A10, A11, Def1

          .= (( S-bound C) + (d * (j2 - 2))) by EUCLID: 52;

          ( N-bound C) > ( S-bound C) by Th9;

          then

           A14: (( N-bound C) - ( S-bound C)) > 0 by XREAL_1: 50;

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

          then

           A15: d > 0 by A14, XREAL_1: 139;

          (j1 - 2) < (j2 - 2) by A5, XREAL_1: 9;

          then (d * (j1 - 2)) < (d * (j2 - 2)) by A15, XREAL_1: 68;

          hence (f . j1) < (f . j2) by A12, A13, XREAL_1: 8;

        end;

        let j;

        assume

         A16: j in ( Seg ( width M));

        set c = ( Col (M,j)), f = ( X_axis c);

        let i1, i2 such that

         A17: i1 in ( dom f) and

         A18: i2 in ( dom f) and

         A19: i1 < i2;

        ( len c) = ( len M) by MATRIX_0:def 8;

        then

         A20: ( dom c) = ( dom M) by FINSEQ_3: 29;

        

         A21: ( dom f) = ( dom c) by SPRECT_2: 15;

        

        then

         A22: (c /. i1) = (c . i1) by A17, PARTFUN1:def 6

        .= (M * (i1,j)) by A17, A20, A21, MATRIX_0:def 8;

        

         A23: [i1, j] in ( Indices M) by A1, A16, A17, A20, A21, ZFMISC_1: 87;

        

         A24: (c /. i2) = (c . i2) by A18, A21, PARTFUN1:def 6

        .= (M * (i2,j)) by A18, A20, A21, MATRIX_0:def 8;

        

         A25: [i2, j] in ( Indices M) by A1, A16, A18, A20, A21, ZFMISC_1: 87;

        set y = (( S-bound C) + (((( N-bound C) - ( S-bound C)) / (2 |^ n)) * (j - 2)));

        set d = ((( E-bound C) - ( W-bound C)) / (2 |^ n));

        

         A26: (f . i1) = ((c /. i1) `1 ) by A17, GOBOARD1:def 1

        .= ( |[(( W-bound C) + (d * (i1 - 2))), y]| `1 ) by A22, A23, Def1

        .= (( W-bound C) + (d * (i1 - 2))) by EUCLID: 52;

        

         A27: (f . i2) = ((c /. i2) `1 ) by A18, GOBOARD1:def 1

        .= ( |[(( W-bound C) + (d * (i2 - 2))), y]| `1 ) by A24, A25, Def1

        .= (( W-bound C) + (d * (i2 - 2))) by EUCLID: 52;

        ( E-bound C) > ( W-bound C) by Th8;

        then

         A28: (( E-bound C) - ( W-bound C)) > 0 by XREAL_1: 50;

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

        then

         A29: d > 0 by A28, XREAL_1: 139;

        (i1 - 2) < (i2 - 2) by A19, XREAL_1: 9;

        then (d * (i1 - 2)) < (d * (i2 - 2)) by A29, XREAL_1: 68;

        hence (f . i1) < (f . i2) by A26, A27, XREAL_1: 8;

      end;

    end

    reserve T for non empty Subset of ( TOP-REAL 2);

    theorem :: JORDAN8:10

    

     Th10: for n be Nat holds ( len ( Gauge (T,n))) >= 4

    proof

      let n be Nat;

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

      

       A1: ( len G) = ((2 |^ n) + 3) by Def1;

      (2 |^ n) >= (n + 1) by NEWTON: 85;

      then

       A2: ( len G) >= ((n + 1) + 3) by A1, XREAL_1: 6;

      (n + 4) >= 4 by NAT_1: 12;

      hence thesis by A2, XXREAL_0: 2;

    end;

    theorem :: JORDAN8:11

    1 <= j & j <= ( len ( Gauge (T,n))) implies ((( Gauge (T,n)) * (2,j)) `1 ) = ( W-bound T)

    proof

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

      set W = ( W-bound T), S = ( S-bound T), E = ( E-bound T), N = ( N-bound T);

      assume that

       A1: 1 <= j and

       A2: j <= ( len ( Gauge (T,n)));

      

       A3: ( len G) = ( width G) by Def1;

      ( len G) >= 4 by Th10;

      then 2 <= ( len G) by XXREAL_0: 2;

      then [2, j] in ( Indices G) by A1, A2, A3, MATRIX_0: 30;

      then (G * (2,j)) = |[(W + (((E - W) / (2 |^ n)) * (2 - 2))), (S + (((N - S) / (2 |^ n)) * (j - 2)))]| by Def1;

      hence thesis by EUCLID: 52;

    end;

    theorem :: JORDAN8:12

    1 <= j & j <= ( len ( Gauge (T,n))) implies ((( Gauge (T,n)) * ((( len ( Gauge (T,n))) -' 1),j)) `1 ) = ( E-bound T)

    proof

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

      set W = ( W-bound T), S = ( S-bound T), E = ( E-bound T), N = ( N-bound T);

      assume that

       A1: 1 <= j and

       A2: j <= ( len ( Gauge (T,n)));

      

       A3: ( len G) = ((2 |^ n) + 3) by Def1;

      

       A4: ( len G) = ( width G) by Def1;

      

       A5: ( len G) >= 4 by Th10;

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

      then

       A6: 1 <= (( len G) -' 1) by NAT_D: 49;

      

       A7: ((( len G) -' 1) - 2) = ((( len G) - 1) - 2) by A5, XREAL_1: 233, XXREAL_0: 2

      .= (2 |^ n) by A3;

      

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

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

      then [(( len G) -' 1), j] in ( Indices G) by A1, A2, A4, A6, MATRIX_0: 30;

      then (G * ((( len G) -' 1),j)) = |[(W + (((E - W) / (2 |^ n)) * ((( len G) -' 1) - 2))), (S + (((N - S) / (2 |^ n)) * (j - 2)))]| by Def1;

      

      hence ((G * ((( len G) -' 1),j)) `1 ) = (W + (((E - W) / (2 |^ n)) * (2 |^ n))) by A7, EUCLID: 52

      .= (W + (E - W)) by A8, XCMPLX_1: 87

      .= ( E-bound T);

    end;

    theorem :: JORDAN8:13

    1 <= i & i <= ( len ( Gauge (T,n))) implies ((( Gauge (T,n)) * (i,2)) `2 ) = ( S-bound T)

    proof

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

      set W = ( W-bound T), S = ( S-bound T), E = ( E-bound T), N = ( N-bound T);

      assume that

       A1: 1 <= i and

       A2: i <= ( len ( Gauge (T,n)));

      

       A3: ( len G) = ( width G) by Def1;

      ( len G) >= 4 by Th10;

      then 2 <= ( len G) by XXREAL_0: 2;

      then [i, 2] in ( Indices G) by A1, A2, A3, MATRIX_0: 30;

      then (G * (i,2)) = |[(W + (((E - W) / (2 |^ n)) * (i - 2))), (S + (((N - S) / (2 |^ n)) * (2 - 2)))]| by Def1;

      hence thesis by EUCLID: 52;

    end;

    theorem :: JORDAN8:14

    1 <= i & i <= ( len ( Gauge (T,n))) implies ((( Gauge (T,n)) * (i,(( len ( Gauge (T,n))) -' 1))) `2 ) = ( N-bound T)

    proof

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

      set W = ( W-bound T), S = ( S-bound T), E = ( E-bound T), N = ( N-bound T);

      assume that

       A1: 1 <= i and

       A2: i <= ( len ( Gauge (T,n)));

      

       A3: ( len G) = ((2 |^ n) + 3) by Def1;

      

       A4: ( len G) = ( width G) by Def1;

      

       A5: ( len G) >= 4 by Th10;

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

      then

       A6: 1 <= (( len G) -' 1) by NAT_D: 49;

      

       A7: ((( len G) -' 1) - 2) = ((( len G) - 1) - 2) by A5, XREAL_1: 233, XXREAL_0: 2

      .= (2 |^ n) by A3;

      

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

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

      then [i, (( len G) -' 1)] in ( Indices G) by A1, A2, A4, A6, MATRIX_0: 30;

      then (G * (i,(( len G) -' 1))) = |[(W + (((E - W) / (2 |^ n)) * (i - 2))), (S + (((N - S) / (2 |^ n)) * ((( len G) -' 1) - 2)))]| by Def1;

      

      hence ((G * (i,(( len G) -' 1))) `2 ) = (S + (((N - S) / (2 |^ n)) * (2 |^ n))) by A7, EUCLID: 52

      .= (S + (N - S)) by A8, XCMPLX_1: 87

      .= ( N-bound T);

    end;

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

    reserve i,j,n for Nat;

    theorem :: JORDAN8:15

    i <= ( len ( Gauge (C,n))) implies ( cell (( Gauge (C,n)),i,( len ( Gauge (C,n))))) misses C

    proof

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

      assume

       A1: i <= ( len G);

      

       A2: ( len G) = ((2 |^ n) + (1 + 2)) by Def1;

      

       A3: ( len G) = ( width G) by Def1;

      assume (( cell (G,i,( len G))) /\ C) <> {} ;

      then

      consider p such that

       A4: p in (( cell (G,i,( len G))) /\ C) by SUBSET_1: 4;

      

       A5: p in ( cell (G,i,( len G))) by A4, XBOOLE_0:def 4;

      

       A6: p in C by A4, XBOOLE_0:def 4;

      4 <= ( len G) by Th10;

      then

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

      set W = ( W-bound C), S = ( S-bound C), E = ( E-bound C), N = ( N-bound C);

      set NS = ((N - S) / (2 |^ n));

       [1, ( width G)] in ( Indices G) by A3, A7, MATRIX_0: 30;

      then

       A8: (G * (1,( width G))) = |[(W + (((E - W) / (2 |^ n)) * (1 - 2))), (S + (NS * (( width G) - 2)))]| by Def1;

      

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

      N > S by Th9;

      then

       A10: (N - S) > 0 by XREAL_1: 50;

      (NS * (( width G) - 2)) = ((NS * (2 |^ n)) + (NS * 1)) by A2, A3

      .= ((N - S) + NS) by A9, XCMPLX_1: 87;

      then ((G * (1,( width G))) `2 ) = (N + NS) by A8, EUCLID: 52;

      then

       A11: ((G * (1,( width G))) `2 ) > N by A9, A10, XREAL_1: 29, XREAL_1: 139;

      

       A12: i = 0 or i >= (1 + 0 ) by NAT_1: 9;

      per cases by A1, A12, XXREAL_0: 1;

        suppose i = 0 ;

        then ( cell (G,i,( width G))) = { |[r, s]| : r <= ((G * (1,1)) `1 ) & ((G * (1,( width G))) `2 ) <= s } by GOBRD11: 25;

        then

        consider r, s such that

         A13: p = |[r, s]| and r <= ((G * (1,1)) `1 ) and

         A14: ((G * (1,( width G))) `2 ) <= s by A3, A5;

        (p `2 ) = s by A13, EUCLID: 52;

        then N < (p `2 ) by A11, A14, XXREAL_0: 2;

        hence contradiction by A6, PSCOMP_1: 24;

      end;

        suppose i = ( len G);

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

        then

        consider r, s such that

         A15: p = |[r, s]| and ((G * (( len G),1)) `1 ) <= r and

         A16: ((G * (1,( width G))) `2 ) <= s by A3, A5;

        (p `2 ) = s by A15, EUCLID: 52;

        then N < (p `2 ) by A11, A16, XXREAL_0: 2;

        hence contradiction by A6, PSCOMP_1: 24;

      end;

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

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

        then

        consider r, s such that

         A17: p = |[r, s]| and ((G * (i,1)) `1 ) <= r and r <= ((G * ((i + 1),1)) `1 ) and

         A18: ((G * (1,( width G))) `2 ) <= s by A3, A5;

        (p `2 ) = s by A17, EUCLID: 52;

        then N < (p `2 ) by A11, A18, XXREAL_0: 2;

        hence contradiction by A6, PSCOMP_1: 24;

      end;

    end;

    theorem :: JORDAN8:16

    j <= ( len ( Gauge (C,n))) implies ( cell (( Gauge (C,n)),( len ( Gauge (C,n))),j)) misses C

    proof

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

      assume

       A1: j <= ( len G);

      

       A2: ( len G) = ((2 |^ n) + (1 + 2)) by Def1;

      

       A3: ( len G) = ( width G) by Def1;

      assume (( cell (G,( len G),j)) /\ C) <> {} ;

      then

      consider p such that

       A4: p in (( cell (G,( len G),j)) /\ C) by SUBSET_1: 4;

      

       A5: p in ( cell (G,( len G),j)) by A4, XBOOLE_0:def 4;

      

       A6: p in C by A4, XBOOLE_0:def 4;

      4 <= ( len G) by Th10;

      then

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

      set W = ( W-bound C), S = ( S-bound C), E = ( E-bound C), N = ( N-bound C);

      set EW = ((E - W) / (2 |^ n));

       [( len G), 1] in ( Indices G) by A3, A7, MATRIX_0: 30;

      then

       A8: (G * (( len G),1)) = |[(W + (EW * (( len G) - 2))), (S + (((N - S) / (2 |^ n)) * (1 - 2)))]| by Def1;

      

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

      E > W by Th8;

      then

       A10: (E - W) > 0 by XREAL_1: 50;

      (EW * (( len G) - 2)) = ((EW * (2 |^ n)) + (EW * 1)) by A2

      .= ((E - W) + EW) by A9, XCMPLX_1: 87;

      then ((G * (( len G),1)) `1 ) = (E + EW) by A8, EUCLID: 52;

      then

       A11: ((G * (( len G),1)) `1 ) > E by A9, A10, XREAL_1: 29, XREAL_1: 139;

      

       A12: j = 0 or j >= (1 + 0 ) by NAT_1: 9;

      per cases by A1, A12, XXREAL_0: 1;

        suppose j = 0 ;

        then ( cell (G,( len G),j)) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r & s <= ((G * (1,1)) `2 ) } by GOBRD11: 27;

        then

        consider r, s such that

         A13: p = |[r, s]| and

         A14: ((G * (( len G),1)) `1 ) <= r and s <= ((G * (1,1)) `2 ) by A5;

        (p `1 ) = r by A13, EUCLID: 52;

        then E < (p `1 ) by A11, A14, XXREAL_0: 2;

        hence contradiction by A6, PSCOMP_1: 24;

      end;

        suppose j = ( len G);

        then ( cell (G,( len G),j)) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r & ((G * (1,( width G))) `2 ) <= s } by A3, GOBRD11: 28;

        then

        consider r, s such that

         A15: p = |[r, s]| and

         A16: ((G * (( len G),1)) `1 ) <= r and ((G * (1,( width G))) `2 ) <= s by A5;

        (p `1 ) = r by A15, EUCLID: 52;

        then E < (p `1 ) by A11, A16, XXREAL_0: 2;

        hence contradiction by A6, PSCOMP_1: 24;

      end;

        suppose 1 <= j & j < ( len G);

        then ( cell (G,( len G),j)) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } by A3, GOBRD11: 29;

        then

        consider r, s such that

         A17: p = |[r, s]| and

         A18: ((G * (( len G),1)) `1 ) <= r and ((G * (1,j)) `2 ) <= s and s <= ((G * (1,(j + 1))) `2 ) by A5;

        (p `1 ) = r by A17, EUCLID: 52;

        then E < (p `1 ) by A11, A18, XXREAL_0: 2;

        hence contradiction by A6, PSCOMP_1: 24;

      end;

    end;

    theorem :: JORDAN8:17

    i <= ( len ( Gauge (C,n))) implies ( cell (( Gauge (C,n)),i, 0 )) misses C

    proof

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

      assume

       A1: i <= ( len G);

      

       A2: ( len G) = ( width G) by Def1;

      assume (( cell (G,i, 0 )) /\ C) <> {} ;

      then

      consider p such that

       A3: p in (( cell (G,i, 0 )) /\ C) by SUBSET_1: 4;

      

       A4: p in ( cell (G,i, 0 )) by A3, XBOOLE_0:def 4;

      

       A5: p in C by A3, XBOOLE_0:def 4;

      4 <= ( len G) by Th10;

      then

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

      set W = ( W-bound C), S = ( S-bound C), E = ( E-bound C), N = ( N-bound C);

      set NS = ((N - S) / (2 |^ n));

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

      then (G * (1,1)) = |[(W + (((E - W) / (2 |^ n)) * (1 - 2))), (S + (NS * (1 - 2)))]| by Def1;

      then

       A7: ((G * (1,1)) `2 ) = (S + (NS * ( - 1))) by EUCLID: 52;

      

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

      N > S by Th9;

      then (N - S) > 0 by XREAL_1: 50;

      then NS > 0 by A8, XREAL_1: 139;

      then (NS * ( - 1)) < ( 0 * ( - 1)) by XREAL_1: 69;

      then

       A9: ((G * (1,1)) `2 ) < (S + 0 ) by A7, XREAL_1: 6;

      

       A10: i = 0 or i >= (1 + 0 ) by NAT_1: 9;

      per cases by A1, A10, XXREAL_0: 1;

        suppose i = 0 ;

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

        then

        consider r, s such that

         A11: p = |[r, s]| and r <= ((G * (1,1)) `1 ) and

         A12: s <= ((G * (1,1)) `2 ) by A4;

        (p `2 ) = s by A11, EUCLID: 52;

        then S > (p `2 ) by A9, A12, XXREAL_0: 2;

        hence contradiction by A5, PSCOMP_1: 24;

      end;

        suppose i = ( len G);

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

        then

        consider r, s such that

         A13: p = |[r, s]| and ((G * (( len G),1)) `1 ) <= r and

         A14: s <= ((G * (1,1)) `2 ) by A4;

        (p `2 ) = s by A13, EUCLID: 52;

        then S > (p `2 ) by A9, A14, XXREAL_0: 2;

        hence contradiction by A5, PSCOMP_1: 24;

      end;

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

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

        then

        consider r, s such that

         A15: p = |[r, s]| and ((G * (i,1)) `1 ) <= r and r <= ((G * ((i + 1),1)) `1 ) and

         A16: s <= ((G * (1,1)) `2 ) by A4;

        (p `2 ) = s by A15, EUCLID: 52;

        then S > (p `2 ) by A9, A16, XXREAL_0: 2;

        hence contradiction by A5, PSCOMP_1: 24;

      end;

    end;

    theorem :: JORDAN8:18

    j <= ( len ( Gauge (C,n))) implies ( cell (( Gauge (C,n)), 0 ,j)) misses C

    proof

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

      assume

       A1: j <= ( len G);

      

       A2: ( len G) = ( width G) by Def1;

      assume (( cell (G, 0 ,j)) /\ C) <> {} ;

      then

      consider p such that

       A3: p in (( cell (G, 0 ,j)) /\ C) by SUBSET_1: 4;

      

       A4: p in ( cell (G, 0 ,j)) by A3, XBOOLE_0:def 4;

      

       A5: p in C by A3, XBOOLE_0:def 4;

      4 <= ( len G) by Th10;

      then

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

      set W = ( W-bound C), S = ( S-bound C), E = ( E-bound C), N = ( N-bound C);

      set EW = ((E - W) / (2 |^ n));

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

      then (G * (1,1)) = |[(W + (EW * (1 - 2))), (S + (((N - S) / (2 |^ n)) * (1 - 2)))]| by Def1;

      then

       A7: ((G * (1,1)) `1 ) = (W + (EW * ( - 1))) by EUCLID: 52;

      

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

      E > W by Th8;

      then (E - W) > 0 by XREAL_1: 50;

      then EW > 0 by A8, XREAL_1: 139;

      then (EW * ( - 1)) < ( 0 * ( - 1)) by XREAL_1: 69;

      then

       A9: ((G * (1,1)) `1 ) < (W + 0 ) by A7, XREAL_1: 6;

      

       A10: j = 0 or j >= (1 + 0 ) by NAT_1: 9;

      per cases by A1, A10, XXREAL_0: 1;

        suppose j = 0 ;

        then ( cell (G, 0 ,j)) = { |[r, s]| : r <= ((G * (1,1)) `1 ) & s <= ((G * (1,1)) `2 ) } by GOBRD11: 24;

        then

        consider r, s such that

         A11: p = |[r, s]| and

         A12: r <= ((G * (1,1)) `1 ) and s <= ((G * (1,1)) `2 ) by A4;

        (p `1 ) = r by A11, EUCLID: 52;

        then W > (p `1 ) by A9, A12, XXREAL_0: 2;

        hence contradiction by A5, PSCOMP_1: 24;

      end;

        suppose j = ( len G);

        then ( cell (G, 0 ,j)) = { |[r, s]| : r <= ((G * (1,1)) `1 ) & ((G * (1,( width G))) `2 ) <= s } by A2, GOBRD11: 25;

        then

        consider r, s such that

         A13: p = |[r, s]| and

         A14: r <= ((G * (1,1)) `1 ) and ((G * (1,( width G))) `2 ) <= s by A4;

        (p `1 ) = r by A13, EUCLID: 52;

        then W > (p `1 ) by A9, A14, XXREAL_0: 2;

        hence contradiction by A5, PSCOMP_1: 24;

      end;

        suppose 1 <= j & j < ( len G);

        then ( cell (G, 0 ,j)) = { |[r, s]| : r <= ((G * (1,1)) `1 ) & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } by A2, GOBRD11: 26;

        then

        consider r, s such that

         A15: p = |[r, s]| and

         A16: r <= ((G * (1,1)) `1 ) and ((G * (1,j)) `2 ) <= s and s <= ((G * (1,(j + 1))) `2 ) by A4;

        (p `1 ) = r by A15, EUCLID: 52;

        then W > (p `1 ) by A9, A16, XXREAL_0: 2;

        hence contradiction by A5, PSCOMP_1: 24;

      end;

    end;