jordan1e.miz



    begin

    reserve n for Nat;

    theorem :: JORDAN1E:1

    

     Th1: for f,g be FinSequence of ( TOP-REAL 2) st f is_in_the_area_of g holds for p be Element of ( TOP-REAL 2) st p in ( rng f) holds (f -: p) is_in_the_area_of g

    proof

      let f,g be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is_in_the_area_of g;

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

      assume

       A2: p in ( rng f);

      then

       A3: (p .. f) <= ( len f) by FINSEQ_4: 21;

      let n be Nat;

      assume

       A4: n in ( dom (f -: p));

      

       A5: ( len (f -: p)) = (p .. f) by A2, FINSEQ_5: 42;

      then n in ( Seg (p .. f)) by A4, FINSEQ_1:def 3;

      then

       A6: ((f -: p) /. n) = (f /. n) by A2, FINSEQ_5: 43;

      

       A7: n in ( Seg ( len (f -: p))) by A4, FINSEQ_1:def 3;

      then n <= (p .. f) by A5, FINSEQ_1: 1;

      then

       A8: n <= ( len f) by A3, XXREAL_0: 2;

      1 <= n by A7, FINSEQ_1: 1;

      then n in ( dom f) by A8, FINSEQ_3: 25;

      hence thesis by A1, A6;

    end;

    theorem :: JORDAN1E:2

    

     Th2: for f,g be FinSequence of ( TOP-REAL 2) st f is_in_the_area_of g holds for p be Element of ( TOP-REAL 2) st p in ( rng f) holds (f :- p) is_in_the_area_of g

    proof

      let f,g be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is_in_the_area_of g;

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

      assume

       A2: p in ( rng f);

      let n be Nat;

      1 <= (p .. f) by A2, FINSEQ_4: 21;

      then

       A3: ( 0 + 1) <= ((n -' 1) + (p .. f)) by XREAL_1: 7;

      assume

       A4: n in ( dom (f :- p));

      then

       A5: n in ( Seg ( len (f :- p))) by FINSEQ_1:def 3;

      then

       A6: ( 0 + 1) <= n by FINSEQ_1: 1;

      then ((n -' 1) + 1) = n by XREAL_1: 235;

      then

       A7: ((f :- p) /. n) = (f /. ((n -' 1) + (p .. f))) by A2, A4, FINSEQ_5: 52;

      ( len (f :- p)) = ((( len f) - (p .. f)) + 1) by A2, FINSEQ_5: 50;

      then n <= ((( len f) - (p .. f)) + 1) by A5, FINSEQ_1: 1;

      then (n - 1) <= (( len f) - (p .. f)) by XREAL_1: 20;

      then

       A8: ((n - 1) + (p .. f)) <= ( len f) by XREAL_1: 19;

      (n - 1) >= 0 by A6, XREAL_1: 19;

      then ((n -' 1) + (p .. f)) <= ( len f) by A8, XREAL_0:def 2;

      then ((n -' 1) + (p .. f)) in ( dom f) by A3, FINSEQ_3: 25;

      hence thesis by A1, A7;

    end;

    theorem :: JORDAN1E:3

    for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) holds ( L_Cut (f,p)) <> {}

    proof

      let f be FinSequence of ( TOP-REAL 2);

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

      assume that

       A1: p in ( L~ f) and

       A2: ( L_Cut (f,p)) = {} ;

      ( len f) <> 0 by A1, TOPREAL1: 22;

      then f <> {} ;

      then

       A3: ( len f) in ( dom f) by FINSEQ_5: 6;

      

       A4: p <> (f . (( Index (p,f)) + 1)) or p = (f . (( Index (p,f)) + 1));

      ( <*p*> ^ ( mid (f,(( Index (p,f)) + 1),( len f)))) is non empty;

      then ( L_Cut (f,p)) = ( mid (f,(( Index (p,f)) + 1),( len f))) by A2, A4, JORDAN3:def 3;

      then not (( Index (p,f)) + 1) in ( dom f) by A2, A3, SPRECT_2: 7;

      then (( Index (p,f)) + 1) < 1 or (( Index (p,f)) + 1) > ( len f) by FINSEQ_3: 25;

      then ( Index (p,f)) >= ( len f) by NAT_1: 11, NAT_1: 13;

      hence contradiction by A1, JORDAN3: 8;

    end;

    theorem :: JORDAN1E:4

    for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) & ( len ( R_Cut (f,p))) >= 2 holds (f . 1) in ( L~ ( R_Cut (f,p)))

    proof

      let f be FinSequence of ( TOP-REAL 2);

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

      assume

       A1: p in ( L~ f);

      then ( len f) <> 0 by TOPREAL1: 22;

      then ( len f) > 0 ;

      then ( 0 + 1) <= ( len f) by NAT_1: 13;

      then

       A2: (( R_Cut (f,p)) . 1) = (f . 1) by A1, JORDAN1B: 3;

      assume 2 <= ( len ( R_Cut (f,p)));

      hence thesis by A2, JORDAN3: 1;

    end;

    theorem :: JORDAN1E:5

    

     Th5: for f be FinSequence of ( TOP-REAL 2) st f is being_S-Seq holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) holds not (f . 1) in ( L~ ( mid (f,(( Index (p,f)) + 1),( len f))))

    proof

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

       A1: f is being_S-Seq;

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

       A2: p in ( L~ f) and

       A3: (f . 1) in ( L~ ( mid (f,(( Index (p,f)) + 1),( len f))));

      ( len f) <> 0 by A2, TOPREAL1: 22;

      then f <> {} ;

      then 1 in ( dom f) by FINSEQ_5: 6;

      then

       A4: (f /. 1) in ( L~ ( mid (f,(( Index (p,f)) + 1),( len f)))) by A3, PARTFUN1:def 6;

      ( Index (p,f)) < ( len f) by A2, JORDAN3: 8;

      then (( Index (p,f)) + 1) <= ( len f) by NAT_1: 13;

      then (( Index (p,f)) + 1) = ( 0 + 1) by A1, A4, JORDAN5B: 16, NAT_1: 11;

      hence contradiction by A2, JORDAN3: 8;

    end;

    theorem :: JORDAN1E:6

    

     Th6: for i,j,m,n be Nat holds (i + j) = (m + n) & i <= m & j <= n implies i = m

    proof

      let i,j,m,n be Nat;

      assume that

       A1: (i + j) = (m + n) and

       A2: i <= m and

       A3: j <= n;

      consider k be Nat such that

       A4: m = (i + k) by A2, NAT_1: 10;

      consider l be Nat such that

       A5: n = (j + l) by A3, NAT_1: 10;

      (j + (l + k)) = (j + 0 ) by A1, A4, A5;

      then k = 0 ;

      hence thesis by A4;

    end;

    theorem :: JORDAN1E:7

    for f be FinSequence of ( TOP-REAL 2) st f is being_S-Seq holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) & (f . 1) in ( L~ ( L_Cut (f,p))) holds (f . 1) = p

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is being_S-Seq;

      

       A2: ( len f) in ( dom f) by A1, FINSEQ_5: 6;

      1 in ( dom f) by A1, FINSEQ_5: 6;

      then

       A3: (f /. 1) = (f . 1) by PARTFUN1:def 6;

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

       A4: p in ( L~ f) and

       A5: (f . 1) in ( L~ ( L_Cut (f,p))) and

       A6: (f . 1) <> p;

      set g = ( mid (f,(( Index (p,f)) + 1),( len f)));

      

       A7: not (f . 1) in ( L~ g) by A1, A4, Th5;

      then p <> (f . (( Index (p,f)) + 1)) by A5, JORDAN3:def 3;

      then

       A8: ( L_Cut (f,p)) = ( <*p*> ^ g) by JORDAN3:def 3;

      per cases ;

        suppose g is empty;

        then ( L_Cut (f,p)) = <*p*> by A8, FINSEQ_1: 34;

        then ( len ( L_Cut (f,p))) = 1 by FINSEQ_1: 39;

        hence contradiction by A5, TOPREAL1: 22;

      end;

        suppose g is non empty;

        then ( L~ ( L_Cut (f,p))) = (( LSeg (p,(g /. 1))) \/ ( L~ g)) by A8, SPPOL_2: 20;

        then

         A9: (f . 1) in ( LSeg (p,(g /. 1))) by A5, A7, XBOOLE_0:def 3;

        

         A10: (1 + 1) <= ( len f) by A1;

        then

         A11: 2 in ( dom f) by FINSEQ_3: 25;

        consider i be Nat such that

         A12: 1 <= i and

         A13: (i + 1) <= ( len ( <*p*> ^ g)) and

         A14: (f /. 1) in ( LSeg (( <*p*> ^ g),i)) by A5, A3, A8, SPPOL_2: 13;

        ( LSeg (( <*p*> ^ g),i)) c= ( LSeg (f,((( Index (p,f)) + i) -' 1))) by A4, A12, A13, JORDAN3: 16;

        then

         A15: ((( Index (p,f)) + i) -' 1) = 1 by A1, A14, JORDAN5B: 30;

        

         A16: 1 <= ( Index (p,f)) by A4, JORDAN3: 8;

        then (1 + 1) <= (( Index (p,f)) + i) by A12, XREAL_1: 7;

        then

         A17: (( Index (p,f)) + i) = (1 + 1) by A15, XREAL_1: 235, XXREAL_0: 2;

        then ( Index (p,f)) = 1 by A12, A16, Th6;

        then p in ( LSeg (f,1)) by A4, JORDAN3: 9;

        then

         A18: p in ( LSeg ((f /. 1),(f /. (1 + 1)))) by A10, TOPREAL1:def 3;

        i = 1 by A12, A16, A17, Th6;

        then (g /. 1) = (f /. (1 + 1)) by A2, A17, A11, SPRECT_2: 8;

        hence contradiction by A6, A3, A9, A18, SPRECT_3: 6;

      end;

    end;

    begin

    definition

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

      let n be Nat;

      :: JORDAN1E:def1

      func Upper_Seq (C,n) -> FinSequence of ( TOP-REAL 2) equals (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) -: ( E-max ( L~ ( Cage (C,n)))));

      coherence ;

    end

    theorem :: JORDAN1E:8

    

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

    proof

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

      let n be Nat;

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

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

      hence thesis by FINSEQ_5: 42;

    end;

    definition

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

      let n be Nat;

      :: JORDAN1E:def2

      func Lower_Seq (C,n) -> FinSequence of ( TOP-REAL 2) equals (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) :- ( E-max ( L~ ( Cage (C,n)))));

      coherence ;

    end

    theorem :: JORDAN1E:9

    

     Th9: for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds ( len ( Lower_Seq (C,n))) = ((( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) - (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) + 1)

    proof

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

      let n be Nat;

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

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

      hence thesis by FINSEQ_5: 50;

    end;

    registration

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

      let n be Nat;

      cluster ( Upper_Seq (C,n)) -> non empty;

      coherence

      proof

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

        then

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

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

        hence thesis by A1, FINSEQ_4: 21;

      end;

      cluster ( Lower_Seq (C,n)) -> non empty;

      coherence

      proof

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

        then

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

        ( len ( Lower_Seq (C,n))) = ((( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) - (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) + 1) by Th9;

        then ((( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) - ( len ( Lower_Seq (C,n)))) + 1) <= ( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by A2, FINSEQ_4: 21;

        then (( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) - ( len ( Lower_Seq (C,n)))) <= (( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) - 1) by XREAL_1: 19;

        hence thesis by XREAL_1: 10;

      end;

    end

    registration

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

      let n be Nat;

      cluster ( Upper_Seq (C,n)) -> one-to-one special unfolded s.n.c.;

      coherence

      proof

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

        

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

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

        then

         A2: ( E-max ( L~ ( Cage (C,n)))) in ( rng f) by FINSEQ_6: 90, SPRECT_2: 43;

        

         A3: ( len ( Upper_Seq (C,n))) = (( E-max ( L~ ( Cage (C,n)))) .. f) by Th8;

        now

          let i1,j1 be object;

          assume that

           A4: i1 in ( dom ( Upper_Seq (C,n))) and

           A5: j1 in ( dom ( Upper_Seq (C,n))) and

           A6: (( Upper_Seq (C,n)) . i1) = (( Upper_Seq (C,n)) . j1) and

           A7: i1 <> j1;

          reconsider i2 = i1, j2 = j1 as Nat by A4, A5;

          

           A8: i2 in ( Seg (( E-max ( L~ ( Cage (C,n)))) .. f)) by A3, A4, FINSEQ_1:def 3;

          then

           A9: 1 <= i2 by FINSEQ_1: 1;

          

           A10: ( L~ ( Cage (C,n))) = ( L~ f) by REVROT_1: 33;

          

           A11: j2 in ( Seg (( E-max ( L~ ( Cage (C,n)))) .. f)) by A3, A5, FINSEQ_1:def 3;

          then

           A12: 1 <= j2 by FINSEQ_1: 1;

          j2 <= (( E-max ( L~ ( Cage (C,n)))) .. f) by A11, FINSEQ_1: 1;

          then

           A13: j2 < ( len f) by A10, SPRECT_5: 16, XXREAL_0: 2;

          

           A14: (( Upper_Seq (C,n)) . j1) = (( Upper_Seq (C,n)) /. j2) by A5, PARTFUN1:def 6

          .= (f /. j2) by A2, A11, FINSEQ_5: 43;

          i2 <= (( E-max ( L~ ( Cage (C,n)))) .. f) by A8, FINSEQ_1: 1;

          then

           A15: i2 < ( len f) by A10, SPRECT_5: 16, XXREAL_0: 2;

          

           A16: (( Upper_Seq (C,n)) . i1) = (( Upper_Seq (C,n)) /. i2) by A4, PARTFUN1:def 6

          .= (f /. i2) by A2, A8, FINSEQ_5: 43;

          per cases by A7, XXREAL_0: 1;

            suppose i2 < j2;

            hence contradiction by A6, A16, A14, A9, A13, GOBOARD7: 36;

          end;

            suppose j2 < i2;

            hence contradiction by A6, A16, A14, A12, A15, GOBOARD7: 36;

          end;

        end;

        hence ( Upper_Seq (C,n)) is one-to-one by FUNCT_1:def 4;

        thus ( Upper_Seq (C,n)) is special;

        thus ( Upper_Seq (C,n)) is unfolded;

        let i,j be Nat;

        assume

         A17: (i + 1) < j;

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

        then

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

        now

          per cases ;

            suppose

             A19: (j + 1) <= ( len ( Upper_Seq (C,n)));

            

             A20: (( E-max ( L~ ( Cage (C,n)))) .. f) <= ( len f) by A2, FINSEQ_4: 21;

            

             A21: (j + 1) <= (( E-max ( L~ ( Cage (C,n)))) .. f) by A2, A19, FINSEQ_5: 42;

             A22:

            now

              per cases by A21, XXREAL_0: 1;

                suppose (j + 1) < (( E-max ( L~ ( Cage (C,n)))) .. f);

                hence (j + 1) < ( len f) by A20, XXREAL_0: 2;

              end;

                suppose

                 A23: (j + 1) = (( E-max ( L~ ( Cage (C,n)))) .. f);

                assume (j + 1) >= ( len f);

                then (( E-max ( L~ ( Cage (C,n)))) .. f) = ( len f) by A20, A23, XXREAL_0: 1;

                

                then ( E-max ( L~ ( Cage (C,n)))) = (f . ( len f)) by A2, FINSEQ_4: 19

                .= (f /. ( len f)) by A18, PARTFUN1:def 6

                .= (f /. 1) by FINSEQ_6:def 1

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

                hence contradiction by TOPREAL5: 19;

              end;

            end;

            j < ( len ( Upper_Seq (C,n))) by A19, NAT_1: 13;

            then

             A24: ( LSeg (( Upper_Seq (C,n)),i)) = ( LSeg (f,i)) by A17, SPPOL_2: 9, XXREAL_0: 2;

            ( LSeg (( Upper_Seq (C,n)),j)) = ( LSeg (f,j)) by A19, SPPOL_2: 9;

            hence thesis by A17, A24, A22, GOBOARD5:def 4;

          end;

            suppose (j + 1) > ( len ( Upper_Seq (C,n)));

            then ( LSeg (( Upper_Seq (C,n)),j)) = {} by TOPREAL1:def 3;

            then (( LSeg (( Upper_Seq (C,n)),i)) /\ ( LSeg (( Upper_Seq (C,n)),j))) = {} ;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      cluster ( Lower_Seq (C,n)) -> one-to-one special unfolded s.n.c.;

      coherence

      proof

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

        

         A25: ( L~ ( Cage (C,n))) = ( L~ f) by REVROT_1: 33;

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

        then

         A26: (f /. 1) = ( W-min ( L~ f)) by A25, FINSEQ_6: 92;

        then (( W-max ( L~ ( Cage (C,n)))) .. f) <= (( N-min ( L~ ( Cage (C,n)))) .. f) by A25, SPRECT_5: 23;

        then (( N-min ( L~ ( Cage (C,n)))) .. f) > 1 by A25, A26, SPRECT_5: 22, XXREAL_0: 2;

        then (( N-max ( L~ ( Cage (C,n)))) .. f) > 1 by A25, A26, SPRECT_5: 24, XXREAL_0: 2;

        then

         A27: (( E-max ( L~ ( Cage (C,n)))) .. f) > 1 by A25, A26, SPRECT_5: 25, XXREAL_0: 2;

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

        then

         A28: ( E-max ( L~ ( Cage (C,n)))) in ( rng f) by FINSEQ_6: 90, SPRECT_2: 43;

        

         A29: ( len ( Lower_Seq (C,n))) = ((( len f) - (( E-max ( L~ ( Cage (C,n)))) .. f)) + 1) by Th9;

        now

          let i1,j1 be object;

          assume that

           A30: i1 in ( dom ( Lower_Seq (C,n))) and

           A31: j1 in ( dom ( Lower_Seq (C,n))) and

           A32: (( Lower_Seq (C,n)) . i1) = (( Lower_Seq (C,n)) . j1) and

           A33: i1 <> j1;

          reconsider i2 = i1, j2 = j1 as Nat by A30, A31;

          

           A34: i2 in ( Seg ( len ( Lower_Seq (C,n)))) by A30, FINSEQ_1:def 3;

          then i2 >= 1 by FINSEQ_1: 1;

          then

           A35: i2 = ((i2 -' 1) + 1) by XREAL_1: 235;

          

           A36: (( Lower_Seq (C,n)) . i1) = (( Lower_Seq (C,n)) /. i2) by A30, PARTFUN1:def 6

          .= (f /. ((i2 -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f))) by A28, A30, A35, FINSEQ_5: 52;

          

           A37: j2 in ( Seg ( len ( Lower_Seq (C,n)))) by A31, FINSEQ_1:def 3;

          then j2 >= 1 by FINSEQ_1: 1;

          then

           A38: j2 = ((j2 -' 1) + 1) by XREAL_1: 235;

          

           A39: (( Lower_Seq (C,n)) . j1) = (( Lower_Seq (C,n)) /. j2) by A31, PARTFUN1:def 6

          .= (f /. ((j2 -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f))) by A28, A31, A38, FINSEQ_5: 52;

          ( 0 + 1) <= i2 by A34, FINSEQ_1: 1;

          then

           A40: (i2 - 1) >= 0 by XREAL_1: 19;

          i2 <= ((( len f) - (( E-max ( L~ ( Cage (C,n)))) .. f)) + 1) by A29, A34, FINSEQ_1: 1;

          then (i2 - 1) <= (( len f) - (( E-max ( L~ ( Cage (C,n)))) .. f)) by XREAL_1: 20;

          then ((i2 - 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) <= ( len f) by XREAL_1: 19;

          then

           A41: ((i2 -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) <= ( len f) by A40, XREAL_0:def 2;

          ( 0 + 1) <= j2 by A37, FINSEQ_1: 1;

          then

           A42: (j2 - 1) >= 0 by XREAL_1: 19;

          j2 <= ((( len f) - (( E-max ( L~ ( Cage (C,n)))) .. f)) + 1) by A29, A37, FINSEQ_1: 1;

          then (j2 - 1) <= (( len f) - (( E-max ( L~ ( Cage (C,n)))) .. f)) by XREAL_1: 20;

          then ((j2 - 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) <= ( len f) by XREAL_1: 19;

          then

           A43: ((j2 -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) <= ( len f) by A42, XREAL_0:def 2;

          ((j2 -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) >= (( E-max ( L~ ( Cage (C,n)))) .. f) by NAT_1: 11;

          then

           A44: 1 < ((j2 -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) by A27, XXREAL_0: 2;

          ((i2 -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) >= (( E-max ( L~ ( Cage (C,n)))) .. f) by NAT_1: 11;

          then

           A45: 1 < ((i2 -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) by A27, XXREAL_0: 2;

          per cases by A33, XXREAL_0: 1;

            suppose i2 < j2;

            then (i2 - 1) < (j2 - 1) by XREAL_1: 9;

            then (i2 - 1) < (j2 -' 1) by XREAL_0:def 2;

            then (i2 -' 1) < (j2 -' 1) by A40, XREAL_0:def 2;

            then ((i2 -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) < ((j2 -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) by XREAL_1: 6;

            hence contradiction by A32, A36, A39, A43, A45, GOBOARD7: 37;

          end;

            suppose j2 < i2;

            then (j2 - 1) < (i2 - 1) by XREAL_1: 9;

            then (j2 - 1) < (i2 -' 1) by XREAL_0:def 2;

            then (j2 -' 1) < (i2 -' 1) by A42, XREAL_0:def 2;

            then ((j2 -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) < ((i2 -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) by XREAL_1: 6;

            hence contradiction by A32, A36, A39, A41, A44, GOBOARD7: 37;

          end;

        end;

        hence ( Lower_Seq (C,n)) is one-to-one by FUNCT_1:def 4;

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

        then

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

        hence ( Lower_Seq (C,n)) is special by SPPOL_2: 39;

        thus ( Lower_Seq (C,n)) is unfolded by A46, SPPOL_2: 27;

        let i,j be Nat;

        assume

         A47: (i + 1) < j;

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

        then j = ((j -' 1) + 1) by A47, XREAL_1: 235, XXREAL_0: 2;

        then

         A48: ( LSeg (( Lower_Seq (C,n)),j)) = ( LSeg (f,((j -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)))) by A46, SPPOL_2: 10;

        now

          per cases ;

            suppose i > 0 ;

            then

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

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

            then

             A50: ( LSeg (( Lower_Seq (C,n)),i)) = ( LSeg (f,((i -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)))) by A28, SPPOL_2: 10;

            ((i + 1) - 1) < (j - 1) by A47, XREAL_1: 9;

            then

             A51: ((i - 1) + 1) < (j -' 1) by XREAL_0:def 2;

            (i - 1) >= 0 by A49, XREAL_1: 19;

            then ((i -' 1) + 1) < (j -' 1) by A51, XREAL_0:def 2;

            then (((i -' 1) + 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) < ((j -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) by XREAL_1: 6;

            then

             A52: (((i -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) + 1) < ((j -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f));

            

             A53: ((i -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) > ( 0 + 1) by A27, XREAL_1: 8;

            now

              per cases ;

                suppose (((j -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) + 1) <= ( len f);

                then ((j -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) < ( len f) by NAT_1: 13;

                then ( LSeg (( Lower_Seq (C,n)),i)) misses ( LSeg (( Lower_Seq (C,n)),j)) by A48, A50, A52, A53, GOBOARD5:def 4;

                hence (( LSeg (( Lower_Seq (C,n)),i)) /\ ( LSeg (( Lower_Seq (C,n)),j))) = {} ;

              end;

                suppose (((j -' 1) + (( E-max ( L~ ( Cage (C,n)))) .. f)) + 1) > ( len f);

                then ( LSeg (( Lower_Seq (C,n)),j)) = {} by A48, TOPREAL1:def 3;

                hence (( LSeg (( Lower_Seq (C,n)),i)) /\ ( LSeg (( Lower_Seq (C,n)),j))) = {} ;

              end;

            end;

            hence (( LSeg (( Lower_Seq (C,n)),i)) /\ ( LSeg (( Lower_Seq (C,n)),j))) = {} ;

          end;

            suppose i = 0 ;

            then ( LSeg (( Lower_Seq (C,n)),i)) = {} by TOPREAL1:def 3;

            hence (( LSeg (( Lower_Seq (C,n)),i)) /\ ( LSeg (( Lower_Seq (C,n)),j))) = {} ;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: JORDAN1E:10

    

     Th10: for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds (( len ( Upper_Seq (C,n))) + ( len ( Lower_Seq (C,n)))) = (( len ( Cage (C,n))) + 1)

    proof

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

      let n be Nat;

      

      thus (( len ( Upper_Seq (C,n))) + ( len ( Lower_Seq (C,n)))) = ((( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) + ( len ( Lower_Seq (C,n)))) by Th8

      .= ((( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) + ((( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) - (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) + 1)) by Th9

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

      .= (( len ( Cage (C,n))) + 1) by FINSEQ_6: 179;

    end;

    theorem :: JORDAN1E:11

    

     Th11: for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) = (( Upper_Seq (C,n)) ^' ( Lower_Seq (C,n)))

    proof

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

      let n be Nat;

      

       A1: ( dom ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) = ( Seg ( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) by FINSEQ_1:def 3;

      

       A2: (( len (( Upper_Seq (C,n)) ^' ( Lower_Seq (C,n)))) + 1) = (( len ( Upper_Seq (C,n))) + ( len ( Lower_Seq (C,n)))) by FINSEQ_6: 139

      .= (( len ( Cage (C,n))) + 1) by Th10

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

      now

        let i be Nat;

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

        then

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

        assume

         A4: i in ( dom ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))));

        then

         A5: 1 <= i by A1, FINSEQ_1: 1;

        

         A6: i <= ( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by A1, A4, FINSEQ_1: 1;

        per cases ;

          suppose

           A7: i <= ( len ( Upper_Seq (C,n)));

          then i <= (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by Th8;

          then

           A8: i in ( Seg (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) by A5, FINSEQ_1: 1;

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

          then

           A9: i in ( dom (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) -: ( E-max ( L~ ( Cage (C,n)))))) by A8, FINSEQ_1:def 3;

          

          thus ((( Upper_Seq (C,n)) ^' ( Lower_Seq (C,n))) . i) = ((( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) -: ( E-max ( L~ ( Cage (C,n))))) . i) by A5, A7, FINSEQ_6: 140

          .= ((( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) -: ( E-max ( L~ ( Cage (C,n))))) /. i) by A9, PARTFUN1:def 6

          .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. i) by A3, A8, FINSEQ_5: 43

          .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) . i) by A4, PARTFUN1:def 6;

        end;

          suppose i > ( len ( Upper_Seq (C,n)));

          then i >= (( len ( Upper_Seq (C,n))) + 1) by NAT_1: 13;

          then

          consider j be Nat such that

           A10: i = ((( len ( Upper_Seq (C,n))) + 1) + j) by NAT_1: 10;

          reconsider j as Nat;

          

           A11: i = (( len ( Upper_Seq (C,n))) + (j + 1)) by A10;

          then

           A12: i = ((( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) + (j + 1)) by Th8;

          

           A13: ( len (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) :- ( E-max ( L~ ( Cage (C,n)))))) = ((( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) - (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) + 1) by A3, FINSEQ_5: 50;

          ((j + 1) + (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) <= ( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by A6, A11, Th8;

          then (j + 1) <= (( len ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) - (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))))) by XREAL_1: 19;

          then ((j + 1) + 1) >= 1 & ((j + 1) + 1) <= ( len (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) :- ( E-max ( L~ ( Cage (C,n)))))) by A13, NAT_1: 11, XREAL_1: 7;

          then

           A14: ((j + 1) + 1) in ( dom (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) :- ( E-max ( L~ ( Cage (C,n)))))) by FINSEQ_3: 25;

          i < (( len (( Upper_Seq (C,n)) ^' ( Lower_Seq (C,n)))) + 1) by A2, A6, NAT_1: 13;

          then i < (( len ( Lower_Seq (C,n))) + ( len ( Upper_Seq (C,n)))) by FINSEQ_6: 139;

          then (i - ( len ( Upper_Seq (C,n)))) < ( len ( Lower_Seq (C,n))) by XREAL_1: 19;

          

          hence ((( Upper_Seq (C,n)) ^' ( Lower_Seq (C,n))) . i) = ((( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) :- ( E-max ( L~ ( Cage (C,n))))) . ((j + 1) + 1)) by A11, FINSEQ_6: 141, NAT_1: 11

          .= ((( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) :- ( E-max ( L~ ( Cage (C,n))))) /. ((j + 1) + 1)) by A14, PARTFUN1:def 6

          .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. ((j + 1) + (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))))) by A3, A14, FINSEQ_5: 52

          .= (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) . i) by A4, A12, PARTFUN1:def 6;

        end;

      end;

      hence thesis by A2, FINSEQ_2: 9;

    end;

    theorem :: JORDAN1E:12

    for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds ( L~ ( Cage (C,n))) = ( L~ (( Upper_Seq (C,n)) ^' ( Lower_Seq (C,n))))

    proof

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

      let n be Nat;

      ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) = (( Upper_Seq (C,n)) ^' ( Lower_Seq (C,n))) by Th11;

      hence thesis by REVROT_1: 33;

    end;

    theorem :: JORDAN1E:13

    for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds for n be Nat holds ( L~ ( Cage (C,n))) = (( L~ ( Upper_Seq (C,n))) \/ ( L~ ( Lower_Seq (C,n))))

    proof

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

      let n be Nat;

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

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

      then ( L~ ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) = (( L~ ( Upper_Seq (C,n))) \/ ( L~ ( Lower_Seq (C,n)))) by SPPOL_2: 24;

      hence thesis by REVROT_1: 33;

    end;

    theorem :: JORDAN1E:14

    

     Th14: for P be Simple_closed_curve holds ( W-min P) <> ( E-min P)

    proof

      let P be Simple_closed_curve;

      now

        assume ( W-min P) = ( E-min P);

        then ( W-bound P) = ( E-bound P) by SPPOL_2: 1;

        hence contradiction by TOPREAL5: 17;

      end;

      hence thesis;

    end;

    theorem :: JORDAN1E:15

    

     Th15: for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds ( len ( Upper_Seq (C,n))) >= 3 & ( len ( Lower_Seq (C,n))) >= 3

    proof

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

      let n be Nat;

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

      set pWa = ( W-max ( L~ ( Cage (C,n))));

      set pEi = ( E-min ( L~ ( Cage (C,n))));

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

      

       A1: pWi <> pEa by TOPREAL5: 19;

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

      

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

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

      then

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

      

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

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

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

      then

       A4: pEa in ( rng ( Lower_Seq (C,n))) & pWi in ( rng ( Lower_Seq (C,n))) by FINSEQ_6: 61, FINSEQ_6: 168;

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

      then

       A5: pEa in ( rng ( Upper_Seq (C,n))) by A3, FINSEQ_5: 46;

      pWa in ( rng ( Cage (C,n))) by SPRECT_2: 44;

      then

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

      

       A7: (( Upper_Seq (C,n)) /. 1) = (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. 1) by A3, FINSEQ_5: 44;

      then

       A8: (( Upper_Seq (C,n)) /. 1) = ( W-min ( L~ ( Cage (C,n)))) by A2, FINSEQ_6: 92;

      then

       A9: pWi in ( rng ( Upper_Seq (C,n))) by FINSEQ_6: 42;

      

       A10: ( L~ ( Cage (C,n))) = ( L~ f) by REVROT_1: 33;

      then (( W-max ( L~ f)) .. f) <= (( N-min ( L~ f)) .. f) by A2, A7, FINSEQ_6: 92, SPRECT_5: 23;

      then

       A11: (( W-max ( L~ f)) .. f) < (( N-max ( L~ f)) .. f) by A7, A8, A10, SPRECT_5: 24, XXREAL_0: 2;

      (( N-max ( L~ f)) .. f) <= (( E-max ( L~ f)) .. f) by A2, A7, A10, FINSEQ_6: 92, SPRECT_5: 25;

      then

       A12: pWa in ( rng ( Upper_Seq (C,n))) by A3, A6, A10, A11, FINSEQ_5: 46, XXREAL_0: 2;

       {pWi, pWa, pEa} c= ( rng ( Upper_Seq (C,n))) by A5, A9, A12, ENUMSET1:def 1;

      then

       A13: ( card {pWi, pWa, pEa}) c= ( card ( rng ( Upper_Seq (C,n)))) by CARD_1: 11;

      ( card ( rng ( Upper_Seq (C,n)))) c= ( card ( dom ( Upper_Seq (C,n)))) by CARD_2: 61;

      then

       A14: ( card ( rng ( Upper_Seq (C,n)))) c= ( len ( Upper_Seq (C,n))) by CARD_1: 62;

      pWi <> pWa & pWa <> pEa by JORDAN1B: 5, SPRECT_2: 58;

      then ( card {pWi, pWa, pEa}) = 3 by A1, CARD_2: 58;

      then ( Segm 3) c= ( Segm ( len ( Upper_Seq (C,n)))) by A13, A14;

      hence ( len ( Upper_Seq (C,n))) >= 3 by NAT_1: 39;

      

       A15: pWi <> pEa by TOPREAL5: 19;

      pEi in ( rng ( Cage (C,n))) by SPRECT_2: 45;

      then

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

      (pEi .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) > (pEa .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by A2, A7, A10, FINSEQ_6: 92, SPRECT_5: 26;

      then

       A17: pEi in ( rng ( Lower_Seq (C,n))) by A3, A16, FINSEQ_6: 62;

       {pWi, pEi, pEa} c= ( rng ( Lower_Seq (C,n))) by A4, A17, ENUMSET1:def 1;

      then

       A18: ( card {pWi, pEi, pEa}) c= ( card ( rng ( Lower_Seq (C,n)))) by CARD_1: 11;

      ( card ( rng ( Lower_Seq (C,n)))) c= ( card ( dom ( Lower_Seq (C,n)))) by CARD_2: 61;

      then

       A19: ( card ( rng ( Lower_Seq (C,n)))) c= ( len ( Lower_Seq (C,n))) by CARD_1: 62;

      pWi <> pEi & pEi <> pEa by Th14, SPRECT_2: 54;

      then ( card {pWi, pEi, pEa}) = 3 by A15, CARD_2: 58;

      then ( Segm 3) c= ( Segm ( len ( Lower_Seq (C,n)))) by A18, A19;

      hence thesis by NAT_1: 39;

    end;

    registration

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

      let n be Nat;

      cluster ( Upper_Seq (C,n)) -> being_S-Seq;

      coherence

      proof

        ( len ( Upper_Seq (C,n))) >= 3 by Th15;

        then ( len ( Upper_Seq (C,n))) >= 2 by XXREAL_0: 2;

        hence thesis;

      end;

      cluster ( Lower_Seq (C,n)) -> being_S-Seq;

      coherence

      proof

        ( len ( Lower_Seq (C,n))) >= 3 by Th15;

        then ( len ( Lower_Seq (C,n))) >= 2 by XXREAL_0: 2;

        hence thesis;

      end;

    end

    theorem :: JORDAN1E:16

    for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds (( L~ ( Upper_Seq (C,n))) /\ ( L~ ( Lower_Seq (C,n)))) = {( W-min ( L~ ( Cage (C,n)))), ( E-max ( L~ ( Cage (C,n))))}

    proof

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

      let n be Nat;

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

      then

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

      

       A2: ( len ( Upper_Seq (C,n))) >= 3 by Th15;

      then

       A3: ( rng ( Upper_Seq (C,n))) c= ( L~ ( Upper_Seq (C,n))) by SPPOL_2: 18, XXREAL_0: 2;

      

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

      thus (( L~ ( Upper_Seq (C,n))) /\ ( L~ ( Lower_Seq (C,n)))) c= {( W-min ( L~ ( Cage (C,n)))), ( E-max ( L~ ( Cage (C,n))))}

      proof

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

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

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

        let x be object;

        assume

         A5: x in (( L~ ( Upper_Seq (C,n))) /\ ( L~ ( Lower_Seq (C,n))));

        then

        reconsider x1 = x as Point of ( TOP-REAL 2);

        assume

         A6: not x in {( W-min ( L~ ( Cage (C,n)))), ( E-max ( L~ ( Cage (C,n))))};

        x in ( L~ ( Upper_Seq (C,n))) by A5, XBOOLE_0:def 4;

        then

        consider i1 be Nat such that

         A7: 1 <= i1 and

         A8: (i1 + 1) <= ( len ( Upper_Seq (C,n))) and

         A9: x1 in ( LSeg (( Upper_Seq (C,n)),i1)) by SPPOL_2: 13;

        

         A10: ( LSeg (( Upper_Seq (C,n)),i1)) = ( LSeg (f,i1)) by A8, SPPOL_2: 9;

        x in ( L~ ( Lower_Seq (C,n))) by A5, XBOOLE_0:def 4;

        then

        consider i2 be Nat such that

         A11: 1 <= i2 and

         A12: (i2 + 1) <= ( len ( Lower_Seq (C,n))) and

         A13: x1 in ( LSeg (( Lower_Seq (C,n)),i2)) by SPPOL_2: 13;

        set i3 = (i2 -' 1);

        

         A14: (i3 + 1) = i2 by A11, XREAL_1: 235;

        then

         A15: (1 + (pE .. f)) <= ((i3 + 1) + (pE .. f)) by A11, XREAL_1: 7;

        

         A16: ( len ( Lower_Seq (C,n))) = ((( len f) - (pE .. f)) + 1) by Th9;

        then i2 < ((( len f) - (pE .. f)) + 1) by A12, NAT_1: 13;

        then (i2 - 1) < (( len f) - (pE .. f)) by XREAL_1: 19;

        then

         A17: ((i2 - 1) + (pE .. f)) < ( len f) by XREAL_1: 20;

        (i2 - 1) >= (1 - 1) by A11, XREAL_1: 9;

        then

         A18: (i3 + (pE .. f)) < ( len f) by A17, XREAL_0:def 2;

        

         A19: ( LSeg (( Lower_Seq (C,n)),i2)) = ( LSeg (f,(i3 + (pE .. f)))) by A1, A14, SPPOL_2: 10;

        

         A20: ( len ( Upper_Seq (C,n))) = (pE .. f) by Th8;

        then (i1 + 1) < ((pE .. f) + 1) by A8, NAT_1: 13;

        then (i1 + 1) < ((i3 + (pE .. f)) + 1) by A15, XXREAL_0: 2;

        then

         A21: (i1 + 1) <= (i3 + (pE .. f)) by NAT_1: 13;

        

         A22: (((pE .. f) -' 1) + 1) = (pE .. f) by A1, FINSEQ_4: 21, XREAL_1: 235;

        (i3 + 1) < ((( len f) - (pE .. f)) + 1) by A12, A14, A16, NAT_1: 13;

        then i3 < (( len f) - (pE .. f)) by XREAL_1: 7;

        then

         A23: (i3 + (pE .. f)) < ( len f) by XREAL_1: 20;

        then

         A24: ((i3 + (pE .. f)) + 1) <= ( len f) by NAT_1: 13;

        now

          per cases by A7, A21, XXREAL_0: 1;

            suppose (i1 + 1) < (i3 + (pE .. f)) & i1 > 1;

            then ( LSeg (f,i1)) misses ( LSeg (f,(i3 + (pE .. f)))) by A23, GOBOARD5:def 4;

            then (( LSeg (f,i1)) /\ ( LSeg (f,(i3 + (pE .. f))))) = {} ;

            hence contradiction by A9, A13, A10, A19, XBOOLE_0:def 4;

          end;

            suppose

             A25: i1 = 1;

            (i3 + (pE .. f)) >= ( 0 + 3) by A2, A20, XREAL_1: 7;

            then

             A26: (i1 + 1) < (i3 + (pE .. f)) by A25, XXREAL_0: 2;

            now

              per cases by A24, XXREAL_0: 1;

                suppose ((i3 + (pE .. f)) + 1) < ( len f);

                then ( LSeg (f,i1)) misses ( LSeg (f,(i3 + (pE .. f)))) by A26, GOBOARD5:def 4;

                then (( LSeg (f,i1)) /\ ( LSeg (f,(i3 + (pE .. f))))) = {} ;

                hence contradiction by A9, A13, A10, A19, XBOOLE_0:def 4;

              end;

                suppose ((i3 + (pE .. f)) + 1) = ( len f);

                then (i3 + (pE .. f)) = (( len f) - 1);

                then (i3 + (pE .. f)) = (( len f) -' 1) by XREAL_0:def 2;

                then (( LSeg (f,i1)) /\ ( LSeg (f,(i3 + (pE .. f))))) = {(f /. 1)} by A25, GOBOARD7: 34, REVROT_1: 30;

                then x1 in {(f /. 1)} by A9, A13, A10, A19, XBOOLE_0:def 4;

                

                then x1 = (f /. 1) by TARSKI:def 1

                .= pW by A4, FINSEQ_6: 92;

                hence contradiction by A6, TARSKI:def 2;

              end;

            end;

            hence contradiction;

          end;

            suppose

             A27: (i1 + 1) = (i3 + (pE .. f));

            (i3 + (pE .. f)) >= (pE .. f) by NAT_1: 11;

            then (pE .. f) < ( len f) by A18, XXREAL_0: 2;

            then ((pE .. f) + 1) <= ( len f) by NAT_1: 13;

            then

             A28: (((pE .. f) -' 1) + (1 + 1)) <= ( len f) by A22;

            ( 0 + (pE .. f)) <= (i3 + (pE .. f)) by XREAL_1: 7;

            then (pE .. f) = (i1 + 1) by A8, A20, A27, XXREAL_0: 1;

            then (( LSeg (f,i1)) /\ ( LSeg (f,(i3 + (pE .. f))))) = {(f /. (pE .. f))} by A7, A22, A27, A28, TOPREAL1:def 6;

            then x1 in {(f /. (pE .. f))} by A9, A13, A10, A19, XBOOLE_0:def 4;

            

            then x1 = (f /. (pE .. f)) by TARSKI:def 1

            .= pE by A1, FINSEQ_5: 38;

            hence contradiction by A6, TARSKI:def 2;

          end;

        end;

        hence contradiction;

      end;

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

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

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

      then

       A29: ( W-min ( L~ ( Cage (C,n)))) in ( rng ( Lower_Seq (C,n))) by FINSEQ_6: 168;

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

      then

       A30: ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Lower_Seq (C,n))) & ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Upper_Seq (C,n))) by A1, FINSEQ_5: 46, FINSEQ_6: 61;

      ( len ( Lower_Seq (C,n))) >= 3 by Th15;

      then

       A31: ( rng ( Lower_Seq (C,n))) c= ( L~ ( Lower_Seq (C,n))) by SPPOL_2: 18, XXREAL_0: 2;

      (( Upper_Seq (C,n)) /. 1) = (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) /. 1) by A1, FINSEQ_5: 44

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

      then

       A32: ( W-min ( L~ ( Cage (C,n)))) in ( rng ( Upper_Seq (C,n))) by FINSEQ_6: 42;

      thus {( W-min ( L~ ( Cage (C,n)))), ( E-max ( L~ ( Cage (C,n))))} c= (( L~ ( Upper_Seq (C,n))) /\ ( L~ ( Lower_Seq (C,n))))

      proof

        let x be object;

        assume

         A33: x in {( W-min ( L~ ( Cage (C,n)))), ( E-max ( L~ ( Cage (C,n))))};

        per cases by A33, TARSKI:def 2;

          suppose x = ( W-min ( L~ ( Cage (C,n))));

          hence thesis by A31, A3, A32, A29, XBOOLE_0:def 4;

        end;

          suppose x = ( E-max ( L~ ( Cage (C,n))));

          hence thesis by A31, A3, A30, XBOOLE_0:def 4;

        end;

      end;

    end;

    theorem :: JORDAN1E:17

    for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds ( Upper_Seq (C,n)) is_in_the_area_of ( Cage (C,n))

    proof

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

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

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

      hence thesis by Th1, JORDAN1B: 10;

    end;

    theorem :: JORDAN1E:18

    for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds ( Lower_Seq (C,n)) is_in_the_area_of ( Cage (C,n))

    proof

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

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

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

      hence thesis by Th2, JORDAN1B: 10;

    end;

    theorem :: JORDAN1E:19

    for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds ((( Cage (C,n)) /. 2) `2 ) = ( N-bound ( L~ ( Cage (C,n))))

    proof

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

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

      then (( Cage (C,n)) /. 2) in ( N-most ( L~ ( Cage (C,n)))) by SPRECT_2: 30;

      then ((( Cage (C,n)) /. 2) `2 ) = (( N-min ( L~ ( Cage (C,n)))) `2 ) by PSCOMP_1: 39;

      hence thesis by EUCLID: 52;

    end;

    theorem :: JORDAN1E:20

    for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds for k be Nat st 1 <= k & (k + 1) <= ( len ( Cage (C,n))) & (( Cage (C,n)) /. k) = ( E-max ( L~ ( Cage (C,n)))) holds ((( Cage (C,n)) /. (k + 1)) `1 ) = ( E-bound ( L~ ( Cage (C,n))))

    proof

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

      

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

      

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

      

       A3: (( 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

       A4: (( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) > 1 by A3, SPRECT_2: 70, XXREAL_0: 2;

      let k be Nat;

      assume that

       A5: 1 <= k and

       A6: (k + 1) <= ( len ( Cage (C,n))) and

       A7: (( Cage (C,n)) /. k) = ( E-max ( L~ ( Cage (C,n))));

      

       A8: k < ( len ( Cage (C,n))) by A6, NAT_1: 13;

      then

       A9: k in ( dom ( Cage (C,n))) by A5, FINSEQ_3: 25;

      then

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

      (( E-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) <= k by A7, A9, FINSEQ_5: 39;

      then

       A10: k > 1 by A4, XXREAL_0: 2;

      then

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

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

       A12: (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (i1,j1)) and

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

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

       A15: 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, A6, JORDAN8: 3;

      

       A16: 1 <= i1 by A11, MATRIX_0: 32;

      

       A17: (k9 + 1) < ( len ( Cage (C,n))) by A6, NAT_1: 13;

      

       A18: 1 <= j1 by A11, MATRIX_0: 32;

      

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

      

       A20: i2 <= ( len ( Gauge (C,n))) by A13, MATRIX_0: 32;

      

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

      ((( Gauge (C,n)) * (i1,j1)) `1 ) = ( E-bound ( L~ ( Cage (C,n)))) by A7, A12, EUCLID: 52

      .= ((( Gauge (C,n)) * (( len ( Gauge (C,n))),j1)) `1 ) by A18, A21, A2, JORDAN1A: 71;

      then

       A22: i1 >= ( len ( Gauge (C,n))) by A16, A18, A21, GOBOARD5: 3;

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

      then

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

      then

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

       A24: [i3, j3] in ( Indices ( Gauge (C,n))) and

       A25: (( Cage (C,n)) /. k9) = (( Gauge (C,n)) * (i3,j3)) and

       A26: [i4, j4] in ( Indices ( Gauge (C,n))) and

       A27: (( Cage (C,n)) /. (k9 + 1)) = (( Gauge (C,n)) * (i4,j4)) and

       A28: 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, A8, JORDAN8: 3;

      

       A29: i1 = i4 by A11, A12, A26, A27, GOBOARD1: 5;

      

       A30: j1 = j4 by A11, A12, A26, A27, GOBOARD1: 5;

      

       A31: 1 <= j3 by A24, MATRIX_0: 32;

      

       A32: j3 <= ( width ( Gauge (C,n))) by A24, MATRIX_0: 32;

      

       A33: i1 <= ( len ( Gauge (C,n))) by A11, MATRIX_0: 32;

      then

       A34: i1 = ( len ( Gauge (C,n))) by A22, XXREAL_0: 1;

      

       A35: j3 = j4

      proof

        assume

         A36: j3 <> j4;

        per cases by A28, A36;

          suppose i3 = i4 & (j3 + 1) = j4;

          hence contradiction by A8, A22, A23, A24, A25, A26, A27, A29, JORDAN10: 1;

        end;

          suppose

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

          k9 < ( len ( Cage (C,n))) by A17, NAT_1: 13;

          then (( Gauge (C,n)) * (i3,j3)) in ( E-most ( L~ ( Cage (C,n)))) by A34, A23, A25, A29, A31, A32, A37, JORDAN1A: 61;

          then

           A38: ((( Gauge (C,n)) * (i4,(j4 + 1))) `2 ) <= ((( Gauge (C,n)) * (i4,j4)) `2 ) by A7, A27, A37, PSCOMP_1: 47;

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

          hence contradiction by A16, A33, A18, A29, A30, A32, A37, A38, GOBOARD5: 4;

        end;

      end;

      

       A39: 1 <= i2 & 1 <= j2 by A13, MATRIX_0: 32;

      

       A40: (k9 + 1) = k;

      

       A41: i3 <= ( len ( Gauge (C,n))) by A24, MATRIX_0: 32;

      i1 = i2

      proof

        assume

         A42: i1 <> i2;

        per cases by A15, A42;

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

          hence contradiction by A20, A22, NAT_1: 13;

        end;

          suppose

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

          (k9 + (1 + 1)) <= ( len ( Cage (C,n))) by A6;

          then

           A44: (( LSeg (( Cage (C,n)),k9)) /\ ( LSeg (( Cage (C,n)),k))) = {(( Cage (C,n)) /. k)} by A23, A40, TOPREAL1:def 6;

          (( Cage (C,n)) /. k9) in ( LSeg (( Cage (C,n)),k9)) & (( Cage (C,n)) /. (k + 1)) in ( LSeg (( Cage (C,n)),k)) by A5, A6, A8, A23, A40, TOPREAL1: 21;

          then (( Cage (C,n)) /. (k + 1)) in {(( Cage (C,n)) /. k)} by A14, A22, A25, A28, A29, A30, A41, A35, A43, A44, NAT_1: 13, XBOOLE_0:def 4;

          then (( Cage (C,n)) /. (k + 1)) = (( Cage (C,n)) /. k) by TARSKI:def 1;

          hence contradiction by A11, A12, A13, A14, A42, GOBOARD1: 5;

        end;

      end;

      

      then ((( Gauge (C,n)) * (i1,j1)) `1 ) = ((( Gauge (C,n)) * (i2,1)) `1 ) by A16, A33, A18, A21, GOBOARD5: 2

      .= ((( Gauge (C,n)) * (i2,j2)) `1 ) by A20, A39, A19, GOBOARD5: 2;

      hence thesis by A7, A12, A14, EUCLID: 52;

    end;

    theorem :: JORDAN1E:21

    for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds for k be Nat st 1 <= k & (k + 1) <= ( len ( Cage (C,n))) & (( Cage (C,n)) /. k) = ( S-max ( L~ ( Cage (C,n)))) holds ((( Cage (C,n)) /. (k + 1)) `2 ) = ( S-bound ( L~ ( Cage (C,n))))

    proof

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

      

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

      

       A2: (( 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 A2, SPRECT_2: 70, XXREAL_0: 2;

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

      then

       A3: (( S-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) > 1 by A2, SPRECT_2: 72, XXREAL_0: 2;

      let k be Nat;

      assume that

       A4: 1 <= k and

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

       A6: (( Cage (C,n)) /. k) = ( S-max ( L~ ( Cage (C,n))));

      

       A7: k < ( len ( Cage (C,n))) by A5, NAT_1: 13;

      then

       A8: k in ( dom ( Cage (C,n))) by A4, FINSEQ_3: 25;

      then

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

      (( S-max ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) <= k by A6, A8, FINSEQ_5: 39;

      then

       A9: k > 1 by A3, XXREAL_0: 2;

      then

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

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

       A11: (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (i1,j1)) and

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

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

       A14: 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, A5, JORDAN8: 3;

      

       A15: 1 <= i1 by A10, MATRIX_0: 32;

      

       A16: j2 <= ( width ( Gauge (C,n))) by A12, MATRIX_0: 32;

      

       A17: 1 <= j2 by A12, MATRIX_0: 32;

      

       A18: j1 <= ( width ( Gauge (C,n))) by A10, MATRIX_0: 32;

      

       A19: (k9 + 1) < ( len ( Cage (C,n))) by A5, NAT_1: 13;

      

       A20: i1 <= ( len ( Gauge (C,n))) by A10, MATRIX_0: 32;

      ((( Gauge (C,n)) * (i1,j1)) `2 ) = ( S-bound ( L~ ( Cage (C,n)))) by A6, A11, EUCLID: 52

      .= ((( Gauge (C,n)) * (i1,1)) `2 ) by A15, A20, JORDAN1A: 72;

      then

       A21: j1 <= 1 by A15, A20, A18, GOBOARD5: 4;

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

      then

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

      then

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

       A23: [i3, j3] in ( Indices ( Gauge (C,n))) and

       A24: (( Cage (C,n)) /. k9) = (( Gauge (C,n)) * (i3,j3)) and

       A25: [i4, j4] in ( Indices ( Gauge (C,n))) and

       A26: (( Cage (C,n)) /. (k9 + 1)) = (( Gauge (C,n)) * (i4,j4)) and

       A27: 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, A7, JORDAN8: 3;

      

       A28: i1 = i4 by A10, A11, A25, A26, GOBOARD1: 5;

      

       A29: j1 = j4 by A10, A11, A25, A26, GOBOARD1: 5;

      

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

      

       A31: i3 <= ( len ( Gauge (C,n))) by A23, MATRIX_0: 32;

      

       A32: 1 <= j1 by A10, MATRIX_0: 32;

      then

       A33: j1 = 1 by A21, XXREAL_0: 1;

      

       A34: i3 = i4

      proof

        assume

         A35: i3 <> i4;

        per cases by A27, A35;

          suppose j3 = j4 & (i3 + 1) = i4;

          hence contradiction by A7, A21, A22, A23, A24, A25, A26, A29, JORDAN10: 3;

        end;

          suppose

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

          k9 < ( len ( Cage (C,n))) by A19, NAT_1: 13;

          then (( Gauge (C,n)) * (i3,j3)) in ( S-most ( L~ ( Cage (C,n)))) by A33, A22, A24, A29, A30, A31, A36, JORDAN1A: 60;

          then

           A37: ((( Gauge (C,n)) * ((i4 + 1),j4)) `1 ) <= ((( Gauge (C,n)) * (i4,j4)) `1 ) by A6, A26, A36, PSCOMP_1: 55;

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

          hence contradiction by A15, A32, A18, A28, A29, A31, A36, A37, GOBOARD5: 3;

        end;

      end;

      

       A38: 1 <= i2 & i2 <= ( len ( Gauge (C,n))) by A12, MATRIX_0: 32;

      

       A39: (k9 + 1) = k;

      

       A40: 1 <= j3 by A23, MATRIX_0: 32;

      j1 = j2

      proof

        assume

         A41: j1 <> j2;

        per cases by A14, A41;

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

          hence contradiction by A17, A21, NAT_1: 13;

        end;

          suppose

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

          (k9 + (1 + 1)) <= ( len ( Cage (C,n))) by A5;

          then

           A43: (( LSeg (( Cage (C,n)),k9)) /\ ( LSeg (( Cage (C,n)),k))) = {(( Cage (C,n)) /. k)} by A22, A39, TOPREAL1:def 6;

          (( Cage (C,n)) /. k9) in ( LSeg (( Cage (C,n)),k9)) & (( Cage (C,n)) /. (k + 1)) in ( LSeg (( Cage (C,n)),k)) by A4, A5, A7, A22, A39, TOPREAL1: 21;

          then (( Cage (C,n)) /. (k + 1)) in {(( Cage (C,n)) /. k)} by A13, A21, A24, A27, A28, A29, A40, A34, A42, A43, NAT_1: 13, XBOOLE_0:def 4;

          then (( Cage (C,n)) /. (k + 1)) = (( Cage (C,n)) /. k) by TARSKI:def 1;

          hence contradiction by A10, A11, A12, A13, A41, GOBOARD1: 5;

        end;

      end;

      

      then ((( Gauge (C,n)) * (i1,j1)) `2 ) = ((( Gauge (C,n)) * (1,j2)) `2 ) by A15, A20, A32, A18, GOBOARD5: 1

      .= ((( Gauge (C,n)) * (i2,j2)) `2 ) by A38, A17, A16, GOBOARD5: 1;

      hence thesis by A6, A11, A13, EUCLID: 52;

    end;

    theorem :: JORDAN1E:22

    for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds for k be Nat st 1 <= k & (k + 1) <= ( len ( Cage (C,n))) & (( Cage (C,n)) /. k) = ( W-min ( L~ ( Cage (C,n)))) holds ((( Cage (C,n)) /. (k + 1)) `1 ) = ( W-bound ( L~ ( Cage (C,n))))

    proof

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

      

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

      

       A2: (( 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 A2, SPRECT_2: 70, XXREAL_0: 2;

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

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

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

      then

       A3: (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) > 1 by A2, SPRECT_2: 74, XXREAL_0: 2;

      let k be Nat;

      assume that

       A4: 1 <= k and

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

       A6: (( Cage (C,n)) /. k) = ( W-min ( L~ ( Cage (C,n))));

      

       A7: k < ( len ( Cage (C,n))) by A5, NAT_1: 13;

      then

       A8: k in ( dom ( Cage (C,n))) by A4, FINSEQ_3: 25;

      then

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

      (( W-min ( L~ ( Cage (C,n)))) .. ( Cage (C,n))) <= k by A6, A8, FINSEQ_5: 39;

      then

       A9: k > 1 by A3, XXREAL_0: 2;

      then

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

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

       A11: (( Cage (C,n)) /. k) = (( Gauge (C,n)) * (i1,j1)) and

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

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

       A14: 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, A5, JORDAN8: 3;

      

       A15: i1 <= ( len ( Gauge (C,n))) by A10, MATRIX_0: 32;

      

       A16: j2 <= ( width ( Gauge (C,n))) by A12, MATRIX_0: 32;

      

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

      

       A18: j1 <= ( width ( Gauge (C,n))) by A10, MATRIX_0: 32;

      

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

      

       A20: i2 <= ( len ( Gauge (C,n))) & 1 <= j2 by A12, MATRIX_0: 32;

      

       A21: (k9 + 1) = k;

      

       A22: (k9 + 1) < ( len ( Cage (C,n))) by A5, NAT_1: 13;

      

       A23: 1 <= j1 by A10, MATRIX_0: 32;

      ((( Gauge (C,n)) * (i1,j1)) `1 ) = ( W-bound ( L~ ( Cage (C,n)))) by A6, A11, EUCLID: 52

      .= ((( Gauge (C,n)) * (1,j1)) `1 ) by A23, A18, A19, JORDAN1A: 73;

      then

       A24: i1 <= 1 by A15, A23, A18, GOBOARD5: 3;

      k >= (1 + 1) by A9, 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 ( Gauge (C,n))) and

       A27: (( Cage (C,n)) /. k9) = (( Gauge (C,n)) * (i3,j3)) and

       A28: [i4, j4] in ( Indices ( Gauge (C,n))) and

       A29: (( Cage (C,n)) /. (k9 + 1)) = (( Gauge (C,n)) * (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, A7, JORDAN8: 3;

      

       A31: i1 = i4 by A10, A11, A28, A29, GOBOARD1: 5;

      

       A32: j1 = j4 by A10, A11, A28, A29, GOBOARD1: 5;

      

       A33: j3 <= ( width ( Gauge (C,n))) by A26, MATRIX_0: 32;

      

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

      

       A35: 1 <= i1 by A10, MATRIX_0: 32;

      then

       A36: i1 = 1 by A24, XXREAL_0: 1;

      

       A37: j3 = j4

      proof

        assume

         A38: j3 <> j4;

        per cases by A30, A38;

          suppose i3 = i4 & j3 = (j4 + 1);

          hence contradiction by A7, A24, A25, A26, A27, A28, A29, A31, JORDAN10: 2;

        end;

          suppose

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

          k9 < ( len ( Cage (C,n))) by A22, NAT_1: 13;

          then (( Gauge (C,n)) * (i3,j3)) in ( W-most ( L~ ( Cage (C,n)))) by A36, A25, A27, A31, A34, A33, A39, JORDAN1A: 59;

          then

           A40: ((( Gauge (C,n)) * (i3,(j3 + 1))) `2 ) <= ((( Gauge (C,n)) * (i3,j3)) `2 ) by A6, A29, A39, PSCOMP_1: 31;

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

          hence contradiction by A35, A15, A18, A31, A32, A34, A39, A40, GOBOARD5: 4;

        end;

      end;

      

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

      i1 = i2

      proof

        assume

         A42: i1 <> i2;

        per cases by A14, A42;

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

          hence contradiction by A17, A24, NAT_1: 13;

        end;

          suppose

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

          (k9 + (1 + 1)) <= ( len ( Cage (C,n))) by A5;

          then

           A44: (( LSeg (( Cage (C,n)),k9)) /\ ( LSeg (( Cage (C,n)),k))) = {(( Cage (C,n)) /. k)} by A25, A21, TOPREAL1:def 6;

          (( Cage (C,n)) /. k9) in ( LSeg (( Cage (C,n)),k9)) & (( Cage (C,n)) /. (k + 1)) in ( LSeg (( Cage (C,n)),k)) by A4, A5, A7, A25, A21, TOPREAL1: 21;

          then (( Cage (C,n)) /. (k + 1)) in {(( Cage (C,n)) /. k)} by A13, A24, A27, A30, A31, A32, A41, A37, A43, A44, NAT_1: 13, XBOOLE_0:def 4;

          then (( Cage (C,n)) /. (k + 1)) = (( Cage (C,n)) /. k) by TARSKI:def 1;

          hence contradiction by A10, A11, A12, A13, A42, GOBOARD1: 5;

        end;

      end;

      

      then ((( Gauge (C,n)) * (i1,j1)) `1 ) = ((( Gauge (C,n)) * (i2,1)) `1 ) by A35, A15, A23, A18, GOBOARD5: 2

      .= ((( Gauge (C,n)) * (i2,j2)) `1 ) by A17, A20, A16, GOBOARD5: 2;

      hence thesis by A6, A11, A13, EUCLID: 52;

    end;