jordan1i.miz



    begin

    reserve i,j,k,n for Nat;

    theorem :: JORDAN1I:1

    

     Th1: for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) > 1

    proof

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

      

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

      then 1 < (( N-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by SPRECT_2: 69;

      then 1 < (( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by A1, SPRECT_2: 70, XXREAL_0: 2;

      then 1 < (( E-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by A1, SPRECT_2: 71, XXREAL_0: 2;

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

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

      hence thesis by A1, SPRECT_2: 74, XXREAL_0: 2;

    end;

    theorem :: JORDAN1I:2

    

     Th2: for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds (( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) > 1

    proof

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

      

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

      then 1 < (( N-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by SPRECT_2: 69;

      hence thesis by A1, SPRECT_2: 70, XXREAL_0: 2;

    end;

    theorem :: JORDAN1I:3

    

     Th3: for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds (( S-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) > 1

    proof

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

      

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

      then 1 < (( N-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by SPRECT_2: 69;

      then 1 < (( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by A1, SPRECT_2: 70, XXREAL_0: 2;

      then 1 < (( E-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) by A1, SPRECT_2: 71, XXREAL_0: 2;

      hence thesis by A1, SPRECT_2: 72, XXREAL_0: 2;

    end;

    begin

    theorem :: JORDAN1I:4

    for f be non constant standard special_circular_sequence, p be Point of ( TOP-REAL 2) st p in ( rng f) holds ( left_cell (f,(p .. f))) = ( left_cell (( Rotate (f,p)),1))

    proof

      set n = 1;

      let f be non constant standard special_circular_sequence, p be Point of ( TOP-REAL 2) such that

       A1: p in ( rng f);

      set k = (p .. f);

      ( len f) > 1 by GOBOARD7: 34, XXREAL_0: 2;

      then k < ( len f) by A1, SPRECT_5: 7;

      then

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

      

       A3: 1 <= k by A1, FINSEQ_4: 21;

      

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

      proof

        (( Rotate (f,p)) /. (((1 + 1) + k) -' (p .. f))) = (( Rotate (f,p)) /. (n + 1)) by NAT_D: 34;

        then

         A5: (( Rotate (f,p)) /. (((k + 1) + 1) -' (p .. f))) = (( Rotate (f,p)) /. (n + 1));

        

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

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

         A7: [i1, j1] in ( Indices ( GoB ( Rotate (f,p)))) & [i2, j2] in ( Indices ( GoB ( Rotate (f,p)))) and

         A8: (( Rotate (f,p)) /. n) = (( GoB ( Rotate (f,p))) * (i1,j1)) and

         A9: (( Rotate (f,p)) /. (n + 1)) = (( GoB ( Rotate (f,p))) * (i2,j2));

        

         A10: ( GoB ( Rotate (f,p))) = ( GoB f) by REVROT_1: 28;

        ( len ( Rotate (f,p))) = ( len f) by FINSEQ_6: 179;

        then (( Rotate (f,p)) /. ( len f)) = (( Rotate (f,p)) /. 1) by FINSEQ_6:def 1;

        then (( Rotate (f,p)) /. ((k + ( len f)) -' (p .. f))) = (( Rotate (f,p)) /. 1) by NAT_D: 34;

        then

         A11: (f /. k) = (( GoB f) * (i1,j1)) by A1, A3, A8, A10, FINSEQ_6: 183;

        k < (k + 1) by NAT_1: 13;

        then

         A12: (f /. (k + 1)) = (( GoB f) * (i2,j2)) by A1, A2, A9, A10, A5, FINSEQ_6: 175;

        then

         A13: i1 = i2 & (j1 + 1) = j2 & ( left_cell (f,k)) = ( cell (( GoB f),(i1 -' 1),j1)) or (i1 + 1) = i2 & j1 = j2 & ( left_cell (f,k)) = ( cell (( GoB f),i1,j1)) or i1 = (i2 + 1) & j1 = j2 & ( left_cell (f,k)) = ( cell (( GoB f),i2,(j2 -' 1))) or i1 = i2 & j1 = (j2 + 1) & ( left_cell (f,k)) = ( cell (( GoB f),i1,j2)) by A3, A2, A7, A10, A11, A6, GOBOARD5:def 7;

        per cases by A3, A2, A7, A10, A11, A12, A6, GOBOARD5:def 7;

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

          hence thesis by A13, REVROT_1: 28;

        end;

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

          hence thesis by A13, REVROT_1: 28;

        end;

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

          hence thesis by A13, REVROT_1: 28;

        end;

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

          hence thesis by A13, REVROT_1: 28;

        end;

      end;

      (n + 1) <= ( len ( Rotate (f,p))) by GOBOARD7: 34, XXREAL_0: 2;

      hence thesis by A4, GOBOARD5:def 7;

    end;

    theorem :: JORDAN1I:5

    

     Th5: for f be non constant standard special_circular_sequence, p be Point of ( TOP-REAL 2) st p in ( rng f) holds ( right_cell (f,(p .. f))) = ( right_cell (( Rotate (f,p)),1))

    proof

      set n = 1;

      let f be non constant standard special_circular_sequence, p be Point of ( TOP-REAL 2) such that

       A1: p in ( rng f);

      set k = (p .. f);

      ( len f) > 1 by GOBOARD7: 34, XXREAL_0: 2;

      then k < ( len f) by A1, SPRECT_5: 7;

      then

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

      

       A3: 1 <= k by A1, FINSEQ_4: 21;

      

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

      proof

        (( Rotate (f,p)) /. (((1 + 1) + k) -' (p .. f))) = (( Rotate (f,p)) /. (n + 1)) by NAT_D: 34;

        then

         A5: (( Rotate (f,p)) /. (((k + 1) + 1) -' (p .. f))) = (( Rotate (f,p)) /. (n + 1));

        

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

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

         A7: [i1, j1] in ( Indices ( GoB ( Rotate (f,p)))) & [i2, j2] in ( Indices ( GoB ( Rotate (f,p)))) and

         A8: (( Rotate (f,p)) /. n) = (( GoB ( Rotate (f,p))) * (i1,j1)) and

         A9: (( Rotate (f,p)) /. (n + 1)) = (( GoB ( Rotate (f,p))) * (i2,j2));

        

         A10: ( GoB ( Rotate (f,p))) = ( GoB f) by REVROT_1: 28;

        ( len ( Rotate (f,p))) = ( len f) by FINSEQ_6: 179;

        then (( Rotate (f,p)) /. ( len f)) = (( Rotate (f,p)) /. 1) by FINSEQ_6:def 1;

        then (( Rotate (f,p)) /. ((k + ( len f)) -' (p .. f))) = (( Rotate (f,p)) /. 1) by NAT_D: 34;

        then

         A11: (f /. k) = (( GoB f) * (i1,j1)) by A1, A3, A8, A10, FINSEQ_6: 183;

        k < (k + 1) by NAT_1: 13;

        then

         A12: (f /. (k + 1)) = (( GoB f) * (i2,j2)) by A1, A2, A9, A10, A5, FINSEQ_6: 175;

        then

         A13: i1 = i2 & (j1 + 1) = j2 & ( right_cell (f,k)) = ( cell (( GoB f),i1,j1)) or (i1 + 1) = i2 & j1 = j2 & ( right_cell (f,k)) = ( cell (( GoB f),i1,(j1 -' 1))) or i1 = (i2 + 1) & j1 = j2 & ( right_cell (f,k)) = ( cell (( GoB f),i2,j2)) or i1 = i2 & j1 = (j2 + 1) & ( right_cell (f,k)) = ( cell (( GoB f),(i1 -' 1),j2)) by A3, A2, A7, A10, A11, A6, GOBOARD5:def 6;

        per cases by A3, A2, A7, A10, A11, A12, A6, GOBOARD5:def 6;

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

          hence thesis by A13, REVROT_1: 28;

        end;

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

          hence thesis by A13, REVROT_1: 28;

        end;

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

          hence thesis by A13, REVROT_1: 28;

        end;

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

          hence thesis by A13, REVROT_1: 28;

        end;

      end;

      (n + 1) <= ( len ( Rotate (f,p))) by GOBOARD7: 34, XXREAL_0: 2;

      hence thesis by A4, GOBOARD5:def 6;

    end;

    theorem :: JORDAN1I:6

    for C be compact connected non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds ( W-min C) in ( right_cell (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))),1))

    proof

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

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

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

      consider j be Nat such that

       A1: 1 <= j and

       A2: j <= ( width G) and

       A3: ( W-min ( L~ f)) = (G * (1,j)) by JORDAN1D: 30;

      

       A4: ( len G) >= 4 by JORDAN8: 10;

      then

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

      set k = (( W-min ( L~ f)) .. f);

      

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

      then

       A7: k in ( dom f) & (f . k) = ( W-min ( L~ f)) by FINSEQ_4: 19, FINSEQ_4: 20;

      then

       A8: (f /. k) = ( W-min ( L~ f)) by PARTFUN1:def 6;

       A9:

      now

        

         A10: 1 < (( W-min ( L~ f)) .. f) by Th1;

        

         A11: 1 in ( dom f) by A6, FINSEQ_3: 31;

        assume k = ( len f);

        then (f /. 1) = ( W-min ( L~ f)) by A8, FINSEQ_6:def 1;

        then (f . 1) = ( W-min ( L~ f)) by A11, PARTFUN1:def 6;

        hence contradiction by A11, A10, FINSEQ_4: 24;

      end;

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

      then

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

      then

       A13: [1, j] in ( Indices ( GoB f)) by JORDAN1H: 44;

      k <= ( len f) by A6, FINSEQ_4: 21;

      then k < ( len f) by A9, XXREAL_0: 1;

      then

       A14: (k + 1) <= ( len f) by NAT_1: 13;

      (f /. k) = (G * (1,j)) by A3, A7, PARTFUN1:def 6;

      then

       A15: (f /. k) = (( GoB f) * (1,j)) by JORDAN1H: 44;

      set p = ( W-min C);

      

       A16: f is_sequence_on G by JORDAN9:def 1;

      

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

      then

       A18: (k + 1) in ( dom f) by A14, FINSEQ_3: 25;

      

       A19: (k + 1) in ( dom f) by A14, A17, FINSEQ_3: 25;

      then

      consider ki,kj be Nat such that

       A20: [ki, kj] in ( Indices G) and

       A21: (f /. (k + 1)) = (G * (ki,kj)) by A16, GOBOARD1:def 9;

      

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

      

       A23: 1 <= k by Th1;

      then

       A24: ((f /. (k + 1)) `1 ) = ( W-bound ( L~ ( Cage (C,n)))) by A8, A14, JORDAN1E: 22;

      then ((G * (1,j)) `1 ) = ((G * (ki,kj)) `1 ) by A3, A21, EUCLID: 52;

      then

       A25: ki = 1 by A20, A12, JORDAN1G: 7;

      2 <= ( len f) by GOBOARD7: 34, XXREAL_0: 2;

      then (f /. (k + 1)) in ( W-most ( L~ f)) by A24, A19, GOBOARD1: 1, SPRECT_2: 12;

      then ((G * (1,j)) `2 ) <= ((G * (ki,kj)) `2 ) by A3, A21, PSCOMP_1: 31;

      then

       A26: j <= kj by A2, A25, A22, GOBOARD5: 4;

       [ki, kj] in ( Indices ( GoB f)) & (f /. (k + 1)) = (( GoB f) * (ki,kj)) by A20, A21, JORDAN1H: 44;

      then ( |.(1 - ki).| + |.(j - kj).|) = 1 by A6, A18, A13, A15, FINSEQ_4: 20, GOBOARD5: 12;

      then

       A27: ( 0 + |.(j - kj).|) = 1 by A25, ABSVALUE: 2;

      then

       A28: (f /. (k + 1)) = (G * (1,(j + 1))) by A21, A25, A26, SEQM_3: 41;

      

       A29: kj = (j + 1) by A26, A27, SEQM_3: 41;

      then 1 <= (j + 1) & (j + 1) <= ( width G) by A20, MATRIX_0: 32;

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

      then

       A30: ( right_cell (f,k,G)) = ( cell (G,1,j)) by A3, A16, A23, A8, A14, A12, A28, GOBRD13: 22;

       A31:

      now

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

        then

         A32: (j + 1) <= ( len G) by A20, A29, MATRIX_0: 32;

        1 <= (j + 1) by A20, A29, MATRIX_0: 32;

        then

         A33: ((G * (2,(j + 1))) `1 ) = ( W-bound C) by A32, JORDAN8: 11;

        assume

         A34: not p in ( right_cell (f,k,G));

        (j + 1) <= ( width G) by A20, A29, MATRIX_0: 32;

        then

         A35: j < ( width G) by NAT_1: 13;

        

         A36: 2 <= ( len G) by A4, XXREAL_0: 2;

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

        then ( LSeg ((G * ((1 + 1),j)),(G * ((1 + 1),(j + 1))))) c= ( cell (G,1,j)) by A1, A35, GOBOARD5: 18;

        then

         A37: not p in ( LSeg ((G * (2,j)),(G * (2,(j + 1))))) by A30, A34;

        

         A38: 1 <= (j + 1) & (j + 1) <= ( width G) by A20, A29, MATRIX_0: 32;

        j <= ( len G) by A2, JORDAN8:def 1;

        then

         A39: ((G * (2,j)) `1 ) = ( W-bound C) by A1, JORDAN8: 11;

        (p `1 ) = ( W-bound C) by EUCLID: 52;

        then

         A40: (p `2 ) > ((G * (2,(j + 1))) `2 ) or (p `2 ) < ((G * (2,j)) `2 ) by A37, A39, A33, GOBOARD7: 7;

        per cases by A1, A2, A40, A38, A36, GOBOARD5: 1;

          suppose

           A41: (p `2 ) > ((G * (1,(j + 1))) `2 );

          ( cell (G,1,j)) meets C by A23, A14, A30, JORDAN9: 31;

          then (( cell (G,1,j)) /\ C) <> {} by XBOOLE_0:def 7;

          then

          consider c be object such that

           A42: c in (( cell (G,1,j)) /\ C) by XBOOLE_0:def 1;

          reconsider c as Element of ( TOP-REAL 2) by A42;

          

           A43: c in ( cell (G,1,j)) by A42, XBOOLE_0:def 4;

          

           A44: c in C by A42, XBOOLE_0:def 4;

          then

           A45: (c `1 ) >= ( W-bound C) by PSCOMP_1: 24;

          

           A46: (1 + 1) <= ( len G) & (j + 1) <= ( width G) by A4, A20, A29, MATRIX_0: 32, XXREAL_0: 2;

          then (c `1 ) <= ((G * ((1 + 1),j)) `1 ) by A1, A43, JORDAN9: 17;

          then c in ( W-most C) by A39, A44, A45, SPRECT_2: 12, XXREAL_0: 1;

          then

           A47: (c `2 ) >= (p `2 ) by PSCOMP_1: 31;

          (c `2 ) <= ((G * (1,(j + 1))) `2 ) by A1, A43, A46, JORDAN9: 17;

          hence contradiction by A41, A47, XXREAL_0: 2;

        end;

          suppose

           A48: (p `2 ) < ((G * (1,j)) `2 );

          ( west_halfline p) meets ( L~ f) by JORDAN1A: 54, SPRECT_1: 13;

          then

          consider r be object such that

           A49: r in ( west_halfline p) and

           A50: r in ( L~ f) by XBOOLE_0: 3;

          reconsider r as Element of ( TOP-REAL 2) by A49;

          r in (( west_halfline p) /\ ( L~ f)) by A49, A50, XBOOLE_0:def 4;

          then (r `1 ) = ( W-bound ( L~ f)) by JORDAN1A: 85, PSCOMP_1: 34;

          then r in ( W-most ( L~ f)) by A50, SPRECT_2: 12;

          then (( W-min ( L~ f)) `2 ) <= (r `2 ) by PSCOMP_1: 31;

          hence contradiction by A3, A48, A49, TOPREAL1:def 13;

        end;

      end;

      ( GoB f) = G by JORDAN1H: 44;

      then p in ( right_cell (f,k)) by A23, A14, A31, JORDAN1H: 23;

      hence thesis by A6, Th5;

    end;

    theorem :: JORDAN1I:7

    for C be compact connected non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds ( E-max C) in ( right_cell (( Rotate (( Cage (C,n)),( E-max ( L~ ( Cage (C,n)))))),1))

    proof

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

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

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

      consider j be Nat such that

       A1: 1 <= j and

       A2: j <= ( width G) and

       A3: ( E-max ( L~ f)) = (G * (( len G),j)) by JORDAN1D: 25;

      

       A4: ( len G) >= 4 by JORDAN8: 10;

      then

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

      set k = (( E-max ( L~ f)) .. f);

      

       A6: ( E-max ( L~ f)) in ( rng f) by SPRECT_2: 46;

      then

       A7: k in ( dom f) & (f . k) = ( E-max ( L~ f)) by FINSEQ_4: 19, FINSEQ_4: 20;

      then

       A8: (f /. k) = ( E-max ( L~ f)) by PARTFUN1:def 6;

       A9:

      now

        

         A10: 1 < (( E-max ( L~ f)) .. f) by Th2;

        

         A11: 1 in ( dom f) by A6, FINSEQ_3: 31;

        assume k = ( len f);

        then (f /. 1) = ( E-max ( L~ f)) by A8, FINSEQ_6:def 1;

        then (f . 1) = ( E-max ( L~ f)) by A11, PARTFUN1:def 6;

        hence contradiction by A11, A10, FINSEQ_4: 24;

      end;

      (f /. k) = (G * (( len G),j)) by A3, A7, PARTFUN1:def 6;

      then

       A12: (f /. k) = (( GoB f) * (( len G),j)) by JORDAN1H: 44;

      k <= ( len f) by A6, FINSEQ_4: 21;

      then k < ( len f) by A9, XXREAL_0: 1;

      then

       A13: (k + 1) <= ( len f) by NAT_1: 13;

      

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

      then

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

      1 <= ((j -' 1) + 1) & ((j -' 1) + 1) <= ( width G) by A1, A2, XREAL_1: 235;

      then

       A16: [( len G), ((j -' 1) + 1)] in ( Indices G) by A14, MATRIX_0: 30;

      set p = ( E-max C);

      

       A17: f is_sequence_on G by JORDAN9:def 1;

      

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

      then

       A19: (k + 1) in ( dom f) by A13, FINSEQ_3: 25;

      

       A20: (k + 1) in ( dom f) by A13, A18, FINSEQ_3: 25;

      then

      consider ki,kj be Nat such that

       A21: [ki, kj] in ( Indices G) and

       A22: (f /. (k + 1)) = (G * (ki,kj)) by A17, GOBOARD1:def 9;

      

       A23: [ki, kj] in ( Indices ( GoB f)) & (f /. (k + 1)) = (( GoB f) * (ki,kj)) by A21, A22, JORDAN1H: 44;

      

       A24: 1 <= k by Th2;

      then

       A25: ((f /. (k + 1)) `1 ) = ( E-bound ( L~ ( Cage (C,n)))) by A8, A13, JORDAN1E: 20;

      then ((G * (( len G),j)) `1 ) = ((G * (ki,kj)) `1 ) by A3, A22, EUCLID: 52;

      then

       A26: ki = ( len G) by A21, A15, JORDAN1G: 7;

      

       A27: kj <= ( width G) & 1 <= ki by A21, MATRIX_0: 32;

       [( len G), j] in ( Indices ( GoB f)) by A15, JORDAN1H: 44;

      then ( |.(( len G) - ki).| + |.(j - kj).|) = 1 by A6, A19, A12, A23, FINSEQ_4: 20, GOBOARD5: 12;

      then

       A28: ( 0 + |.(j - kj).|) = 1 by A26, ABSVALUE: 2;

      2 <= ( len f) by GOBOARD7: 34, XXREAL_0: 2;

      then (f /. (k + 1)) in ( E-most ( L~ f)) by A25, A20, GOBOARD1: 1, SPRECT_2: 13;

      then ((G * (( len G),j)) `2 ) >= ((G * (ki,kj)) `2 ) by A3, A22, PSCOMP_1: 47;

      then j >= kj by A1, A26, A27, GOBOARD5: 4;

      then j = (kj + 1) by A28, SEQM_3: 41;

      then kj = (j - 1);

      then

       A29: kj = (j -' 1) by A1, XREAL_1: 233;

      then

       A30: 1 <= (j -' 1) by A21, MATRIX_0: 32;

      

       A31: (j -' 1) <= ( width G) by A21, A29, MATRIX_0: 32;

      (f /. k) = (G * (( len G),((j -' 1) + 1))) by A1, A3, A8, XREAL_1: 235;

      then

       A32: ( right_cell (f,k,G)) = ( cell (G,(( len G) -' 1),(j -' 1))) by A17, A24, A13, A21, A22, A26, A29, A16, GOBRD13: 28;

       A33:

      now

        (j -' 1) <= ( len G) by A31, JORDAN8:def 1;

        then

         A34: ((G * ((( len G) -' 1),(j -' 1))) `1 ) = ( E-bound C) by A30, JORDAN8: 12;

        j <= ( len G) by A2, JORDAN8:def 1;

        then

         A35: ((G * ((( len G) -' 1),j)) `1 ) = ( E-bound C) by A1, JORDAN8: 12;

        assume

         A36: not p in ( right_cell (f,k,G));

        

         A37: 1 < ( len G) by A4, XXREAL_0: 2;

        then

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

        

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

        then

         A40: ((G * (1,j)) `2 ) = ((G * ((( len G) -' 1),j)) `2 ) & ((G * (1,(j -' 1))) `2 ) = ((G * ((( len G) -' 1),(j -' 1))) `2 ) by A1, A2, A30, A31, A38, GOBOARD5: 1;

        (j -' 1) < j by A30, NAT_D: 51;

        then (j -' 1) < ( width G) by A2, XXREAL_0: 2;

        then ( LSeg ((G * ((( len G) -' 1),(j -' 1))),(G * ((( len G) -' 1),((j -' 1) + 1))))) c= ( cell (G,(( len G) -' 1),(j -' 1))) by A30, A38, A39, GOBOARD5: 19;

        then not p in ( LSeg ((G * ((( len G) -' 1),(j -' 1))),(G * ((( len G) -' 1),((j -' 1) + 1))))) by A32, A36;

        then

         A41: not p in ( LSeg ((G * ((( len G) -' 1),(j -' 1))),(G * ((( len G) -' 1),j)))) by A1, XREAL_1: 235;

        (p `1 ) = ( E-bound C) by EUCLID: 52;

        then

         A42: (p `2 ) > ((G * ((( len G) -' 1),j)) `2 ) or (p `2 ) < ((G * ((( len G) -' 1),(j -' 1))) `2 ) by A41, A34, A35, GOBOARD7: 7;

        per cases by A1, A2, A5, A30, A31, A42, A40, GOBOARD5: 1;

          suppose

           A43: (p `2 ) < ((G * (( len G),(j -' 1))) `2 );

          

           A44: 1 <= (j -' 1) & ((j -' 1) + 1) <= ( width G) by A1, A2, A21, A29, MATRIX_0: 32, XREAL_1: 235;

          ( cell (G,(( len G) -' 1),(j -' 1))) meets C by A24, A13, A32, JORDAN9: 31;

          then (( cell (G,(( len G) -' 1),(j -' 1))) /\ C) <> {} by XBOOLE_0:def 7;

          then

          consider c be object such that

           A45: c in (( cell (G,(( len G) -' 1),(j -' 1))) /\ C) by XBOOLE_0:def 1;

          reconsider c as Element of ( TOP-REAL 2) by A45;

          

           A46: 1 <= (( len G) -' 1) & ((( len G) -' 1) + 1) <= ( len G) by A37, NAT_D: 49, XREAL_1: 235;

          

           A47: c in ( cell (G,(( len G) -' 1),(j -' 1))) by A45, XBOOLE_0:def 4;

          then

           A48: ((G * ((( len G) -' 1),(j -' 1))) `1 ) <= (c `1 ) by A46, A44, JORDAN9: 17;

          

           A49: c in C by A45, XBOOLE_0:def 4;

          then (c `1 ) <= ( E-bound C) by PSCOMP_1: 24;

          then c in ( E-most C) by A34, A49, A48, SPRECT_2: 13, XXREAL_0: 1;

          then

           A50: (c `2 ) <= (p `2 ) by PSCOMP_1: 47;

          ((G * ((( len G) -' 1),(j -' 1))) `2 ) <= (c `2 ) by A47, A46, A44, JORDAN9: 17;

          then ((G * (1,(j -' 1))) `2 ) <= (c `2 ) by A30, A31, A38, A39, GOBOARD5: 1;

          then ((G * (( len G),(j -' 1))) `2 ) <= (c `2 ) by A5, A30, A31, GOBOARD5: 1;

          hence contradiction by A43, A50, XXREAL_0: 2;

        end;

          suppose

           A51: (p `2 ) > ((G * (( len G),j)) `2 );

          ( east_halfline p) meets ( L~ f) by JORDAN1A: 52, SPRECT_1: 14;

          then

          consider r be object such that

           A52: r in ( east_halfline p) and

           A53: r in ( L~ f) by XBOOLE_0: 3;

          reconsider r as Element of ( TOP-REAL 2) by A52;

          r in (( east_halfline p) /\ ( L~ f)) by A52, A53, XBOOLE_0:def 4;

          then (r `1 ) = ( E-bound ( L~ f)) by JORDAN1A: 83, PSCOMP_1: 50;

          then r in ( E-most ( L~ f)) by A53, SPRECT_2: 13;

          then (( E-max ( L~ f)) `2 ) >= (r `2 ) by PSCOMP_1: 47;

          hence contradiction by A3, A51, A52, TOPREAL1:def 11;

        end;

      end;

      ( GoB f) = G by JORDAN1H: 44;

      then p in ( right_cell (f,k)) by A24, A13, A33, JORDAN1H: 23;

      hence thesis by A6, Th5;

    end;

    theorem :: JORDAN1I:8

    for C be compact connected non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds ( S-max C) in ( right_cell (( Rotate (( Cage (C,n)),( S-max ( L~ ( Cage (C,n)))))),1))

    proof

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

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

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

      consider j be Nat such that

       A1: 1 <= j and

       A2: j <= ( len G) and

       A3: ( S-max ( L~ f)) = (G * (j,1)) by JORDAN1D: 28;

      

       A4: f is_sequence_on G by JORDAN9:def 1;

      set k = (( S-max ( L~ f)) .. f);

      

       A5: ( S-max ( L~ f)) in ( rng f) by SPRECT_2: 42;

      then

       A6: k in ( dom f) & (f . k) = ( S-max ( L~ f)) by FINSEQ_4: 19, FINSEQ_4: 20;

      then

       A7: (f /. k) = ( S-max ( L~ f)) by PARTFUN1:def 6;

       A8:

      now

        

         A9: 1 < (( S-max ( L~ f)) .. f) by Th3;

        

         A10: 1 in ( dom f) by A5, FINSEQ_3: 31;

        assume k = ( len f);

        then (f /. 1) = ( S-max ( L~ f)) by A7, FINSEQ_6:def 1;

        then (f . 1) = ( S-max ( L~ f)) by A10, PARTFUN1:def 6;

        hence contradiction by A10, A9, FINSEQ_4: 24;

      end;

      k <= ( len f) by A5, FINSEQ_4: 21;

      then k < ( len f) by A8, XXREAL_0: 1;

      then

       A11: (k + 1) <= ( len f) by NAT_1: 13;

      

       A12: (f /. k) = (G * (((j -' 1) + 1),1)) by A1, A3, A7, XREAL_1: 235;

      (f /. k) = (G * (j,1)) by A3, A6, PARTFUN1:def 6;

      then

       A13: (f /. k) = (( GoB f) * (j,1)) by JORDAN1H: 44;

      set p = ( S-max C);

      

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

      

       A15: ( len G) >= 4 by JORDAN8: 10;

      then

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

      

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

      then

       A18: (k + 1) in ( dom f) by A11, FINSEQ_3: 25;

      

       A19: (k + 1) in ( dom f) by A11, A17, FINSEQ_3: 25;

      then

      consider kj,ki be Nat such that

       A20: [kj, ki] in ( Indices G) and

       A21: (f /. (k + 1)) = (G * (kj,ki)) by A4, GOBOARD1:def 9;

      

       A22: [kj, ki] in ( Indices ( GoB f)) & (f /. (k + 1)) = (( GoB f) * (kj,ki)) by A20, A21, JORDAN1H: 44;

      

       A23: ki <= ( width G) by A20, MATRIX_0: 32;

      

       A24: 1 <= kj by A20, MATRIX_0: 32;

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

      then

       A25: [j, 1] in ( Indices G) by A1, A2, A16, MATRIX_0: 30;

      then

       A26: [((j -' 1) + 1), 1] in ( Indices G) by A1, XREAL_1: 235;

      

       A27: 1 <= k by Th3;

      then

       A28: ((f /. (k + 1)) `2 ) = ( S-bound ( L~ ( Cage (C,n)))) by A7, A11, JORDAN1E: 21;

      then ((G * (j,1)) `2 ) = ((G * (kj,ki)) `2 ) by A3, A21, EUCLID: 52;

      then

       A29: ki = 1 by A20, A25, JORDAN1G: 6;

       [j, 1] in ( Indices ( GoB f)) by A25, JORDAN1H: 44;

      then ( |.(1 - ki).| + |.(j - kj).|) = 1 by A5, A18, A13, A22, FINSEQ_4: 20, GOBOARD5: 12;

      then

       A30: ( 0 + |.(j - kj).|) = 1 by A29, ABSVALUE: 2;

      

       A31: kj <= ( len G) by A20, MATRIX_0: 32;

      2 <= ( len f) by GOBOARD7: 34, XXREAL_0: 2;

      then (f /. (k + 1)) in ( S-most ( L~ f)) by A28, A19, GOBOARD1: 1, SPRECT_2: 11;

      then ((G * (j,1)) `1 ) >= ((G * (kj,ki)) `1 ) by A3, A21, PSCOMP_1: 55;

      then kj <= j by A1, A29, A23, A31, GOBOARD5: 3;

      then (kj + 1) = j by A30, SEQM_3: 41;

      then

       A32: kj = (j - 1);

      then kj = (j -' 1) by A24, NAT_D: 39;

      then

       A33: [(j -' 1), 1] in ( Indices G) by A16, A24, A31, A14, MATRIX_0: 30;

      (f /. (k + 1)) = (G * ((j -' 1),1)) by A21, A29, A24, A32, NAT_D: 39;

      then

       A34: ( right_cell (f,k,G)) = ( cell (G,(j -' 1),1)) by A4, A27, A11, A33, A26, A12, GOBRD13: 26;

       A35:

      now

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

        then

         A36: 1 < ( width G) by JORDAN8:def 1;

        assume

         A37: not p in ( right_cell (f,k,G));

        

         A38: 1 <= (j -' 1) by A24, A32, NAT_D: 39;

        then (j -' 1) < j by NAT_D: 51;

        then (j -' 1) < ( len G) by A2, XXREAL_0: 2;

        then ( LSeg ((G * ((j -' 1),(1 + 1))),(G * (((j -' 1) + 1),(1 + 1))))) c= ( cell (G,(j -' 1),1)) by A36, A38, GOBOARD5: 21;

        then ( LSeg ((G * ((j -' 1),2)),(G * (j,2)))) c= ( cell (G,(j -' 1),1)) by A1, XREAL_1: 235;

        then

         A39: not p in ( LSeg ((G * ((j -' 1),2)),(G * (j,2)))) by A34, A37;

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

        then

         A40: 2 <= ( width G) by A15, XXREAL_0: 2;

        

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

        

         A42: (j -' 1) <= ( len G) by A24, A31, A32, NAT_D: 39;

        then

         A43: ((G * ((j -' 1),2)) `2 ) = ( S-bound C) by A38, JORDAN8: 13;

        ((G * (j,2)) `2 ) = ( S-bound C) & (p `2 ) = ( S-bound C) by A1, A2, EUCLID: 52, JORDAN8: 13;

        then

         A44: (p `1 ) > ((G * (j,2)) `1 ) or (p `1 ) < ((G * ((j -' 1),2)) `1 ) by A39, A43, GOBOARD7: 8;

        per cases by A1, A2, A38, A42, A44, A40, GOBOARD5: 2;

          suppose

           A45: (p `1 ) < ((G * ((j -' 1),1)) `1 );

          ( cell (G,(j -' 1),1)) meets C by A27, A11, A34, JORDAN9: 31;

          then (( cell (G,(j -' 1),1)) /\ C) <> {} by XBOOLE_0:def 7;

          then

          consider c be object such that

           A46: c in (( cell (G,(j -' 1),1)) /\ C) by XBOOLE_0:def 1;

          reconsider c as Element of ( TOP-REAL 2) by A46;

          

           A47: c in ( cell (G,(j -' 1),1)) by A46, XBOOLE_0:def 4;

          

           A48: c in C by A46, XBOOLE_0:def 4;

          then

           A49: (c `2 ) >= ( S-bound C) by PSCOMP_1: 24;

          

           A50: ((j -' 1) + 1) <= ( len G) & (1 + 1) <= ( width G) by A1, A2, A15, A41, XREAL_1: 235, XXREAL_0: 2;

          then (c `2 ) <= ((G * ((j -' 1),(1 + 1))) `2 ) by A38, A47, JORDAN9: 17;

          then c in ( S-most C) by A43, A48, A49, SPRECT_2: 11, XXREAL_0: 1;

          then

           A51: (c `1 ) <= (p `1 ) by PSCOMP_1: 55;

          ((G * ((j -' 1),1)) `1 ) <= (c `1 ) by A38, A47, A50, JORDAN9: 17;

          hence contradiction by A45, A51, XXREAL_0: 2;

        end;

          suppose

           A52: (p `1 ) > ((G * (j,1)) `1 );

          ( south_halfline p) meets ( L~ f) by JORDAN1A: 53, SPRECT_1: 12;

          then

          consider r be object such that

           A53: r in ( south_halfline p) and

           A54: r in ( L~ f) by XBOOLE_0: 3;

          reconsider r as Element of ( TOP-REAL 2) by A53;

          r in (( south_halfline p) /\ ( L~ f)) by A53, A54, XBOOLE_0:def 4;

          then (r `2 ) = ( S-bound ( L~ f)) by JORDAN1A: 84, PSCOMP_1: 58;

          then r in ( S-most ( L~ f)) by A54, SPRECT_2: 11;

          then (( S-max ( L~ f)) `1 ) >= (r `1 ) by PSCOMP_1: 55;

          hence contradiction by A3, A52, A53, TOPREAL1:def 12;

        end;

      end;

      ( GoB f) = G by JORDAN1H: 44;

      then p in ( right_cell (f,k)) by A27, A11, A35, JORDAN1H: 23;

      hence thesis by A5, Th5;

    end;

    begin

    theorem :: JORDAN1I:9

    

     Th9: for f be clockwise_oriented non constant standard special_circular_sequence holds for p be Point of ( TOP-REAL 2) st (p `1 ) < ( W-bound ( L~ f)) holds p in ( LeftComp f)

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

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

      set g = ( Rotate (f,( N-min ( L~ f))));

      

       A1: ( L~ f) = ( L~ g) by REVROT_1: 33;

      assume

       A2: (p `1 ) < ( W-bound ( L~ f));

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

      then (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then p in ( LeftComp g) by A1, A2, JORDAN2C: 110;

      hence thesis by REVROT_1: 36;

    end;

    theorem :: JORDAN1I:10

    

     Th10: for f be clockwise_oriented non constant standard special_circular_sequence holds for p be Point of ( TOP-REAL 2) st (p `1 ) > ( E-bound ( L~ f)) holds p in ( LeftComp f)

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

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

      set g = ( Rotate (f,( N-min ( L~ f))));

      

       A1: ( L~ f) = ( L~ g) by REVROT_1: 33;

      assume

       A2: (p `1 ) > ( E-bound ( L~ f));

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

      then (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then p in ( LeftComp g) by A1, A2, JORDAN2C: 111;

      hence thesis by REVROT_1: 36;

    end;

    theorem :: JORDAN1I:11

    

     Th11: for f be clockwise_oriented non constant standard special_circular_sequence holds for p be Point of ( TOP-REAL 2) st (p `2 ) < ( S-bound ( L~ f)) holds p in ( LeftComp f)

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

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

      set g = ( Rotate (f,( N-min ( L~ f))));

      

       A1: ( L~ f) = ( L~ g) by REVROT_1: 33;

      assume

       A2: (p `2 ) < ( S-bound ( L~ f));

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

      then (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then p in ( LeftComp g) by A1, A2, JORDAN2C: 112;

      hence thesis by REVROT_1: 36;

    end;

    theorem :: JORDAN1I:12

    

     Th12: for f be clockwise_oriented non constant standard special_circular_sequence holds for p be Point of ( TOP-REAL 2) st (p `2 ) > ( N-bound ( L~ f)) holds p in ( LeftComp f)

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

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

      set g = ( Rotate (f,( N-min ( L~ f))));

      

       A1: ( L~ f) = ( L~ g) by REVROT_1: 33;

      assume

       A2: (p `2 ) > ( N-bound ( L~ f));

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

      then (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then p in ( LeftComp g) by A1, A2, JORDAN2C: 113;

      hence thesis by REVROT_1: 36;

    end;

    theorem :: JORDAN1I:13

    

     Th13: for f be clockwise_oriented non constant standard special_circular_sequence holds for G be Go-board st f is_sequence_on G holds for i,j,k be Nat st 1 <= k & (k + 1) <= ( len f) & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * ((i + 1),j)) & (f /. (k + 1)) = (G * (i,j)) holds j < ( width G)

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      let G be Go-board;

      assume

       A1: f is_sequence_on G;

      let i,j,k be Nat;

      assume that

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

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

       A4: [(i + 1), j] in ( Indices G) & (f /. k) = (G * ((i + 1),j)) & (f /. (k + 1)) = (G * (i,j));

      assume

       A5: j >= ( width G);

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

      then

       A6: j = ( width G) by A5, XXREAL_0: 1;

      

       A7: i <= ( len G) by A3, MATRIX_0: 32;

      ( right_cell (f,k,G)) = ( cell (G,i,j)) by A1, A2, A3, A4, GOBRD13: 26;

      then not (( right_cell (f,k,G)) \ ( L~ f)) is bounded by A7, A6, JORDAN1A: 27, TOPREAL6: 90;

      then not ( RightComp f) is bounded by A1, A2, JORDAN9: 27, RLTOPSP1: 42;

      then not ( BDD ( L~ f)) is bounded by GOBRD14: 37;

      hence contradiction by JORDAN2C: 106;

    end;

    theorem :: JORDAN1I:14

    

     Th14: for f be clockwise_oriented non constant standard special_circular_sequence holds for G be Go-board st f is_sequence_on G holds for i,j,k be Nat st 1 <= k & (k + 1) <= ( len f) & [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * (i,(j + 1))) holds i < ( len G)

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      let G be Go-board;

      assume

       A1: f is_sequence_on G;

      let i,j,k be Nat;

      assume that

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

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

       A4: [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * (i,(j + 1)));

      assume

       A5: i >= ( len G);

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

      then

       A6: i = ( len G) by A5, XXREAL_0: 1;

      

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

      ( right_cell (f,k,G)) = ( cell (G,i,j)) by A1, A2, A3, A4, GOBRD13: 22;

      then not (( right_cell (f,k,G)) \ ( L~ f)) is bounded by A7, A6, JORDAN1B: 34, TOPREAL6: 90;

      then not ( RightComp f) is bounded by A1, A2, JORDAN9: 27, RLTOPSP1: 42;

      then not ( BDD ( L~ f)) is bounded by GOBRD14: 37;

      hence contradiction by JORDAN2C: 106;

    end;

    theorem :: JORDAN1I:15

    

     Th15: for f be clockwise_oriented non constant standard special_circular_sequence holds for G be Go-board st f is_sequence_on G holds for i,j,k be Nat st 1 <= k & (k + 1) <= ( len f) & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * ((i + 1),j)) holds j > 1

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      let G be Go-board;

      assume

       A1: f is_sequence_on G;

      let i,j,k be Nat;

      assume that

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

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

       A4: [(i + 1), j] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * ((i + 1),j));

      assume

       A5: j <= 1;

      1 <= j by A3, MATRIX_0: 32;

      then j = 1 by A5, XXREAL_0: 1;

      then

       A6: (j -' 1) = 0 by XREAL_1: 232;

      

       A7: i <= ( len G) by A3, MATRIX_0: 32;

      ( right_cell (f,k,G)) = ( cell (G,i,(j -' 1))) by A1, A2, A3, A4, GOBRD13: 24;

      then not (( right_cell (f,k,G)) \ ( L~ f)) is bounded by A7, A6, JORDAN1A: 26, TOPREAL6: 90;

      then not ( RightComp f) is bounded by A1, A2, JORDAN9: 27, RLTOPSP1: 42;

      then not ( BDD ( L~ f)) is bounded by GOBRD14: 37;

      hence contradiction by JORDAN2C: 106;

    end;

    theorem :: JORDAN1I:16

    

     Th16: for f be clockwise_oriented non constant standard special_circular_sequence holds for G be Go-board st f is_sequence_on G holds for i,j,k be Nat st 1 <= k & (k + 1) <= ( len f) & [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,(j + 1))) & (f /. (k + 1)) = (G * (i,j)) holds i > 1

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      let G be Go-board;

      assume

       A1: f is_sequence_on G;

      let i,j,k be Nat;

      assume that

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

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

       A4: [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,(j + 1))) & (f /. (k + 1)) = (G * (i,j));

      assume

       A5: i <= 1;

      1 <= i by A3, MATRIX_0: 32;

      then i = 1 by A5, XXREAL_0: 1;

      then

       A6: (i -' 1) = 0 by XREAL_1: 232;

      

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

      ( right_cell (f,k,G)) = ( cell (G,(i -' 1),j)) by A1, A2, A3, A4, GOBRD13: 28;

      then not (( right_cell (f,k,G)) \ ( L~ f)) is bounded by A7, A6, JORDAN1B: 33, TOPREAL6: 90;

      then not ( RightComp f) is bounded by A1, A2, JORDAN9: 27, RLTOPSP1: 42;

      then not ( BDD ( L~ f)) is bounded by GOBRD14: 37;

      hence contradiction by JORDAN2C: 106;

    end;

    theorem :: JORDAN1I:17

    

     Th17: for f be clockwise_oriented non constant standard special_circular_sequence holds for G be Go-board st f is_sequence_on G holds for i,j,k be Nat st 1 <= k & (k + 1) <= ( len f) & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * ((i + 1),j)) & (f /. (k + 1)) = (G * (i,j)) holds ((f /. k) `2 ) <> ( N-bound ( L~ f))

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      let G be Go-board;

      assume

       A1: f is_sequence_on G;

      let i,j,k be Nat;

      assume that

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

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

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

       A5: (f /. k) = (G * ((i + 1),j)) and

       A6: (f /. (k + 1)) = (G * (i,j)) and

       A7: ((f /. k) `2 ) = ( N-bound ( L~ f));

      

       A8: ( right_cell (f,k,G)) = ( cell (G,i,j)) by A1, A2, A3, A4, A5, A6, GOBRD13: 26;

      

       A9: j <= ( width G) by A4, MATRIX_0: 32;

      

       A10: 1 <= (i + 1) & 1 <= j by A4, MATRIX_0: 32;

      set p = ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))));

      

       A11: ( 0 + 1) <= i & 1 <= j by A3, MATRIX_0: 32;

      

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

      

       A13: (i + 1) <= ( len G) by A4, MATRIX_0: 32;

      per cases by A12, XXREAL_0: 1;

        suppose j = ( width G);

        hence contradiction by A1, A2, A3, A4, A5, A6, Th13;

      end;

        suppose

         A14: j < ( width G);

        i < ( len G) by A13, NAT_1: 13;

        then

         A15: ( Int ( cell (G,i,j))) = { |[r, s]| where r,s be Real : ((G * (i,1)) `1 ) < r & r < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s & s < ((G * (1,(j + 1))) `2 ) } by A11, A14, GOBOARD6: 26;

        (j + 1) <= ( width G) by A14, NAT_1: 13;

        then

         A16: p in ( Int ( right_cell (f,k,G))) by A11, A13, A8, GOBOARD6: 31;

        then

        consider r,s be Real such that

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

         A18: ((G * (1,j)) `2 ) < s and s < ((G * (1,(j + 1))) `2 ) by A8, A15;

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

        then (p `2 ) > ( N-bound ( L~ f)) by A5, A7, A13, A10, A9, A18, GOBOARD5: 1;

        then

         A19: p in ( LeftComp f) by Th12;

        ( Int ( right_cell (f,k,G))) c= ( RightComp f) by A1, A2, JORDAN1H: 25;

        then p in (( LeftComp f) /\ ( RightComp f)) by A16, A19, XBOOLE_0:def 4;

        then ( LeftComp f) meets ( RightComp f) by XBOOLE_0:def 7;

        hence contradiction by GOBRD14: 14;

      end;

    end;

    theorem :: JORDAN1I:18

    

     Th18: for f be clockwise_oriented non constant standard special_circular_sequence holds for G be Go-board st f is_sequence_on G holds for i,j,k be Nat st 1 <= k & (k + 1) <= ( len f) & [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * (i,(j + 1))) holds ((f /. k) `1 ) <> ( E-bound ( L~ f))

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      let G be Go-board;

      assume

       A1: f is_sequence_on G;

      let i,j,k be Nat;

      assume that

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

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

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

       A5: (f /. k) = (G * (i,j)) and

       A6: (f /. (k + 1)) = (G * (i,(j + 1))) and

       A7: ((f /. k) `1 ) = ( E-bound ( L~ f));

      

       A8: ( right_cell (f,k,G)) = ( cell (G,i,j)) by A1, A2, A3, A4, A5, A6, GOBRD13: 22;

      

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

      

       A10: ( 0 + 1) <= i & 1 <= j by A3, MATRIX_0: 32;

      set p = ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))));

      

       A11: i <= ( len G) by A3, MATRIX_0: 32;

      

       A12: (j + 1) <= ( width G) by A4, MATRIX_0: 32;

      per cases by A11, XXREAL_0: 1;

        suppose i = ( len G);

        hence contradiction by A1, A2, A3, A4, A5, A6, Th14;

      end;

        suppose

         A13: i < ( len G);

        j < ( width G) by A12, NAT_1: 13;

        then

         A14: ( Int ( cell (G,i,j))) = { |[r, s]| where r,s be Real : ((G * (i,1)) `1 ) < r & r < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s & s < ((G * (1,(j + 1))) `2 ) } by A10, A13, GOBOARD6: 26;

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

        then

         A15: p in ( Int ( right_cell (f,k,G))) by A10, A12, A8, GOBOARD6: 31;

        then

        consider r,s be Real such that

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

         A17: ((G * (i,1)) `1 ) < r and r < ((G * ((i + 1),1)) `1 ) and ((G * (1,j)) `2 ) < s and s < ((G * (1,(j + 1))) `2 ) by A8, A14;

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

        then (p `1 ) > ( E-bound ( L~ f)) by A5, A7, A11, A10, A9, A17, GOBOARD5: 2;

        then

         A18: p in ( LeftComp f) by Th10;

        ( Int ( right_cell (f,k,G))) c= ( RightComp f) by A1, A2, JORDAN1H: 25;

        then p in (( LeftComp f) /\ ( RightComp f)) by A15, A18, XBOOLE_0:def 4;

        then ( LeftComp f) meets ( RightComp f) by XBOOLE_0:def 7;

        hence contradiction by GOBRD14: 14;

      end;

    end;

    theorem :: JORDAN1I:19

    

     Th19: for f be clockwise_oriented non constant standard special_circular_sequence holds for G be Go-board st f is_sequence_on G holds for i,j,k be Nat st 1 <= k & (k + 1) <= ( len f) & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * ((i + 1),j)) holds ((f /. k) `2 ) <> ( S-bound ( L~ f))

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      let G be Go-board;

      assume

       A1: f is_sequence_on G;

      let i,j,k be Nat;

      assume that

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

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

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

       A5: (f /. k) = (G * (i,j)) and

       A6: (f /. (k + 1)) = (G * ((i + 1),j)) and

       A7: ((f /. k) `2 ) = ( S-bound ( L~ f));

      

       A8: ( right_cell (f,k,G)) = ( cell (G,i,(j -' 1))) by A1, A2, A3, A4, A5, A6, GOBRD13: 24;

      

       A9: i <= ( len G) by A3, MATRIX_0: 32;

      

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

      

       A11: (i + 1) <= ( len G) by A4, MATRIX_0: 32;

      set p = ((1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))));

      

       A12: ( 0 + 1) <= i by A3, MATRIX_0: 32;

      

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

      then

       A14: ((j -' 1) + 1) = j by XREAL_1: 235;

      per cases by A13, XXREAL_0: 1;

        suppose j = 1;

        hence contradiction by A1, A2, A3, A4, A5, A6, Th15;

      end;

        suppose j > 1;

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

        then

         A15: (j - 1) >= ((1 + 1) - 1) by XREAL_1: 9;

        j < (( width G) + 1) by A10, NAT_1: 13;

        then

         A16: (j - 1) < ((( width G) + 1) - 1) by XREAL_1: 9;

        i < ( len G) by A11, NAT_1: 13;

        then

         A17: ( Int ( cell (G,i,(j -' 1)))) = { |[r, s]| where r,s be Real : ((G * (i,1)) `1 ) < r & r < ((G * ((i + 1),1)) `1 ) & ((G * (1,(j -' 1))) `2 ) < s & s < ((G * (1,j)) `2 ) } by A12, A14, A15, A16, GOBOARD6: 26;

        

         A18: p in ( Int ( right_cell (f,k,G))) by A12, A10, A11, A8, A14, A15, GOBOARD6: 31;

        then

        consider r,s be Real such that

         A19: p = |[r, s]| and ((G * (i,1)) `1 ) < r and r < ((G * ((i + 1),1)) `1 ) and ((G * (1,(j -' 1))) `2 ) < s and

         A20: s < ((G * (1,j)) `2 ) by A8, A17;

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

        then (p `2 ) < ( S-bound ( L~ f)) by A5, A7, A12, A9, A13, A10, A20, GOBOARD5: 1;

        then

         A21: p in ( LeftComp f) by Th11;

        ( Int ( right_cell (f,k,G))) c= ( RightComp f) by A1, A2, JORDAN1H: 25;

        then p in (( LeftComp f) /\ ( RightComp f)) by A18, A21, XBOOLE_0:def 4;

        then ( LeftComp f) meets ( RightComp f) by XBOOLE_0:def 7;

        hence contradiction by GOBRD14: 14;

      end;

    end;

    theorem :: JORDAN1I:20

    

     Th20: for f be clockwise_oriented non constant standard special_circular_sequence holds for G be Go-board st f is_sequence_on G holds for i,j,k be Nat st 1 <= k & (k + 1) <= ( len f) & [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,(j + 1))) & (f /. (k + 1)) = (G * (i,j)) holds ((f /. k) `1 ) <> ( W-bound ( L~ f))

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      let G be Go-board;

      assume

       A1: f is_sequence_on G;

      let i,j,k be Nat;

      assume that

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

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

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

       A5: (f /. k) = (G * (i,(j + 1))) and

       A6: (f /. (k + 1)) = (G * (i,j)) and

       A7: ((f /. k) `1 ) = ( W-bound ( L~ f));

      

       A8: ( right_cell (f,k,G)) = ( cell (G,(i -' 1),j)) by A1, A2, A3, A4, A5, A6, GOBRD13: 28;

      

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

      

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

      

       A11: 1 <= (j + 1) by A4, MATRIX_0: 32;

      

       A12: (j + 1) <= ( width G) by A4, MATRIX_0: 32;

      set p = ((1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))));

      

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

      

       A14: ( 0 + 1) <= i by A3, MATRIX_0: 32;

      then

       A15: ((i -' 1) + 1) = i by XREAL_1: 235;

      per cases by A14, XXREAL_0: 1;

        suppose i = 1;

        hence contradiction by A1, A2, A3, A4, A5, A6, Th16;

      end;

        suppose i > 1;

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

        then

         A16: (i - 1) >= ((1 + 1) - 1) by XREAL_1: 9;

        i < (( len G) + 1) by A13, NAT_1: 13;

        then

         A17: (i - 1) < ((( len G) + 1) - 1) by XREAL_1: 9;

        j < ( width G) by A12, NAT_1: 13;

        then

         A18: ( Int ( cell (G,(i -' 1),j))) = { |[r, s]| where r,s be Real : ((G * ((i -' 1),1)) `1 ) < r & r < ((G * (i,1)) `1 ) & ((G * (1,j)) `2 ) < s & s < ((G * (1,(j + 1))) `2 ) } by A10, A15, A16, A17, GOBOARD6: 26;

        

         A19: p in ( Int ( right_cell (f,k,G))) by A13, A10, A12, A8, A15, A16, GOBOARD6: 31;

        then

        consider r,s be Real such that

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

         A21: r < ((G * (i,1)) `1 ) and ((G * (1,j)) `2 ) < s and s < ((G * (1,(j + 1))) `2 ) by A8, A18;

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

        then (p `1 ) < ( W-bound ( L~ f)) by A5, A7, A9, A11, A12, A21, GOBOARD5: 2;

        then

         A22: p in ( LeftComp f) by Th9;

        ( Int ( right_cell (f,k,G))) c= ( RightComp f) by A1, A2, JORDAN1H: 25;

        then p in (( LeftComp f) /\ ( RightComp f)) by A19, A22, XBOOLE_0:def 4;

        then ( LeftComp f) meets ( RightComp f) by XBOOLE_0:def 7;

        hence contradiction by GOBRD14: 14;

      end;

    end;

    theorem :: JORDAN1I:21

    

     Th21: for f be clockwise_oriented non constant standard special_circular_sequence holds for G be Go-board holds for k be Nat st f is_sequence_on G & 1 <= k & (k + 1) <= ( len f) & (f /. k) = ( W-min ( L~ f)) holds ex i,j be Nat st [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * (i,(j + 1)))

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      let G be Go-board;

      let k be Nat;

      assume that

       A1: f is_sequence_on G and

       A2: 1 <= k and

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

       A4: (f /. k) = ( W-min ( L~ f));

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

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

       A6: (f /. k) = (G * (i1,j1)) and

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

       A8: (f /. (k + 1)) = (G * (i2,j2)) and

       A9: 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, A2, A3, JORDAN8: 3;

      

       A10: ((G * (i1,j1)) `1 ) = ( W-bound ( L~ f)) by A4, A6, EUCLID: 52;

      

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

      

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

      take i1, j1;

      

       A13: 1 <= i1 by A5, MATRIX_0: 32;

      

       A14: (k + 1) >= (1 + 1) by A2, XREAL_1: 7;

      then

       A15: ( len f) >= 2 by A3, XXREAL_0: 2;

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

      then

       A16: (k + 1) in ( dom f) by A3, FINSEQ_3: 25;

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

      then

       A17: ((G * (i1,j1)) `1 ) <= ((G * (i2,j2)) `1 ) by A8, A10, PSCOMP_1: 24;

      

       A18: i1 <= ( len G) & j1 <= ( width G) by A5, MATRIX_0: 32;

      

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

      then

       A20: k in ( dom f) by A2, FINSEQ_3: 25;

      

       A21: i2 <= ( len G) & j2 <= ( width G) by A7, MATRIX_0: 32;

      

       A22: 1 <= j1 by A5, MATRIX_0: 32;

      per cases by A9;

        suppose

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

        thus [i1, j1] in ( Indices G) by A5;

        thus [i1, (j1 + 1)] in ( Indices G) by A7, A23;

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

        thus thesis by A8, A23;

      end;

        suppose

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

        reconsider k9 = (k - 1) as Nat by A20, FINSEQ_3: 26;

        k > 1 by A2, A24, XXREAL_0: 1;

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

        then

         A25: k9 >= ((1 + 1) - 1) by XREAL_1: 9;

        then

        consider i3,j3,i4,j4 be Nat such that

         A26: [i3, j3] in ( Indices G) and

         A27: (f /. k9) = (G * (i3,j3)) and

         A28: [i4, j4] in ( Indices G) and

         A29: (f /. (k9 + 1)) = (G * (i4,j4)) and

         A30: i3 = i4 & (j3 + 1) = j4 or (i3 + 1) = i4 & j3 = j4 or i3 = (i4 + 1) & j3 = j4 or i3 = i4 & j3 = (j4 + 1) by A1, A19, JORDAN8: 3;

        

         A31: i1 = i4 by A5, A6, A28, A29, GOBOARD1: 5;

        (k9 + 1) < ( len f) by A3, NAT_1: 13;

        then k9 < ( len f) by NAT_1: 13;

        then

         A32: k9 in ( dom f) by A25, FINSEQ_3: 25;

        

         A33: 1 <= i3 by A26, MATRIX_0: 32;

        

         A34: j1 = j4 by A5, A6, A28, A29, GOBOARD1: 5;

        

         A35: 1 <= j3 by A26, MATRIX_0: 32;

        

         A36: i3 <= ( len G) & j3 <= ( width G) by A26, MATRIX_0: 32;

        

         A37: j3 = j4

        proof

          assume

           A38: j3 <> j4;

          per cases by A30, A38;

            suppose

             A39: i3 = i4 & j3 = (j4 + 1);

            then ((G * (i3,j3)) `1 ) <> ( W-bound ( L~ f)) by A1, A19, A25, A26, A27, A28, A29, Th20;

            then ((G * (i3,1)) `1 ) <> ( W-bound ( L~ f)) by A33, A35, A36, GOBOARD5: 2;

            then (( W-min ( L~ f)) `1 ) <> ( W-bound ( L~ f)) by A4, A6, A13, A22, A18, A31, A39, GOBOARD5: 2;

            hence contradiction by EUCLID: 52;

          end;

            suppose

             A40: i3 = i4 & (j3 + 1) = j4;

            ((G * (i3,j3)) `1 ) = ((G * (i3,1)) `1 ) by A33, A35, A36, GOBOARD5: 2

            .= (( W-min ( L~ f)) `1 ) by A4, A6, A13, A22, A18, A31, A40, GOBOARD5: 2

            .= ( W-bound ( L~ f)) by EUCLID: 52;

            then (G * (i3,j3)) in ( W-most ( L~ f)) by A15, A27, A32, GOBOARD1: 1, SPRECT_2: 12;

            then ((G * (i4,j4)) `2 ) <= ((G * (i3,j3)) `2 ) by A4, A29, PSCOMP_1: 31;

            then j3 >= (j3 + 1) by A13, A18, A31, A34, A35, A40, GOBOARD5: 4;

            hence contradiction by NAT_1: 13;

          end;

        end;

        

         A41: (k9 + 1) = k;

        (f /. k9) in ( L~ f) by A3, A14, A32, GOBOARD1: 1, XXREAL_0: 2;

        then

         A42: ((G * (i1,j1)) `1 ) <= ((G * (i3,j3)) `1 ) by A10, A27, PSCOMP_1: 24;

        now

          per cases by A30, A37;

            suppose (i3 + 1) = i4;

            then i3 >= (i3 + 1) by A22, A18, A31, A34, A33, A42, A37, GOBOARD5: 3;

            hence contradiction by NAT_1: 13;

          end;

            suppose

             A43: i3 = (i4 + 1);

            (k9 + (1 + 1)) <= ( len f) by A3;

            then

             A44: (( LSeg (f,k9)) /\ ( LSeg (f,k))) = {(f /. k)} by A25, A41, TOPREAL1:def 6;

            (f /. k9) in ( LSeg (f,k9)) & (f /. (k + 1)) in ( LSeg (f,k)) by A2, A3, A19, A25, A41, TOPREAL1: 21;

            then (f /. (k + 1)) in {(f /. k)} by A8, A24, A27, A31, A34, A37, A43, A44, XBOOLE_0:def 4;

            then

             A45: (f /. (k + 1)) = (f /. k) by TARSKI:def 1;

            i1 <> i2 by A24;

            hence contradiction by A5, A6, A7, A8, A45, GOBOARD1: 5;

          end;

        end;

        hence thesis;

      end;

        suppose

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

        set k1 = ( len f);

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

        then

         A47: ( len f) > (1 + 0 ) by A2, XXREAL_0: 2;

        then ( len f) in ( dom f) by FINSEQ_3: 25;

        then

        reconsider k9 = (( len f) - 1) as Nat by FINSEQ_3: 26;

        (k + 1) >= (1 + 1) by A2, XREAL_1: 7;

        then ( len f) >= (1 + 1) by A3, XXREAL_0: 2;

        then

         A48: k9 >= ((1 + 1) - 1) by XREAL_1: 9;

        then

        consider i3,j3,i4,j4 be Nat such that

         A49: [i3, j3] in ( Indices G) and

         A50: (f /. k9) = (G * (i3,j3)) and

         A51: [i4, j4] in ( Indices G) and

         A52: (f /. (k9 + 1)) = (G * (i4,j4)) and

         A53: i3 = i4 & (j3 + 1) = j4 or (i3 + 1) = i4 & j3 = j4 or i3 = (i4 + 1) & j3 = j4 or i3 = i4 & j3 = (j4 + 1) by A1, JORDAN8: 3;

        

         A54: (f /. k1) = (f /. 1) by FINSEQ_6:def 1;

        then

         A55: i1 = i4 by A5, A6, A46, A51, A52, GOBOARD1: 5;

        

         A56: j1 = j4 by A5, A6, A46, A54, A51, A52, GOBOARD1: 5;

        

         A57: 1 <= j3 by A49, MATRIX_0: 32;

        (k9 + 1) <= ( len f);

        then k9 < ( len f) by NAT_1: 13;

        then

         A58: k9 in ( dom f) by A48, FINSEQ_3: 25;

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

        then

         A59: ((G * (i1,j1)) `1 ) <= ((G * (i3,j3)) `1 ) by A10, A50, PSCOMP_1: 24;

        

         A60: 1 <= i3 by A49, MATRIX_0: 32;

        

         A61: i3 <= ( len G) & j3 <= ( width G) by A49, MATRIX_0: 32;

        

         A62: j3 = j4

        proof

          assume

           A63: j3 <> j4;

          per cases by A53, A63;

            suppose

             A64: i3 = i4 & j3 = (j4 + 1);

            then ((G * (i3,j3)) `1 ) <> ( W-bound ( L~ f)) by A1, A48, A49, A50, A51, A52, Th20;

            then ((G * (i3,1)) `1 ) <> ( W-bound ( L~ f)) by A60, A57, A61, GOBOARD5: 2;

            then (( W-min ( L~ f)) `1 ) <> ( W-bound ( L~ f)) by A4, A6, A13, A22, A18, A55, A64, GOBOARD5: 2;

            hence contradiction by EUCLID: 52;

          end;

            suppose

             A65: i3 = i4 & (j3 + 1) = j4;

            ((G * (i3,j3)) `1 ) = ((G * (i3,1)) `1 ) by A60, A57, A61, GOBOARD5: 2

            .= (( W-min ( L~ f)) `1 ) by A4, A6, A13, A22, A18, A55, A65, GOBOARD5: 2

            .= ( W-bound ( L~ f)) by EUCLID: 52;

            then (G * (i3,j3)) in ( W-most ( L~ f)) by A15, A50, A58, GOBOARD1: 1, SPRECT_2: 12;

            then ((G * (i4,j4)) `2 ) <= ((G * (i3,j3)) `2 ) by A4, A46, A54, A52, PSCOMP_1: 31;

            then j3 >= (j3 + 1) by A13, A18, A55, A56, A57, A65, GOBOARD5: 4;

            hence contradiction by NAT_1: 13;

          end;

        end;

        

         A66: (k9 + 1) = k1;

        now

          per cases by A53, A62;

            suppose (i3 + 1) = i4;

            then i3 >= (i3 + 1) by A22, A18, A55, A56, A60, A59, A62, GOBOARD5: 3;

            hence contradiction by NAT_1: 13;

          end;

            suppose

             A67: i3 = (i4 + 1);

            (( len f) - 1) >= 0 by A47, XREAL_1: 19;

            then (( len f) -' 1) = (( len f) - 1) by XREAL_0:def 2;

            

            then

             A68: (( LSeg (f,k)) /\ ( LSeg (f,k9))) = {(f . k)} by A46, JORDAN4: 42

            .= {(f /. k)} by A20, PARTFUN1:def 6;

            (f /. k9) in ( LSeg (f,k9)) & (f /. (k + 1)) in ( LSeg (f,k)) by A2, A3, A48, A66, TOPREAL1: 21;

            then (f /. (k + 1)) in {(f /. k)} by A8, A46, A50, A55, A56, A62, A67, A68, XBOOLE_0:def 4;

            then

             A69: (f /. (k + 1)) = (f /. k) by TARSKI:def 1;

            i1 <> i2 by A46;

            hence contradiction by A5, A6, A7, A8, A69, GOBOARD1: 5;

          end;

        end;

        hence thesis;

      end;

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

        then i2 >= (i2 + 1) by A22, A18, A12, A17, GOBOARD5: 3;

        hence thesis by NAT_1: 13;

      end;

        suppose

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

        ((G * (i2,j2)) `1 ) = ((G * (i2,1)) `1 ) by A12, A11, A21, GOBOARD5: 2

        .= ( W-bound ( L~ f)) by A13, A22, A18, A10, A70, GOBOARD5: 2;

        then (G * (i2,j2)) in ( W-most ( L~ f)) by A8, A15, A16, GOBOARD1: 1, SPRECT_2: 12;

        then ((G * (i1,j1)) `2 ) <= ((G * (i2,j2)) `2 ) by A4, A6, PSCOMP_1: 31;

        then j2 >= (j2 + 1) by A13, A18, A11, A70, GOBOARD5: 4;

        hence thesis by NAT_1: 13;

      end;

    end;

    theorem :: JORDAN1I:22

    for f be clockwise_oriented non constant standard special_circular_sequence holds for G be Go-board holds for k be Nat st f is_sequence_on G & 1 <= k & (k + 1) <= ( len f) & (f /. k) = ( N-min ( L~ f)) holds ex i,j be Nat st [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * ((i + 1),j))

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      let G be Go-board;

      let k be Nat;

      assume that

       A1: f is_sequence_on G and

       A2: 1 <= k and

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

       A4: (f /. k) = ( N-min ( L~ f));

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

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

       A6: (f /. k) = (G * (i1,j1)) and

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

       A8: (f /. (k + 1)) = (G * (i2,j2)) and

       A9: 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, A2, A3, JORDAN8: 3;

      

       A10: ((G * (i1,j1)) `2 ) = ( N-bound ( L~ f)) by A4, A6, EUCLID: 52;

      

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

      

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

      take i1, j1;

      

       A13: 1 <= i1 by A5, MATRIX_0: 32;

      

       A14: (k + 1) >= (1 + 1) by A2, XREAL_1: 7;

      then

       A15: ( len f) >= 2 by A3, XXREAL_0: 2;

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

      then

       A16: (k + 1) in ( dom f) by A3, FINSEQ_3: 25;

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

      then

       A17: ((G * (i1,j1)) `2 ) >= ((G * (i2,j2)) `2 ) by A8, A10, PSCOMP_1: 24;

      

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

      

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

      then

       A20: k in ( dom f) by A2, FINSEQ_3: 25;

      

       A21: i2 <= ( len G) & 1 <= j2 by A7, MATRIX_0: 32;

      

       A22: i1 <= ( len G) & 1 <= j1 by A5, MATRIX_0: 32;

      per cases by A9;

        suppose

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

        thus [i1, j1] in ( Indices G) by A5;

        thus [(i1 + 1), j1] in ( Indices G) by A7, A23;

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

        thus thesis by A8, A23;

      end;

        suppose

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

        reconsider k9 = (k - 1) as Nat by A20, FINSEQ_3: 26;

        k > 1 by A2, A24, XXREAL_0: 1;

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

        then

         A25: k9 >= ((1 + 1) - 1) by XREAL_1: 9;

        then

        consider i3,j3,i4,j4 be Nat such that

         A26: [i3, j3] in ( Indices G) and

         A27: (f /. k9) = (G * (i3,j3)) and

         A28: [i4, j4] in ( Indices G) and

         A29: (f /. (k9 + 1)) = (G * (i4,j4)) and

         A30: i3 = i4 & (j3 + 1) = j4 or (i3 + 1) = i4 & j3 = j4 or i3 = (i4 + 1) & j3 = j4 or i3 = i4 & j3 = (j4 + 1) by A1, A19, JORDAN8: 3;

        

         A31: i1 = i4 by A5, A6, A28, A29, GOBOARD1: 5;

        (k9 + 1) < ( len f) by A3, NAT_1: 13;

        then k9 < ( len f) by NAT_1: 13;

        then

         A32: k9 in ( dom f) by A25, FINSEQ_3: 25;

        

         A33: 1 <= i3 by A26, MATRIX_0: 32;

        

         A34: j3 <= ( width G) by A26, MATRIX_0: 32;

        

         A35: j1 = j4 by A5, A6, A28, A29, GOBOARD1: 5;

        

         A36: i3 <= ( len G) & 1 <= j3 by A26, MATRIX_0: 32;

        

         A37: i3 = i4

        proof

          assume

           A38: i3 <> i4;

          per cases by A30, A38;

            suppose

             A39: j3 = j4 & i3 = (i4 + 1);

            then ((G * (i3,j3)) `2 ) <> ( N-bound ( L~ f)) by A1, A19, A25, A26, A27, A28, A29, Th17;

            then ((G * (1,j3)) `2 ) <> ( N-bound ( L~ f)) by A33, A36, A34, GOBOARD5: 1;

            then (( N-min ( L~ f)) `2 ) <> ( N-bound ( L~ f)) by A4, A6, A13, A22, A18, A35, A39, GOBOARD5: 1;

            hence contradiction by EUCLID: 52;

          end;

            suppose

             A40: j3 = j4 & (i3 + 1) = i4;

            ((G * (i3,j3)) `2 ) = ((G * (1,j3)) `2 ) by A33, A36, A34, GOBOARD5: 1

            .= (( N-min ( L~ f)) `2 ) by A4, A6, A13, A22, A18, A35, A40, GOBOARD5: 1

            .= ( N-bound ( L~ f)) by EUCLID: 52;

            then (G * (i3,j3)) in ( N-most ( L~ f)) by A15, A27, A32, GOBOARD1: 1, SPRECT_2: 10;

            then ((G * (i4,j4)) `1 ) <= ((G * (i3,j3)) `1 ) by A4, A29, PSCOMP_1: 39;

            then i3 >= (i3 + 1) by A22, A18, A31, A35, A33, A40, GOBOARD5: 3;

            hence contradiction by NAT_1: 13;

          end;

        end;

        

         A41: (k9 + 1) = k;

        (f /. k9) in ( L~ f) by A3, A14, A32, GOBOARD1: 1, XXREAL_0: 2;

        then

         A42: ((G * (i1,j1)) `2 ) >= ((G * (i3,j3)) `2 ) by A10, A27, PSCOMP_1: 24;

        now

          per cases by A30, A37;

            suppose (j4 + 1) = j3;

            then j4 >= (j4 + 1) by A13, A22, A31, A35, A34, A42, A37, GOBOARD5: 4;

            hence contradiction by NAT_1: 13;

          end;

            suppose

             A43: j4 = (j3 + 1);

            (k9 + (1 + 1)) <= ( len f) by A3;

            then

             A44: (( LSeg (f,k9)) /\ ( LSeg (f,k))) = {(f /. k)} by A25, A41, TOPREAL1:def 6;

            (f /. k9) in ( LSeg (f,k9)) & (f /. (k + 1)) in ( LSeg (f,k)) by A2, A3, A19, A25, A41, TOPREAL1: 21;

            then (f /. (k + 1)) in {(f /. k)} by A8, A24, A27, A31, A35, A37, A43, A44, XBOOLE_0:def 4;

            then

             A45: (f /. (k + 1)) = (f /. k) by TARSKI:def 1;

            j1 <> j2 by A24;

            hence contradiction by A5, A6, A7, A8, A45, GOBOARD1: 5;

          end;

        end;

        hence thesis;

      end;

        suppose

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

        set k1 = ( len f);

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

        then

         A47: ( len f) > (1 + 0 ) by A2, XXREAL_0: 2;

        then ( len f) in ( dom f) by FINSEQ_3: 25;

        then

        reconsider k9 = (( len f) - 1) as Nat by FINSEQ_3: 26;

        (k + 1) >= (1 + 1) by A2, XREAL_1: 7;

        then ( len f) >= (1 + 1) by A3, XXREAL_0: 2;

        then

         A48: k9 >= ((1 + 1) - 1) by XREAL_1: 9;

        then

        consider i3,j3,i4,j4 be Nat such that

         A49: [i3, j3] in ( Indices G) and

         A50: (f /. k9) = (G * (i3,j3)) and

         A51: [i4, j4] in ( Indices G) and

         A52: (f /. (k9 + 1)) = (G * (i4,j4)) and

         A53: i3 = i4 & (j3 + 1) = j4 or (i3 + 1) = i4 & j3 = j4 or i3 = (i4 + 1) & j3 = j4 or i3 = i4 & j3 = (j4 + 1) by A1, JORDAN8: 3;

        

         A54: (f /. k1) = (f /. 1) by FINSEQ_6:def 1;

        then

         A55: i1 = i4 by A5, A6, A46, A51, A52, GOBOARD1: 5;

        (k9 + 1) <= ( len f);

        then k9 < ( len f) by NAT_1: 13;

        then

         A56: k9 in ( dom f) by A48, FINSEQ_3: 25;

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

        then

         A57: ((G * (i1,j1)) `2 ) >= ((G * (i3,j3)) `2 ) by A10, A50, PSCOMP_1: 24;

        

         A58: 1 <= i3 by A49, MATRIX_0: 32;

        

         A59: j1 = j4 by A5, A6, A46, A54, A51, A52, GOBOARD1: 5;

        

         A60: j3 <= ( width G) by A49, MATRIX_0: 32;

        

         A61: i3 <= ( len G) & 1 <= j3 by A49, MATRIX_0: 32;

        

         A62: i3 = i4

        proof

          assume

           A63: i3 <> i4;

          per cases by A53, A63;

            suppose

             A64: j3 = j4 & i3 = (i4 + 1);

            then ((G * (i3,j3)) `2 ) <> ( N-bound ( L~ f)) by A1, A48, A49, A50, A51, A52, Th17;

            then ((G * (1,j3)) `2 ) <> ( N-bound ( L~ f)) by A58, A61, A60, GOBOARD5: 1;

            then (( N-min ( L~ f)) `2 ) <> ( N-bound ( L~ f)) by A4, A6, A13, A22, A18, A59, A64, GOBOARD5: 1;

            hence contradiction by EUCLID: 52;

          end;

            suppose

             A65: j3 = j4 & (i3 + 1) = i4;

            ((G * (i3,j3)) `2 ) = ((G * (1,j3)) `2 ) by A58, A61, A60, GOBOARD5: 1

            .= (( N-min ( L~ f)) `2 ) by A4, A6, A13, A22, A18, A59, A65, GOBOARD5: 1

            .= ( N-bound ( L~ f)) by EUCLID: 52;

            then (G * (i3,j3)) in ( N-most ( L~ f)) by A15, A50, A56, GOBOARD1: 1, SPRECT_2: 10;

            then ((G * (i4,j4)) `1 ) <= ((G * (i3,j3)) `1 ) by A4, A46, A54, A52, PSCOMP_1: 39;

            then i3 >= (i3 + 1) by A22, A18, A55, A59, A58, A65, GOBOARD5: 3;

            hence contradiction by NAT_1: 13;

          end;

        end;

        

         A66: (k9 + 1) = k1;

        now

          per cases by A53, A62;

            suppose (j4 + 1) = j3;

            then j4 >= (j4 + 1) by A13, A22, A55, A59, A60, A57, A62, GOBOARD5: 4;

            hence contradiction by NAT_1: 13;

          end;

            suppose

             A67: j4 = (j3 + 1);

            (( len f) - 1) >= 0 by A47, XREAL_1: 19;

            then (( len f) -' 1) = (( len f) - 1) by XREAL_0:def 2;

            

            then

             A68: (( LSeg (f,k)) /\ ( LSeg (f,k9))) = {(f . k)} by A46, JORDAN4: 42

            .= {(f /. k)} by A20, PARTFUN1:def 6;

            (f /. k9) in ( LSeg (f,k9)) & (f /. (k + 1)) in ( LSeg (f,k)) by A2, A3, A48, A66, TOPREAL1: 21;

            then (f /. (k + 1)) in {(f /. k)} by A8, A46, A50, A55, A59, A62, A67, A68, XBOOLE_0:def 4;

            then

             A69: (f /. (k + 1)) = (f /. k) by TARSKI:def 1;

            j1 <> j2 by A46;

            hence contradiction by A5, A6, A7, A8, A69, GOBOARD1: 5;

          end;

        end;

        hence thesis;

      end;

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

        then j1 >= (j1 + 1) by A13, A22, A11, A17, GOBOARD5: 4;

        hence thesis by NAT_1: 13;

      end;

        suppose

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

        ((G * (i2,j2)) `2 ) = ((G * (1,j2)) `2 ) by A12, A21, A11, GOBOARD5: 1

        .= ( N-bound ( L~ f)) by A13, A22, A18, A10, A70, GOBOARD5: 1;

        then (G * (i2,j2)) in ( N-most ( L~ f)) by A8, A15, A16, GOBOARD1: 1, SPRECT_2: 10;

        then ((G * (i1,j1)) `1 ) <= ((G * (i2,j2)) `1 ) by A4, A6, PSCOMP_1: 39;

        then i2 >= (i2 + 1) by A22, A18, A12, A70, GOBOARD5: 3;

        hence thesis by NAT_1: 13;

      end;

    end;

    theorem :: JORDAN1I:23

    

     Th23: for f be clockwise_oriented non constant standard special_circular_sequence holds for G be Go-board holds for k be Nat st f is_sequence_on G & 1 <= k & (k + 1) <= ( len f) & (f /. k) = ( E-max ( L~ f)) holds ex i,j be Nat st [i, (j + 1)] in ( Indices G) & [i, j] in ( Indices G) & (f /. k) = (G * (i,(j + 1))) & (f /. (k + 1)) = (G * (i,j))

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      let G be Go-board;

      let k be Nat;

      assume that

       A1: f is_sequence_on G and

       A2: 1 <= k and

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

       A4: (f /. k) = ( E-max ( L~ f));

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

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

       A6: (f /. k) = (G * (i1,j1)) and

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

       A8: (f /. (k + 1)) = (G * (i2,j2)) and

       A9: 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, A2, A3, JORDAN8: 3;

      

       A10: ((G * (i1,j1)) `1 ) = ( E-bound ( L~ f)) by A4, A6, EUCLID: 52;

      

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

      take i2, j2;

      

       A12: i1 <= ( len G) by A5, MATRIX_0: 32;

      

       A13: (k + 1) >= (1 + 1) by A2, XREAL_1: 7;

      then

       A14: ( len f) >= 2 by A3, XXREAL_0: 2;

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

      then

       A15: (k + 1) in ( dom f) by A3, FINSEQ_3: 25;

      then (f /. (k + 1)) in ( L~ f) by A3, A13, GOBOARD1: 1, XXREAL_0: 2;

      then

       A16: ((G * (i1,j1)) `1 ) >= ((G * (i2,j2)) `1 ) by A8, A10, PSCOMP_1: 24;

      

       A17: 1 <= i1 & 1 <= j1 by A5, MATRIX_0: 32;

      

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

      then

       A19: k in ( dom f) by A2, FINSEQ_3: 25;

      

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

      

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

      

       A22: 1 <= i2 & 1 <= j2 by A7, MATRIX_0: 32;

      now

        per cases by A9;

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

          hence [i2, j2] in ( Indices G) & [i2, (j2 + 1)] in ( Indices G) & (f /. k) = (G * (i2,(j2 + 1))) by A5, A6, A7;

        end;

          suppose

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

          reconsider k9 = (k - 1) as Nat by A19, FINSEQ_3: 26;

          k > 1 by A2, A23, XXREAL_0: 1;

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

          then

           A24: k9 >= ((1 + 1) - 1) by XREAL_1: 9;

          then

          consider i3,j3,i4,j4 be Nat such that

           A25: [i3, j3] in ( Indices G) and

           A26: (f /. k9) = (G * (i3,j3)) and

           A27: [i4, j4] in ( Indices G) and

           A28: (f /. (k9 + 1)) = (G * (i4,j4)) and

           A29: i3 = i4 & (j3 + 1) = j4 or (i3 + 1) = i4 & j3 = j4 or i3 = (i4 + 1) & j3 = j4 or i3 = i4 & j3 = (j4 + 1) by A1, A18, JORDAN8: 3;

          

           A30: i1 = i4 by A5, A6, A27, A28, GOBOARD1: 5;

          (k9 + 1) < ( len f) by A3, NAT_1: 13;

          then k9 < ( len f) by NAT_1: 13;

          then

           A31: k9 in ( dom f) by A24, FINSEQ_3: 25;

          

           A32: i3 <= ( len G) by A25, MATRIX_0: 32;

          

           A33: j1 = j4 by A5, A6, A27, A28, GOBOARD1: 5;

          

           A34: j3 <= ( width G) by A25, MATRIX_0: 32;

          

           A35: 1 <= i3 & 1 <= j3 by A25, MATRIX_0: 32;

          

           A36: j3 = j4

          proof

            assume

             A37: j3 <> j4;

            per cases by A29, A37;

              suppose

               A38: i3 = i4 & j4 = (j3 + 1);

              then ((G * (i3,j3)) `1 ) <> ( E-bound ( L~ f)) by A1, A18, A24, A25, A26, A27, A28, Th18;

              then ((G * (i3,1)) `1 ) <> ( E-bound ( L~ f)) by A32, A35, A34, GOBOARD5: 2;

              then (( E-max ( L~ f)) `1 ) <> ( E-bound ( L~ f)) by A4, A6, A12, A17, A21, A30, A38, GOBOARD5: 2;

              hence contradiction by EUCLID: 52;

            end;

              suppose

               A39: i3 = i4 & (j4 + 1) = j3;

              ((G * (i3,j3)) `1 ) = ((G * (i3,1)) `1 ) by A32, A35, A34, GOBOARD5: 2

              .= (( E-max ( L~ f)) `1 ) by A4, A6, A12, A17, A21, A30, A39, GOBOARD5: 2

              .= ( E-bound ( L~ f)) by EUCLID: 52;

              then (G * (i3,j3)) in ( E-most ( L~ f)) by A14, A26, A31, GOBOARD1: 1, SPRECT_2: 13;

              then ((G * (i4,j4)) `2 ) >= ((G * (i3,j3)) `2 ) by A4, A28, PSCOMP_1: 47;

              then j4 >= (j4 + 1) by A12, A17, A30, A33, A34, A39, GOBOARD5: 4;

              hence contradiction by NAT_1: 13;

            end;

          end;

          

           A40: (k9 + 1) = k;

          (f /. k9) in ( L~ f) by A3, A13, A31, GOBOARD1: 1, XXREAL_0: 2;

          then

           A41: ((G * (i1,j1)) `1 ) >= ((G * (i3,j3)) `1 ) by A10, A26, PSCOMP_1: 24;

          now

            per cases by A29, A36;

              suppose (i4 + 1) = i3;

              then i4 >= (i4 + 1) by A17, A21, A30, A33, A32, A41, A36, GOBOARD5: 3;

              hence contradiction by NAT_1: 13;

            end;

              suppose

               A42: i4 = (i3 + 1);

              (k9 + (1 + 1)) <= ( len f) by A3;

              then

               A43: (( LSeg (f,k9)) /\ ( LSeg (f,k))) = {(f /. k)} by A24, A40, TOPREAL1:def 6;

              (f /. k9) in ( LSeg (f,k9)) & (f /. (k + 1)) in ( LSeg (f,k)) by A2, A3, A18, A24, A40, TOPREAL1: 21;

              then (f /. (k + 1)) in {(f /. k)} by A8, A23, A26, A30, A33, A36, A42, A43, XBOOLE_0:def 4;

              then

               A44: (f /. (k + 1)) = (f /. k) by TARSKI:def 1;

              i1 <> i2 by A23;

              hence contradiction by A5, A6, A7, A8, A44, GOBOARD1: 5;

            end;

          end;

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

        end;

          suppose

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

          set k1 = ( len f);

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

          then

           A46: ( len f) > (1 + 0 ) by A2, XXREAL_0: 2;

          then ( len f) in ( dom f) by FINSEQ_3: 25;

          then

          reconsider k9 = (( len f) - 1) as Nat by FINSEQ_3: 26;

          (k + 1) >= (1 + 1) by A2, XREAL_1: 7;

          then ( len f) >= (1 + 1) by A3, XXREAL_0: 2;

          then

           A47: k9 >= ((1 + 1) - 1) by XREAL_1: 9;

          then

          consider i3,j3,i4,j4 be Nat such that

           A48: [i3, j3] in ( Indices G) and

           A49: (f /. k9) = (G * (i3,j3)) and

           A50: [i4, j4] in ( Indices G) and

           A51: (f /. (k9 + 1)) = (G * (i4,j4)) and

           A52: i3 = i4 & (j3 + 1) = j4 or (i3 + 1) = i4 & j3 = j4 or i3 = (i4 + 1) & j3 = j4 or i3 = i4 & j3 = (j4 + 1) by A1, JORDAN8: 3;

          

           A53: (f /. k1) = (f /. 1) by FINSEQ_6:def 1;

          then

           A54: i1 = i4 by A5, A6, A45, A50, A51, GOBOARD1: 5;

          

           A55: j1 = j4 by A5, A6, A45, A53, A50, A51, GOBOARD1: 5;

          

           A56: j3 <= ( width G) by A48, MATRIX_0: 32;

          (k9 + 1) <= ( len f);

          then k9 < ( len f) by NAT_1: 13;

          then

           A57: k9 in ( dom f) by A47, FINSEQ_3: 25;

          then (f /. k9) in ( L~ f) by A3, A13, GOBOARD1: 1, XXREAL_0: 2;

          then

           A58: ((G * (i1,j1)) `1 ) >= ((G * (i3,j3)) `1 ) by A10, A49, PSCOMP_1: 24;

          

           A59: i3 <= ( len G) by A48, MATRIX_0: 32;

          

           A60: 1 <= i3 & 1 <= j3 by A48, MATRIX_0: 32;

          

           A61: j3 = j4

          proof

            assume

             A62: j3 <> j4;

            per cases by A52, A62;

              suppose

               A63: i3 = i4 & j4 = (j3 + 1);

              then ((G * (i3,j3)) `1 ) <> ( E-bound ( L~ f)) by A1, A47, A48, A49, A50, A51, Th18;

              then ((G * (i3,1)) `1 ) <> ( E-bound ( L~ f)) by A59, A60, A56, GOBOARD5: 2;

              then (( E-max ( L~ f)) `1 ) <> ( E-bound ( L~ f)) by A4, A6, A12, A17, A21, A54, A63, GOBOARD5: 2;

              hence contradiction by EUCLID: 52;

            end;

              suppose

               A64: i3 = i4 & (j4 + 1) = j3;

              ((G * (i3,j3)) `1 ) = ((G * (i3,1)) `1 ) by A59, A60, A56, GOBOARD5: 2

              .= (( E-max ( L~ f)) `1 ) by A4, A6, A12, A17, A21, A54, A64, GOBOARD5: 2

              .= ( E-bound ( L~ f)) by EUCLID: 52;

              then (G * (i3,j3)) in ( E-most ( L~ f)) by A14, A49, A57, GOBOARD1: 1, SPRECT_2: 13;

              then ((G * (i4,j4)) `2 ) >= ((G * (i3,j3)) `2 ) by A4, A45, A53, A51, PSCOMP_1: 47;

              then j4 >= (j4 + 1) by A12, A17, A54, A55, A56, A64, GOBOARD5: 4;

              hence contradiction by NAT_1: 13;

            end;

          end;

          

           A65: (k9 + 1) = k1;

          now

            per cases by A52, A61;

              suppose (i4 + 1) = i3;

              then i4 >= (i4 + 1) by A17, A21, A54, A55, A59, A58, A61, GOBOARD5: 3;

              hence contradiction by NAT_1: 13;

            end;

              suppose

               A66: i4 = (i3 + 1);

              (( len f) - 1) >= 0 by A46, XREAL_1: 19;

              then (( len f) -' 1) = (( len f) - 1) by XREAL_0:def 2;

              

              then

               A67: (( LSeg (f,k)) /\ ( LSeg (f,k9))) = {(f . k)} by A45, JORDAN4: 42

              .= {(f /. k)} by A19, PARTFUN1:def 6;

              (f /. k9) in ( LSeg (f,k9)) & (f /. (k + 1)) in ( LSeg (f,k)) by A2, A3, A47, A65, TOPREAL1: 21;

              then (f /. (k + 1)) in {(f /. k)} by A8, A45, A49, A54, A55, A61, A66, A67, XBOOLE_0:def 4;

              then

               A68: (f /. (k + 1)) = (f /. k) by TARSKI:def 1;

              i1 <> i2 by A45;

              hence contradiction by A5, A6, A7, A8, A68, GOBOARD1: 5;

            end;

          end;

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

        end;

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

          then i1 >= (i1 + 1) by A17, A21, A20, A16, GOBOARD5: 3;

          hence [i2, j2] in ( Indices G) & [i2, (j2 + 1)] in ( Indices G) & (f /. k) = (G * (i2,(j2 + 1))) by NAT_1: 13;

        end;

          suppose

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

          ((G * (i2,j2)) `1 ) = ((G * (i2,1)) `1 ) by A20, A22, A11, GOBOARD5: 2

          .= ( E-bound ( L~ f)) by A12, A17, A21, A10, A69, GOBOARD5: 2;

          then (G * (i2,j2)) in ( E-most ( L~ f)) by A8, A14, A15, GOBOARD1: 1, SPRECT_2: 13;

          then ((G * (i1,j1)) `2 ) >= ((G * (i2,j2)) `2 ) by A4, A6, PSCOMP_1: 47;

          then j1 >= (j1 + 1) by A12, A17, A11, A69, GOBOARD5: 4;

          hence [i2, j2] in ( Indices G) & [i2, (j2 + 1)] in ( Indices G) & (f /. k) = (G * (i2,(j2 + 1))) by NAT_1: 13;

        end;

      end;

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

      thus thesis by A8;

    end;

    theorem :: JORDAN1I:24

    

     Th24: for f be clockwise_oriented non constant standard special_circular_sequence holds for G be Go-board holds for k be Nat st f is_sequence_on G & 1 <= k & (k + 1) <= ( len f) & (f /. k) = ( S-max ( L~ f)) holds ex i,j be Nat st [(i + 1), j] in ( Indices G) & [i, j] in ( Indices G) & (f /. k) = (G * ((i + 1),j)) & (f /. (k + 1)) = (G * (i,j))

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      let G be Go-board;

      let k be Nat;

      assume that

       A1: f is_sequence_on G and

       A2: 1 <= k and

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

       A4: (f /. k) = ( S-max ( L~ f));

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

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

       A6: (f /. k) = (G * (i1,j1)) and

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

       A8: (f /. (k + 1)) = (G * (i2,j2)) and

       A9: 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, A2, A3, JORDAN8: 3;

      

       A10: ((G * (i1,j1)) `2 ) = ( S-bound ( L~ f)) by A4, A6, EUCLID: 52;

      

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

      take i2, j2;

      

       A12: i1 <= ( len G) by A5, MATRIX_0: 32;

      

       A13: (k + 1) >= (1 + 1) by A2, XREAL_1: 7;

      then

       A14: ( len f) >= 2 by A3, XXREAL_0: 2;

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

      then

       A15: (k + 1) in ( dom f) by A3, FINSEQ_3: 25;

      then (f /. (k + 1)) in ( L~ f) by A3, A13, GOBOARD1: 1, XXREAL_0: 2;

      then

       A16: ((G * (i1,j1)) `2 ) <= ((G * (i2,j2)) `2 ) by A8, A10, PSCOMP_1: 24;

      

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

      

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

      then

       A19: k in ( dom f) by A2, FINSEQ_3: 25;

      

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

      

       A21: 1 <= i1 & j1 <= ( width G) by A5, MATRIX_0: 32;

      

       A22: 1 <= i2 & j2 <= ( width G) by A7, MATRIX_0: 32;

      now

        per cases by A9;

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

          hence [(i2 + 1), j2] in ( Indices G) & [i2, j2] in ( Indices G) & (f /. k) = (G * ((i2 + 1),j2)) by A5, A6, A7;

        end;

          suppose

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

          reconsider k9 = (k - 1) as Nat by A19, FINSEQ_3: 26;

          k > 1 by A2, A23, XXREAL_0: 1;

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

          then

           A24: k9 >= ((1 + 1) - 1) by XREAL_1: 9;

          then

          consider i3,j3,i4,j4 be Nat such that

           A25: [i3, j3] in ( Indices G) and

           A26: (f /. k9) = (G * (i3,j3)) and

           A27: [i4, j4] in ( Indices G) and

           A28: (f /. (k9 + 1)) = (G * (i4,j4)) and

           A29: i3 = i4 & (j3 + 1) = j4 or (i3 + 1) = i4 & j3 = j4 or i3 = (i4 + 1) & j3 = j4 or i3 = i4 & j3 = (j4 + 1) by A1, A18, JORDAN8: 3;

          

           A30: i1 = i4 by A5, A6, A27, A28, GOBOARD1: 5;

          (k9 + 1) < ( len f) by A3, NAT_1: 13;

          then k9 < ( len f) by NAT_1: 13;

          then

           A31: k9 in ( dom f) by A24, FINSEQ_3: 25;

          

           A32: i3 <= ( len G) by A25, MATRIX_0: 32;

          

           A33: 1 <= j3 by A25, MATRIX_0: 32;

          

           A34: j1 = j4 by A5, A6, A27, A28, GOBOARD1: 5;

          

           A35: 1 <= i3 & j3 <= ( width G) by A25, MATRIX_0: 32;

          

           A36: i3 = i4

          proof

            assume

             A37: i3 <> i4;

            per cases by A29, A37;

              suppose

               A38: j3 = j4 & i4 = (i3 + 1);

              then ((G * (i3,j3)) `2 ) <> ( S-bound ( L~ f)) by A1, A18, A24, A25, A26, A27, A28, Th19;

              then ((G * (1,j3)) `2 ) <> ( S-bound ( L~ f)) by A32, A33, A35, GOBOARD5: 1;

              then (( S-max ( L~ f)) `2 ) <> ( S-bound ( L~ f)) by A4, A6, A12, A17, A21, A34, A38, GOBOARD5: 1;

              hence contradiction by EUCLID: 52;

            end;

              suppose

               A39: j3 = j4 & (i4 + 1) = i3;

              ((G * (i3,j3)) `2 ) = ((G * (1,j3)) `2 ) by A32, A33, A35, GOBOARD5: 1

              .= (( S-max ( L~ f)) `2 ) by A4, A6, A12, A17, A21, A34, A39, GOBOARD5: 1

              .= ( S-bound ( L~ f)) by EUCLID: 52;

              then (G * (i3,j3)) in ( S-most ( L~ f)) by A14, A26, A31, GOBOARD1: 1, SPRECT_2: 11;

              then ((G * (i4,j4)) `1 ) >= ((G * (i3,j3)) `1 ) by A4, A28, PSCOMP_1: 55;

              then i4 >= (i4 + 1) by A17, A21, A30, A34, A32, A39, GOBOARD5: 3;

              hence contradiction by NAT_1: 13;

            end;

          end;

          

           A40: (k9 + 1) = k;

          (f /. k9) in ( L~ f) by A3, A13, A31, GOBOARD1: 1, XXREAL_0: 2;

          then

           A41: ((G * (i1,j1)) `2 ) <= ((G * (i3,j3)) `2 ) by A10, A26, PSCOMP_1: 24;

          now

            per cases by A29, A36;

              suppose (j3 + 1) = j4;

              then j3 >= (j3 + 1) by A12, A21, A30, A34, A33, A41, A36, GOBOARD5: 4;

              hence contradiction by NAT_1: 13;

            end;

              suppose

               A42: j3 = (j4 + 1);

              (k9 + (1 + 1)) <= ( len f) by A3;

              then

               A43: (( LSeg (f,k9)) /\ ( LSeg (f,k))) = {(f /. k)} by A24, A40, TOPREAL1:def 6;

              (f /. k9) in ( LSeg (f,k9)) & (f /. (k + 1)) in ( LSeg (f,k)) by A2, A3, A18, A24, A40, TOPREAL1: 21;

              then (f /. (k + 1)) in {(f /. k)} by A8, A23, A26, A30, A34, A36, A42, A43, XBOOLE_0:def 4;

              then

               A44: (f /. (k + 1)) = (f /. k) by TARSKI:def 1;

              j1 <> j2 by A23;

              hence contradiction by A5, A6, A7, A8, A44, GOBOARD1: 5;

            end;

          end;

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

        end;

          suppose

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

          set k1 = ( len f);

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

          then

           A46: ( len f) > (1 + 0 ) by A2, XXREAL_0: 2;

          then ( len f) in ( dom f) by FINSEQ_3: 25;

          then

          reconsider k9 = (( len f) - 1) as Nat by FINSEQ_3: 26;

          (k + 1) >= (1 + 1) by A2, XREAL_1: 7;

          then ( len f) >= (1 + 1) by A3, XXREAL_0: 2;

          then

           A47: k9 >= ((1 + 1) - 1) by XREAL_1: 9;

          then

          consider i3,j3,i4,j4 be Nat such that

           A48: [i3, j3] in ( Indices G) and

           A49: (f /. k9) = (G * (i3,j3)) and

           A50: [i4, j4] in ( Indices G) and

           A51: (f /. (k9 + 1)) = (G * (i4,j4)) and

           A52: i3 = i4 & (j3 + 1) = j4 or (i3 + 1) = i4 & j3 = j4 or i3 = (i4 + 1) & j3 = j4 or i3 = i4 & j3 = (j4 + 1) by A1, JORDAN8: 3;

          

           A53: (f /. k1) = (f /. 1) by FINSEQ_6:def 1;

          then

           A54: i1 = i4 by A5, A6, A45, A50, A51, GOBOARD1: 5;

          (k9 + 1) <= ( len f);

          then k9 < ( len f) by NAT_1: 13;

          then

           A55: k9 in ( dom f) by A47, FINSEQ_3: 25;

          then (f /. k9) in ( L~ f) by A3, A13, GOBOARD1: 1, XXREAL_0: 2;

          then

           A56: ((G * (i1,j1)) `2 ) <= ((G * (i3,j3)) `2 ) by A10, A49, PSCOMP_1: 24;

          

           A57: i3 <= ( len G) by A48, MATRIX_0: 32;

          

           A58: j1 = j4 by A5, A6, A45, A53, A50, A51, GOBOARD1: 5;

          

           A59: 1 <= j3 by A48, MATRIX_0: 32;

          

           A60: 1 <= i3 & j3 <= ( width G) by A48, MATRIX_0: 32;

          

           A61: i3 = i4

          proof

            assume

             A62: i3 <> i4;

            per cases by A52, A62;

              suppose

               A63: j3 = j4 & i4 = (i3 + 1);

              then ((G * (i3,j3)) `2 ) <> ( S-bound ( L~ f)) by A1, A47, A48, A49, A50, A51, Th19;

              then ((G * (1,j3)) `2 ) <> ( S-bound ( L~ f)) by A57, A59, A60, GOBOARD5: 1;

              then (( S-max ( L~ f)) `2 ) <> ( S-bound ( L~ f)) by A4, A6, A12, A17, A21, A58, A63, GOBOARD5: 1;

              hence contradiction by EUCLID: 52;

            end;

              suppose

               A64: j3 = j4 & (i4 + 1) = i3;

              ((G * (i3,j3)) `2 ) = ((G * (1,j3)) `2 ) by A57, A59, A60, GOBOARD5: 1

              .= (( S-max ( L~ f)) `2 ) by A4, A6, A12, A17, A21, A58, A64, GOBOARD5: 1

              .= ( S-bound ( L~ f)) by EUCLID: 52;

              then (G * (i3,j3)) in ( S-most ( L~ f)) by A14, A49, A55, GOBOARD1: 1, SPRECT_2: 11;

              then ((G * (i4,j4)) `1 ) >= ((G * (i3,j3)) `1 ) by A4, A45, A53, A51, PSCOMP_1: 55;

              then i4 >= (i4 + 1) by A17, A21, A54, A58, A57, A64, GOBOARD5: 3;

              hence contradiction by NAT_1: 13;

            end;

          end;

          

           A65: (k9 + 1) = k1;

          now

            per cases by A52, A61;

              suppose (j3 + 1) = j4;

              then j3 >= (j3 + 1) by A12, A21, A54, A58, A59, A56, A61, GOBOARD5: 4;

              hence contradiction by NAT_1: 13;

            end;

              suppose

               A66: j3 = (j4 + 1);

              (( len f) - 1) >= 0 by A46, XREAL_1: 19;

              then (( len f) -' 1) = (( len f) - 1) by XREAL_0:def 2;

              

              then

               A67: (( LSeg (f,k)) /\ ( LSeg (f,k9))) = {(f . k)} by A45, JORDAN4: 42

              .= {(f /. k)} by A19, PARTFUN1:def 6;

              (f /. k9) in ( LSeg (f,k9)) & (f /. (k + 1)) in ( LSeg (f,k)) by A2, A3, A47, A65, TOPREAL1: 21;

              then (f /. (k + 1)) in {(f /. k)} by A8, A45, A49, A54, A58, A61, A66, A67, XBOOLE_0:def 4;

              then

               A68: (f /. (k + 1)) = (f /. k) by TARSKI:def 1;

              j1 <> j2 by A45;

              hence contradiction by A5, A6, A7, A8, A68, GOBOARD1: 5;

            end;

          end;

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

        end;

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

          then j2 >= (j2 + 1) by A12, A21, A11, A16, GOBOARD5: 4;

          hence [(i2 + 1), j2] in ( Indices G) & [i2, j2] in ( Indices G) & (f /. k) = (G * ((i2 + 1),j2)) by NAT_1: 13;

        end;

          suppose

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

          ((G * (i2,j2)) `2 ) = ((G * (1,j2)) `2 ) by A20, A11, A22, GOBOARD5: 1

          .= ( S-bound ( L~ f)) by A12, A17, A21, A10, A69, GOBOARD5: 1;

          then (G * (i2,j2)) in ( S-most ( L~ f)) by A8, A14, A15, GOBOARD1: 1, SPRECT_2: 11;

          then ((G * (i1,j1)) `1 ) >= ((G * (i2,j2)) `1 ) by A4, A6, PSCOMP_1: 55;

          then i1 >= (i1 + 1) by A17, A21, A20, A69, GOBOARD5: 3;

          hence [(i2 + 1), j2] in ( Indices G) & [i2, j2] in ( Indices G) & (f /. k) = (G * ((i2 + 1),j2)) by NAT_1: 13;

        end;

      end;

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

      thus thesis by A8;

    end;

    theorem :: JORDAN1I:25

    for f be non constant standard special_circular_sequence holds f is clockwise_oriented iff (( Rotate (f,( W-min ( L~ f)))) /. 2) in ( W-most ( L~ f))

    proof

      set i = 1;

      let f be non constant standard special_circular_sequence;

      set r = ( Rotate (f,( W-min ( L~ f))));

      

       A1: r is_sequence_on ( GoB r) by GOBOARD5:def 5;

      

       A2: (1 + 1) <= ( len r) by TOPREAL8: 3;

      then

       A3: ( Int ( left_cell (r,1))) c= ( LeftComp r) by GOBOARD9: 21;

      set j = ( i_s_w r);

      

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

      then

       A5: (r /. 1) = ( W-min ( L~ f)) by FINSEQ_6: 92;

      

       A6: 2 <= ( len f) by TOPREAL8: 3;

      thus f is clockwise_oriented implies (r /. 2) in ( W-most ( L~ f))

      proof

        set k = (( W-min ( L~ f)) .. f);

        k < ( len f) by SPRECT_5: 20;

        then

         A7: (k + 1) <= ( len f) by NAT_1: 13;

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

        then

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

        then (f /. (k + 1)) = (f . (k + 1)) by PARTFUN1:def 6;

        then

         A9: (f /. (k + 1)) in ( rng f) by A8, FUNCT_1: 3;

        

         A10: ( rng f) c= ( L~ f) by A6, SPPOL_2: 18;

        

         A11: (f /. k) = ( W-min ( L~ f)) by A4, FINSEQ_5: 38;

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

        

        then

         A12: (f /. (k + 1)) = (r /. (((k + 1) + 1) -' k)) by A4, A7, FINSEQ_6: 175

        .= (r /. ((k + (1 + 1)) -' k))

        .= (r /. 2) by NAT_D: 34;

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

        then

         A13: f is_sequence_on ( GoB r) by REVROT_1: 28;

        assume f is clockwise_oriented;

        then

        consider i,j be Nat such that

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

         A15: [i, (j + 1)] in ( Indices ( GoB r)) and

         A16: (f /. k) = (( GoB r) * (i,j)) and

         A17: (f /. (k + 1)) = (( GoB r) * (i,(j + 1))) by A4, A7, A11, A13, Th21, FINSEQ_4: 21;

        

         A18: 1 <= i & i <= ( len ( GoB r)) by A14, MATRIX_0: 32;

        

         A19: 1 <= (j + 1) & (j + 1) <= ( width ( GoB r)) by A15, MATRIX_0: 32;

        

         A20: 1 <= j & j <= ( width ( GoB r)) by A14, MATRIX_0: 32;

        1 <= i & i <= ( len ( GoB r)) by A14, MATRIX_0: 32;

        

        then ((f /. (k + 1)) `1 ) = ((( GoB r) * (i,1)) `1 ) by A17, A19, GOBOARD5: 2

        .= ((f /. k) `1 ) by A16, A18, A20, GOBOARD5: 2

        .= ( W-bound ( L~ f)) by A11, EUCLID: 52;

        hence thesis by A12, A9, A10, SPRECT_2: 12;

      end;

      

       A21: [i, j] in ( Indices ( GoB r)) by JORDAN5D:def 1;

      then

       A22: i <= ( len ( GoB r)) & j <= ( width ( GoB r)) by MATRIX_0: 32;

      ( len r) > 2 by TOPREAL8: 3;

      then

       A23: (1 + 1) in ( dom r) by FINSEQ_3: 25;

      then

      consider i2,j2 be Nat such that

       A24: [i2, j2] in ( Indices ( GoB r)) and

       A25: (r /. (1 + 1)) = (( GoB r) * (i2,j2)) by A1, GOBOARD1:def 9;

      

       A26: 1 <= j2 by A24, MATRIX_0: 32;

      

       A27: ( L~ r) = ( L~ f) by REVROT_1: 33;

      then

       A28: (( GoB r) * (i,j)) = (r /. 1) by A5, JORDAN5D:def 1;

      assume

       A29: (r /. 2) in ( W-most ( L~ f));

      then ((( GoB r) * (i2,j2)) `1 ) = ((( GoB r) * (1,j)) `1 ) by A5, A28, A25, PSCOMP_1: 31;

      then

       A30: i2 = 1 by A21, A24, JORDAN1G: 7;

      ( rng r) = ( rng f) by FINSEQ_6: 90, SPRECT_2: 43;

      then 1 in ( dom r) by FINSEQ_3: 31, SPRECT_2: 43;

      then ( |.(1 - 1).| + |.(j - j2).|) = 1 by A1, A21, A28, A23, A24, A25, A30, GOBOARD1:def 9;

      then ( 0 + |.(j - j2).|) = 1 by ABSVALUE: 2;

      then

       A31: |.(j2 - j).| = 1 by UNIFORM1: 11;

      ((( GoB r) * (1,j)) `2 ) <= ((( GoB r) * (i2,j2)) `2 ) by A5, A28, A29, A25, PSCOMP_1: 31;

      then (j2 - j) >= 0 by A22, A30, A26, GOBOARD5: 4, XREAL_1: 48;

      then

       A32: (j2 - j) = 1 by A31, ABSVALUE:def 1;

      then j2 = (j + 1);

      then (i -' 1) = (1 - 1) & ( left_cell (r,1,( GoB r))) = ( cell (( GoB r),(i -' 1),j)) by A2, A1, A21, A28, A24, A25, A30, GOBRD13: 21, XREAL_1: 233;

      then

       A33: ( left_cell (r,1)) = ( cell (( GoB r), 0 ,j)) by A2, JORDAN1H: 21;

      ( Int ( left_cell (r,1))) <> {} by A2, GOBOARD9: 15;

      then

      consider p be object such that

       A34: p in ( Int ( left_cell (r,1))) by XBOOLE_0:def 1;

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

      

       A35: ( LeftComp r) is_a_component_of (( L~ r) ` ) & ( UBD ( L~ r)) is_a_component_of (( L~ r) ` ) by GOBOARD9:def 1, JORDAN2C: 124;

      

       A36: 1 <= j by A21, MATRIX_0: 32;

      (j + 1) <= ( width ( GoB r)) by A24, A32, MATRIX_0: 32;

      then j < ( width ( GoB r)) by NAT_1: 13;

      then ( Int ( left_cell (r,1))) = { |[t, s]| where t,s be Real : t < ((( GoB r) * (1,1)) `1 ) & ((( GoB r) * (1,j)) `2 ) < s & s < ((( GoB r) * (1,(j + 1))) `2 ) } by A36, A33, GOBOARD6: 20;

      then

      consider t,s be Real such that

       A37: p = |[t, s]| and

       A38: t < ((( GoB r) * (1,1)) `1 ) and ((( GoB r) * (1,j)) `2 ) < s and s < ((( GoB r) * (1,(j + 1))) `2 ) by A34;

      now

        

         A39: ((( GoB r) * (1,j)) `1 ) = ((( GoB r) * (1,1)) `1 ) by A36, A22, GOBOARD5: 2;

        assume ( west_halfline p) meets ( L~ r);

        then (( west_halfline p) /\ ( L~ r)) <> {} by XBOOLE_0:def 7;

        then

        consider a be object such that

         A40: a in (( west_halfline p) /\ ( L~ r)) by XBOOLE_0:def 1;

        

         A41: a in ( L~ r) by A40, XBOOLE_0:def 4;

        

         A42: a in ( west_halfline p) by A40, XBOOLE_0:def 4;

        reconsider a as Point of ( TOP-REAL 2) by A40;

        (a `1 ) <= (p `1 ) by A42, TOPREAL1:def 13;

        then (a `1 ) <= t by A37, EUCLID: 52;

        then (a `1 ) < ((( GoB r) * (i,j)) `1 ) by A38, A39, XXREAL_0: 2;

        then (a `1 ) < ( W-bound ( L~ r)) by A27, A5, A28, EUCLID: 52;

        hence contradiction by A41, PSCOMP_1: 24;

      end;

      then

       A43: ( west_halfline p) c= ( UBD ( L~ r)) by JORDAN2C: 126;

      p in ( west_halfline p) by TOPREAL1: 38;

      then ( LeftComp r) meets ( UBD ( L~ r)) by A3, A34, A43, XBOOLE_0: 3;

      then r is clockwise_oriented by A35, GOBOARD9: 1, JORDAN1H: 41;

      hence thesis by JORDAN1H: 40;

    end;

    theorem :: JORDAN1I:26

    for f be non constant standard special_circular_sequence holds f is clockwise_oriented iff (( Rotate (f,( E-max ( L~ f)))) /. 2) in ( E-most ( L~ f))

    proof

      let f be non constant standard special_circular_sequence;

      set r = ( Rotate (f,( E-max ( L~ f))));

      set j = ( i_n_e r);

      set i = ( len ( GoB r));

      

       A1: (1 + 1) <= ( len r) & r is_sequence_on ( GoB r) by GOBOARD5:def 5, TOPREAL8: 3;

      

       A2: ( E-max ( L~ f)) in ( rng f) by SPRECT_2: 46;

      then

       A3: (r /. 1) = ( E-max ( L~ f)) by FINSEQ_6: 92;

      

       A4: 2 <= ( len f) by TOPREAL8: 3;

      thus f is clockwise_oriented implies (r /. 2) in ( E-most ( L~ f))

      proof

        set k = (( E-max ( L~ f)) .. f);

        k < ( len f) by SPRECT_5: 16;

        then

         A5: (k + 1) <= ( len f) by NAT_1: 13;

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

        then

         A6: (k + 1) in ( dom f) by A5, FINSEQ_3: 25;

        then (f /. (k + 1)) = (f . (k + 1)) by PARTFUN1:def 6;

        then

         A7: (f /. (k + 1)) in ( rng f) by A6, FUNCT_1: 3;

        

         A8: ( rng f) c= ( L~ f) by A4, SPPOL_2: 18;

        

         A9: (f /. k) = ( E-max ( L~ f)) by A2, FINSEQ_5: 38;

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

        

        then

         A10: (f /. (k + 1)) = (r /. (((k + 1) + 1) -' k)) by A2, A5, FINSEQ_6: 175

        .= (r /. ((k + (1 + 1)) -' k))

        .= (r /. 2) by NAT_D: 34;

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

        then

         A11: f is_sequence_on ( GoB r) by REVROT_1: 28;

        assume f is clockwise_oriented;

        then

        consider i,j be Nat such that

         A12: [i, (j + 1)] in ( Indices ( GoB r)) and

         A13: [i, j] in ( Indices ( GoB r)) and

         A14: (f /. k) = (( GoB r) * (i,(j + 1))) and

         A15: (f /. (k + 1)) = (( GoB r) * (i,j)) by A2, A5, A9, A11, Th23, FINSEQ_4: 21;

        

         A16: 1 <= j & j <= ( width ( GoB r)) by A13, MATRIX_0: 32;

        

         A17: 1 <= (j + 1) & (j + 1) <= ( width ( GoB r)) by A12, MATRIX_0: 32;

        

         A18: 1 <= i & i <= ( len ( GoB r)) by A12, MATRIX_0: 32;

        1 <= i & i <= ( len ( GoB r)) by A12, MATRIX_0: 32;

        

        then ((f /. (k + 1)) `1 ) = ((( GoB r) * (i,1)) `1 ) by A15, A16, GOBOARD5: 2

        .= ((f /. k) `1 ) by A14, A18, A17, GOBOARD5: 2

        .= ( E-bound ( L~ f)) by A9, EUCLID: 52;

        hence thesis by A10, A7, A8, SPRECT_2: 13;

      end;

      assume

       A19: (r /. 2) in ( E-most ( L~ f));

      ( len r) > 2 by TOPREAL8: 3;

      then

       A20: r is_sequence_on ( GoB r) & (1 + 1) in ( dom r) by FINSEQ_3: 25, GOBOARD5:def 5;

      then

      consider i2,j2 be Nat such that

       A21: [i2, j2] in ( Indices ( GoB r)) and

       A22: (r /. (1 + 1)) = (( GoB r) * (i2,j2)) by GOBOARD1:def 9;

      

       A23: j2 <= ( width ( GoB r)) by A21, MATRIX_0: 32;

      

       A24: [i, j] in ( Indices ( GoB r)) by JORDAN5D:def 4;

      then

       A25: 1 <= j by MATRIX_0: 32;

      then

       A26: [i, ((j -' 1) + 1)] in ( Indices ( GoB r)) by A24, XREAL_1: 235;

      

       A27: ( L~ r) = ( L~ f) by REVROT_1: 33;

      then

       A28: (( GoB r) * (i,j)) = (r /. 1) by A3, JORDAN5D:def 4;

      then

       A29: (r /. 1) = (( GoB r) * (i,((j -' 1) + 1))) by A25, XREAL_1: 235;

      (( GoB r) * (i,j)) in ( E-most ( L~ r)) by A27, A3, A28, PSCOMP_1: 50;

      then ((( GoB r) * (i,j)) `1 ) = (( E-min ( L~ r)) `1 ) by PSCOMP_1: 47;

      then

       A30: ((( GoB r) * (i2,j2)) `1 ) = ((( GoB r) * (i,j)) `1 ) by A27, A19, A22, PSCOMP_1: 47;

      then

       A31: i2 = i by A24, A21, JORDAN1G: 7;

      

       A32: (1 + 1) <= ( len r) by TOPREAL8: 3;

      then

       A33: ( Int ( left_cell (r,1))) c= ( LeftComp r) by GOBOARD9: 21;

      ( Int ( left_cell (r,1))) <> {} by A32, GOBOARD9: 15;

      then

      consider p be object such that

       A34: p in ( Int ( left_cell (r,1))) by XBOOLE_0:def 1;

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

      

       A35: ( LeftComp r) is_a_component_of (( L~ r) ` ) & ( UBD ( L~ r)) is_a_component_of (( L~ r) ` ) by GOBOARD9:def 1, JORDAN2C: 124;

      

       A36: 1 <= j2 by A21, MATRIX_0: 32;

      

       A37: j <= ( width ( GoB r)) by A24, MATRIX_0: 32;

      ( rng r) = ( rng f) by FINSEQ_6: 90, SPRECT_2: 46;

      then 1 in ( dom r) by FINSEQ_3: 31, SPRECT_2: 46;

      then ( |.(i2 - i2).| + |.(j - j2).|) = 1 by A24, A28, A20, A21, A22, A31, GOBOARD1:def 9;

      then

       A38: ( 0 + |.(j - j2).|) = 1 by ABSVALUE: 2;

      

       A39: 1 <= i by A24, MATRIX_0: 32;

      ((( GoB r) * (i,j)) `2 ) >= ((( GoB r) * (i2,j2)) `2 ) by A3, A28, A19, A22, PSCOMP_1: 47;

      then (j - j2) >= 0 by A39, A25, A31, A23, GOBOARD5: 4, XREAL_1: 48;

      then

       A40: (j - j2) = 1 by A38, ABSVALUE:def 1;

      then j2 = (j - 1);

      then

       A41: j2 = (j -' 1) by A25, XREAL_1: 233;

      then [i, (j -' 1)] in ( Indices ( GoB r)) & (r /. (1 + 1)) = (( GoB r) * (i,(j -' 1))) by A24, A21, A22, A30, JORDAN1G: 7;

      then ( left_cell (r,1,( GoB r))) = ( cell (( GoB r),i,(j -' 1))) by A1, A26, A29, GOBRD13: 27;

      then

       A42: ( left_cell (r,1)) = ( cell (( GoB r),i,(j -' 1))) by A32, JORDAN1H: 21;

      (j - 1) < (j - 0 ) by XREAL_1: 15;

      then (j -' 1) < ( width ( GoB r)) by A37, A40, A41, XXREAL_0: 2;

      then ( Int ( left_cell (r,1))) = { |[t, s]| where t,s be Real : ((( GoB r) * (i,1)) `1 ) < t & ((( GoB r) * (1,(j -' 1))) `2 ) < s & s < ((( GoB r) * (1,((j -' 1) + 1))) `2 ) } by A36, A41, A42, GOBOARD6: 23;

      then

      consider t,s be Real such that

       A43: p = |[t, s]| and

       A44: ((( GoB r) * (i,1)) `1 ) < t and ((( GoB r) * (1,(j -' 1))) `2 ) < s and s < ((( GoB r) * (1,((j -' 1) + 1))) `2 ) by A34;

      now

        assume ( east_halfline p) meets ( L~ r);

        then (( east_halfline p) /\ ( L~ r)) <> {} by XBOOLE_0:def 7;

        then

        consider a be object such that

         A45: a in (( east_halfline p) /\ ( L~ r)) by XBOOLE_0:def 1;

        

         A46: a in ( L~ r) by A45, XBOOLE_0:def 4;

        

         A47: a in ( east_halfline p) by A45, XBOOLE_0:def 4;

        reconsider a as Point of ( TOP-REAL 2) by A45;

        (a `1 ) >= (p `1 ) by A47, TOPREAL1:def 11;

        then

         A48: (a `1 ) >= t by A43, EUCLID: 52;

        ((( GoB r) * (i,1)) `1 ) = ((( GoB r) * (i,j)) `1 ) by A39, A25, A37, GOBOARD5: 2;

        then (a `1 ) > ((( GoB r) * (i,j)) `1 ) by A44, A48, XXREAL_0: 2;

        then (a `1 ) > ( E-bound ( L~ r)) by A27, A3, A28, EUCLID: 52;

        hence contradiction by A46, PSCOMP_1: 24;

      end;

      then

       A49: ( east_halfline p) c= ( UBD ( L~ r)) by JORDAN2C: 127;

      p in ( east_halfline p) by TOPREAL1: 38;

      then ( LeftComp r) meets ( UBD ( L~ r)) by A33, A34, A49, XBOOLE_0: 3;

      then r is clockwise_oriented by A35, GOBOARD9: 1, JORDAN1H: 41;

      hence thesis by JORDAN1H: 40;

    end;

    theorem :: JORDAN1I:27

    for f be non constant standard special_circular_sequence holds f is clockwise_oriented iff (( Rotate (f,( S-max ( L~ f)))) /. 2) in ( S-most ( L~ f))

    proof

      set j = 1;

      let f be non constant standard special_circular_sequence;

      set r = ( Rotate (f,( S-max ( L~ f))));

      

       A1: r is_sequence_on ( GoB r) by GOBOARD5:def 5;

      ( len r) > 2 by TOPREAL8: 3;

      then

       A2: (1 + 1) in ( dom r) by FINSEQ_3: 25;

      then

      consider i2,j2 be Nat such that

       A3: [i2, j2] in ( Indices ( GoB r)) and

       A4: (r /. (1 + 1)) = (( GoB r) * (i2,j2)) by A1, GOBOARD1:def 9;

      

       A5: i2 <= ( len ( GoB r)) by A3, MATRIX_0: 32;

      set i = ( i_e_s r);

      

       A6: ( S-max ( L~ f)) in ( rng f) by SPRECT_2: 42;

      then

       A7: (r /. 1) = ( S-max ( L~ f)) by FINSEQ_6: 92;

      

       A8: 2 <= ( len f) by TOPREAL8: 3;

      thus f is clockwise_oriented implies (r /. 2) in ( S-most ( L~ f))

      proof

        set k = (( S-max ( L~ f)) .. f);

        k < ( len f) by SPRECT_5: 14;

        then

         A9: (k + 1) <= ( len f) by NAT_1: 13;

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

        then

         A10: (k + 1) in ( dom f) by A9, FINSEQ_3: 25;

        then (f /. (k + 1)) = (f . (k + 1)) by PARTFUN1:def 6;

        then

         A11: (f /. (k + 1)) in ( rng f) by A10, FUNCT_1: 3;

        

         A12: ( rng f) c= ( L~ f) by A8, SPPOL_2: 18;

        

         A13: (f /. k) = ( S-max ( L~ f)) by A6, FINSEQ_5: 38;

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

        

        then

         A14: (f /. (k + 1)) = (r /. (((k + 1) + 1) -' k)) by A6, A9, FINSEQ_6: 175

        .= (r /. ((k + (1 + 1)) -' k))

        .= (r /. 2) by NAT_D: 34;

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

        then

         A15: f is_sequence_on ( GoB r) by REVROT_1: 28;

        assume f is clockwise_oriented;

        then

        consider i,j be Nat such that

         A16: [(i + 1), j] in ( Indices ( GoB r)) and

         A17: [i, j] in ( Indices ( GoB r)) and

         A18: (f /. k) = (( GoB r) * ((i + 1),j)) and

         A19: (f /. (k + 1)) = (( GoB r) * (i,j)) by A6, A9, A13, A15, Th24, FINSEQ_4: 21;

        

         A20: 1 <= (i + 1) & (i + 1) <= ( len ( GoB r)) by A16, MATRIX_0: 32;

        

         A21: 1 <= j & j <= ( width ( GoB r)) by A16, MATRIX_0: 32;

        

         A22: 1 <= j & j <= ( width ( GoB r)) by A16, MATRIX_0: 32;

        1 <= i & i <= ( len ( GoB r)) by A17, MATRIX_0: 32;

        

        then ((f /. (k + 1)) `2 ) = ((( GoB r) * (1,j)) `2 ) by A19, A21, GOBOARD5: 1

        .= ((f /. k) `2 ) by A18, A20, A22, GOBOARD5: 1

        .= ( S-bound ( L~ f)) by A13, EUCLID: 52;

        hence thesis by A14, A11, A12, SPRECT_2: 11;

      end;

      assume

       A23: (r /. 2) in ( S-most ( L~ f));

      

       A24: [i, j] in ( Indices ( GoB r)) by JORDAN5D:def 6;

      then

       A25: 1 <= i by MATRIX_0: 32;

      

       A26: ( L~ r) = ( L~ f) by REVROT_1: 33;

      then

       A27: (( GoB r) * (i,j)) = (r /. 1) by A7, JORDAN5D:def 6;

      

      then ((( GoB r) * (i,1)) `2 ) = ( S-bound ( L~ f)) by A7, EUCLID: 52

      .= (( S-min ( L~ f)) `2 ) by EUCLID: 52;

      then ((( GoB r) * (i2,j2)) `2 ) = ((( GoB r) * (i,1)) `2 ) by A23, A4, PSCOMP_1: 55;

      then

       A28: j2 = 1 by A24, A3, JORDAN1G: 6;

      

       A29: j <= ( width ( GoB r)) by A24, MATRIX_0: 32;

      ( rng r) = ( rng f) by FINSEQ_6: 90, SPRECT_2: 42;

      then 1 in ( dom r) by FINSEQ_3: 31, SPRECT_2: 42;

      then ( |.(1 - 1).| + |.(i - i2).|) = 1 by A1, A24, A27, A2, A3, A4, A28, GOBOARD1:def 9;

      then

       A30: ( 0 + |.(i - i2).|) = 1 by ABSVALUE: 2;

      ((( GoB r) * (i2,j2)) `1 ) <= ((( GoB r) * (i,1)) `1 ) by A7, A27, A23, A4, PSCOMP_1: 55;

      then (i - i2) >= 0 by A25, A29, A28, A5, GOBOARD5: 3, XREAL_1: 48;

      then

       A31: (i - i2) = 1 by A30, ABSVALUE:def 1;

      then i2 = (i - 1);

      then

       A32: i2 = (i -' 1) by A25, XREAL_1: 233;

      then

       A33: 1 <= (i -' 1) by A3, MATRIX_0: 32;

      

       A34: i <= ( len ( GoB r)) by A24, MATRIX_0: 32;

      

       A35: (1 + 1) <= ( len r) by TOPREAL8: 3;

      then

       A36: ( Int ( left_cell (r,1))) c= ( LeftComp r) by GOBOARD9: 21;

      ( Int ( left_cell (r,1))) <> {} by A35, GOBOARD9: 15;

      then

      consider p be object such that

       A37: p in ( Int ( left_cell (r,1))) by XBOOLE_0:def 1;

       [((i -' 1) + 1), j] in ( Indices ( GoB r)) by A24, A25, XREAL_1: 235;

      then (j -' 1) = (1 - 1) & ( left_cell (r,1,( GoB r))) = ( cell (( GoB r),(i -' 1),(j -' 1))) by A35, A1, A27, A3, A4, A28, A31, A32, GOBRD13: 25, XREAL_1: 233;

      then

       A38: ( left_cell (r,1)) = ( cell (( GoB r),(i -' 1), 0 )) by A35, JORDAN1H: 21;

      (i - 1) < i by XREAL_1: 146;

      then (i -' 1) < ( len ( GoB r)) by A34, A31, A32, XXREAL_0: 2;

      then

       A39: ( Int ( left_cell (r,1))) = { |[t, s]| where t,s be Real : ((( GoB r) * ((i -' 1),1)) `1 ) < t & t < ((( GoB r) * (((i -' 1) + 1),1)) `1 ) & s < ((( GoB r) * (1,1)) `2 ) } by A33, A38, GOBOARD6: 24;

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

      

       A40: ( LeftComp r) is_a_component_of (( L~ r) ` ) & ( UBD ( L~ r)) is_a_component_of (( L~ r) ` ) by GOBOARD9:def 1, JORDAN2C: 124;

      consider t,s be Real such that

       A41: p = |[t, s]| and ((( GoB r) * ((i -' 1),1)) `1 ) < t and t < ((( GoB r) * (((i -' 1) + 1),1)) `1 ) and

       A42: s < ((( GoB r) * (1,1)) `2 ) by A39, A37;

      now

        assume ( south_halfline p) meets ( L~ r);

        then (( south_halfline p) /\ ( L~ r)) <> {} by XBOOLE_0:def 7;

        then

        consider a be object such that

         A43: a in (( south_halfline p) /\ ( L~ r)) by XBOOLE_0:def 1;

        

         A44: a in ( L~ r) by A43, XBOOLE_0:def 4;

        

         A45: a in ( south_halfline p) by A43, XBOOLE_0:def 4;

        reconsider a as Point of ( TOP-REAL 2) by A43;

        (a `2 ) <= (p `2 ) by A45, TOPREAL1:def 12;

        then (a `2 ) <= s by A41, EUCLID: 52;

        then

         A46: (a `2 ) < ((( GoB r) * (1,1)) `2 ) by A42, XXREAL_0: 2;

        ((( GoB r) * (i,1)) `2 ) = ((( GoB r) * (1,1)) `2 ) by A25, A34, A29, GOBOARD5: 1;

        then (a `2 ) < ( S-bound ( L~ r)) by A26, A7, A27, A46, EUCLID: 52;

        hence contradiction by A44, PSCOMP_1: 24;

      end;

      then

       A47: ( south_halfline p) c= ( UBD ( L~ r)) by JORDAN2C: 128;

      p in ( south_halfline p) by TOPREAL1: 38;

      then ( LeftComp r) meets ( UBD ( L~ r)) by A36, A37, A47, XBOOLE_0: 3;

      then r is clockwise_oriented by A40, GOBOARD9: 1, JORDAN1H: 41;

      hence thesis by JORDAN1H: 40;

    end;

    theorem :: JORDAN1I:28

    for C be compact non vertical non horizontal non empty being_simple_closed_curve Subset of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) holds (p `1 ) = ((( W-bound C) + ( E-bound C)) / 2) & i > 0 & 1 <= k & k <= ( width ( Gauge (C,i))) & (( Gauge (C,i)) * (( Center ( Gauge (C,i))),k)) in ( Upper_Arc ( L~ ( Cage (C,i)))) & (p `2 ) = ( upper_bound ( proj2 .: (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,i)) * (( Center ( Gauge (C,i))),k)))) /\ ( Lower_Arc ( L~ ( Cage (C,i))))))) implies ex j st 1 <= j & j <= ( width ( Gauge (C,i))) & p = (( Gauge (C,i)) * (( Center ( Gauge (C,i))),j))

    proof

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

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

      assume that

       A1: (p `1 ) = ((( W-bound C) + ( E-bound C)) / 2) and

       A2: i > 0 and

       A3: 1 <= k and

       A4: k <= ( width ( Gauge (C,i))) and

       A5: (( Gauge (C,i)) * (( Center ( Gauge (C,i))),k)) in ( Upper_Arc ( L~ ( Cage (C,i)))) and

       A6: (p `2 ) = ( upper_bound ( proj2 .: (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,i)) * (( Center ( Gauge (C,i))),k)))) /\ ( Lower_Arc ( L~ ( Cage (C,i)))))));

      set f = ( Lower_Seq (C,i));

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

      

       A7: ( Center ( Gauge (C,i))) <= ( len G) by JORDAN1B: 13;

      4 <= ( len G) by JORDAN8: 10;

      then

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

      4 <= ( len ( Gauge (C,1))) by JORDAN8: 10;

      then 1 <= ( len ( Gauge (C,1))) by XXREAL_0: 2;

      then

       A9: ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)) `1 ) = ((G * (( Center G),1)) `1 ) by A2, A8, JORDAN1A: 36;

      

       A10: 1 <= ( Center ( Gauge (C,1))) & ( Center ( Gauge (C,1))) <= ( len ( Gauge (C,1))) by JORDAN1B: 11, JORDAN1B: 13;

      

       A11: 1 <= ( Center ( Gauge (C,i))) by JORDAN1B: 11;

      then

       A12: ((G * (( Center G),k)) `1 ) = ((G * (( Center G),1)) `1 ) by A3, A4, A7, GOBOARD5: 2;

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

      then

       A13: ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)) `2 ) <= ((G * (( Center G),1)) `2 ) by A11, A7, A10, JORDAN1A: 43;

      

       A14: (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(G * (( Center G),k)))) /\ ( L~ f)) c= (( LSeg ((G * (( Center G),1)),(G * (( Center G),k)))) /\ ( L~ f))

      proof

        let a be object;

        assume

         A15: a in (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(G * (( Center G),k)))) /\ ( L~ f));

        then

        reconsider q = a as Point of ( TOP-REAL 2);

        

         A16: a in ( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(G * (( Center G),k)))) by A15, XBOOLE_0:def 4;

        

         A17: a in ( L~ f) by A15, XBOOLE_0:def 4;

        then q in (( L~ f) \/ ( L~ ( Upper_Seq (C,i)))) by XBOOLE_0:def 3;

        then q in ( L~ ( Cage (C,i))) by JORDAN1E: 13;

        then ( S-bound ( L~ ( Cage (C,i)))) <= (q `2 ) by PSCOMP_1: 24;

        then

         A18: ((G * (( Center G),1)) `2 ) <= (q `2 ) by A7, JORDAN1A: 72, JORDAN1B: 11;

        ((G * (( Center G),1)) `2 ) <= ((G * (( Center G),k)) `2 ) by A3, A4, A11, A7, JORDAN1A: 19;

        then ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)) `2 ) <= ((G * (( Center G),k)) `2 ) by A13, XXREAL_0: 2;

        then

         A19: (q `2 ) <= ((G * (( Center G),k)) `2 ) by A16, TOPREAL1: 4;

        (q `1 ) = ((G * (( Center G),1)) `1 ) by A9, A12, A16, GOBOARD7: 5;

        then q in ( LSeg ((G * (( Center G),1)),(G * (( Center G),k)))) by A12, A19, A18, GOBOARD7: 7;

        hence thesis by A17, XBOOLE_0:def 4;

      end;

      

       A20: (G * (( Center G),k)) in ( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(G * (( Center G),k)))) by RLTOPSP1: 68;

      ((G * (( Center G),1)) `2 ) <= ((G * (( Center G),k)) `2 ) by A3, A4, A11, A7, JORDAN1A: 19;

      then (G * (( Center G),1)) in ( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(G * (( Center G),k)))) by A9, A12, A13, GOBOARD7: 7;

      then ( LSeg ((G * (( Center G),1)),(G * (( Center G),k)))) c= ( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(G * (( Center G),k)))) by A20, TOPREAL1: 6;

      then (( LSeg ((G * (( Center G),1)),(G * (( Center G),k)))) /\ ( L~ f)) c= (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(G * (( Center G),k)))) /\ ( L~ f)) by XBOOLE_1: 27;

      then (( LSeg ((G * (( Center G),1)),(G * (( Center G),k)))) /\ ( L~ f)) = (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(G * (( Center G),k)))) /\ ( L~ f)) by A14, XBOOLE_0:def 10;

      then

       A21: ( upper_bound ( proj2 .: (( LSeg ((G * (( Center ( Gauge (C,i))),1)),(G * (( Center ( Gauge (C,i))),k)))) /\ ( L~ f)))) = ( upper_bound ( proj2 .: (( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,i)) * (( Center ( Gauge (C,i))),k)))) /\ ( Lower_Arc ( L~ ( Cage (C,i))))))) by A2, JORDAN1G: 56;

      

       A22: f is_sequence_on G & ( Upper_Arc ( L~ ( Cage (C,i)))) c= ( L~ ( Cage (C,i))) by JORDAN1F: 12, JORDAN6: 61;

      ( len G) >= 4 by JORDAN8: 10;

      then ( width G) >= 4 by JORDAN8:def 1;

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

      then

       A23: [( Center ( Gauge (C,i))), 1] in ( Indices G) by A11, A7, MATRIX_0: 30;

       [( Center ( Gauge (C,i))), k] in ( Indices G) by A3, A4, A11, A7, MATRIX_0: 30;

      then

      consider n such that

       A24: 1 <= n and

       A25: n <= k and

       A26: ((G * (( Center ( Gauge (C,i))),n)) `2 ) = ( upper_bound ( proj2 .: (( LSeg ((G * (( Center ( Gauge (C,i))),1)),(G * (( Center ( Gauge (C,i))),k)))) /\ ( L~ f)))) by A3, A4, A5, A11, A7, A23, A22, JORDAN1F: 2, JORDAN1G: 46;

      take n;

      thus 1 <= n by A24;

      thus n <= ( width ( Gauge (C,i))) by A4, A25, XXREAL_0: 2;

      then (p `1 ) = ((( Gauge (C,i)) * (( Center ( Gauge (C,i))),n)) `1 ) by A1, A2, A24, JORDAN1G: 35;

      hence thesis by A6, A26, A21, TOPREAL3: 6;

    end;