jordan1b.miz



    begin

    reserve E for compact non vertical non horizontal Subset of ( TOP-REAL 2),

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

G for Go-board,

i,j,m,n for Nat,

p for Point of ( TOP-REAL 2);

    theorem :: JORDAN1B:1

    for f be FinSequence holds f is empty iff ( Rev f) is empty

    proof

      let f be FinSequence;

      thus f is empty implies ( Rev f) is empty;

      assume ( Rev f) is empty;

      then

      reconsider g = ( Rev f) as empty FinSequence;

      ( Rev g) is empty;

      hence thesis;

    end;

    theorem :: JORDAN1B:2

    for D be non empty set, f be FinSequence of D holds for i, j st 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f) holds ( mid (f,i,j)) is non empty

    proof

      let D be non empty set, f be FinSequence of D;

      let i, j;

      assume that

       A1: 1 <= i and

       A2: i <= ( len f) and

       A3: 1 <= j and

       A4: j <= ( len f);

      

       A5: j in ( dom f) by A3, A4, FINSEQ_3: 25;

      i in ( dom f) by A1, A2, FINSEQ_3: 25;

      hence thesis by A5, SPRECT_2: 7;

    end;

    theorem :: JORDAN1B:3

    

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

    proof

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

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

      assume that

       A1: 1 <= ( len f) and

       A2: p in ( L~ f);

      

       A3: 1 <= ( Index (p,f)) by A2, JORDAN3: 8;

      

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

      now

        per cases ;

          suppose p <> (f . 1);

          then

           A5: ( R_Cut (f,p)) = (( mid (f,1,( Index (p,f)))) ^ <*p*>) by JORDAN3:def 4;

          

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

          then ( Index (p,f)) in ( dom f) by A3, FINSEQ_3: 25;

          then ( len ( mid (f,1,( Index (p,f))))) >= 1 by A4, SPRECT_2: 5;

          

          hence (( R_Cut (f,p)) . 1) = (( mid (f,1,( Index (p,f)))) . 1) by A5, FINSEQ_6: 109

          .= (f . 1) by A1, A3, A6, FINSEQ_6: 118;

        end;

          suppose

           A7: p = (f . 1);

          then ( R_Cut (f,p)) = <*p*> by JORDAN3:def 4;

          hence thesis by A7, FINSEQ_1: 40;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN1B:4

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

    proof

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

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

       A1: f is being_S-Seq and

       A2: p in ( L~ f);

      ( Rev f) is being_S-Seq by A1;

      then

       A3: 2 <= ( len ( Rev f)) by TOPREAL1:def 8;

      

       A4: p in ( L~ ( Rev f)) by A2, SPPOL_2: 22;

      then ( L_Cut (( Rev ( Rev f)),p)) = ( Rev ( R_Cut (( Rev f),p))) by A1, JORDAN3: 22;

      

      hence (( L_Cut (f,p)) . ( len ( L_Cut (f,p)))) = (( Rev ( R_Cut (( Rev f),p))) . ( len ( R_Cut (( Rev f),p)))) by FINSEQ_5:def 3

      .= (( R_Cut (( Rev f),p)) . 1) by FINSEQ_5: 62

      .= (( Rev f) . 1) by A4, A3, Th3, XXREAL_0: 2

      .= (f . ( len f)) by FINSEQ_5: 62;

    end;

    theorem :: JORDAN1B:5

    for P be Simple_closed_curve holds ( W-max P) <> ( E-max P)

    proof

      let P be Simple_closed_curve;

      now

        

         A1: |[( E-bound P), ( upper_bound ( proj2 | ( E-most P)))]| = ( E-max P) by PSCOMP_1:def 23;

        

         A2: |[( W-bound P), ( upper_bound ( proj2 | ( W-most P)))]| = ( W-max P) by PSCOMP_1:def 20;

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

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

        hence contradiction by TOPREAL5: 17;

      end;

      hence thesis;

    end;

    theorem :: JORDAN1B:6

    for D be non empty set holds for f be FinSequence of D st 1 <= i & i < ( len f) holds (( mid (f,i,(( len f) -' 1))) ^ <*(f /. ( len f))*>) = ( mid (f,i,( len f)))

    proof

      let D be non empty set;

      let f be FinSequence of D;

      assume that

       A1: 1 <= i and

       A2: i < ( len f);

      

       A3: (i + 1) <= ( len f) by A2, NAT_1: 13;

      then

       A4: ((i + 1) - 1) <= (( len f) - 1) by XREAL_1: 9;

      then

       A5: i <= (( len f) -' 1) by XREAL_0:def 2;

      ( 0 + i) <= (( len f) - 1) by A4;

      then ((( len f) - 1) - i) >= 0 by XREAL_1: 19;

      then

       A6: ((( len f) -' 1) - i) >= 0 by A4, XREAL_0:def 2;

      

       A7: (( len f) - i) >= 0 by A3, XREAL_1: 19;

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

      then (( len f) - 1) <= ((( len f) + 1) - 1) by XREAL_1: 9;

      then

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

      

      then

       A9: (( len ( mid (f,i,(( len f) -' 1)))) + 1) = ((((( len f) -' 1) -' i) + 1) + 1) by A1, A5, JORDAN4: 8

      .= ((((( len f) -' 1) - i) + 1) + 1) by A6, XREAL_0:def 2

      .= ((((( len f) - 1) - i) + 1) + 1) by A4, XREAL_0:def 2

      .= ((( len f) -' i) + 1) by A7, XREAL_0:def 2

      .= ( len ( mid (f,i,( len f)))) by A1, A2, JORDAN4: 8;

       A10:

      now

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

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

        then

         A11: ( len f) in ( dom f) by FINSEQ_1:def 3;

        i in ( Seg ( len f)) by A1, A2, FINSEQ_1: 1;

        then

         A12: i in ( dom f) by FINSEQ_1:def 3;

        let j be Nat;

        assume that

         A13: 1 <= j and

         A14: j <= ( len ( mid (f,i,( len f))));

        per cases by A14, XXREAL_0: 1;

          suppose j < ( len ( mid (f,i,( len f))));

          then

           A15: j <= ( len ( mid (f,i,(( len f) -' 1)))) by A9, NAT_1: 13;

          then j in ( Seg ( len ( mid (f,i,(( len f) -' 1))))) by A13, FINSEQ_1: 1;

          then

           A16: j in ( dom ( mid (f,i,(( len f) -' 1)))) by FINSEQ_1:def 3;

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

          then (( len f) -' 1) in ( Seg ( len f)) by A8, FINSEQ_1: 1;

          then

           A17: (( len f) -' 1) in ( dom f) by FINSEQ_1:def 3;

          j in ( Seg ( len ( mid (f,i,( len f))))) by A13, A14, FINSEQ_1: 1;

          then

           A18: j in ( dom ( mid (f,i,( len f)))) by FINSEQ_1:def 3;

          j in NAT by ORDINAL1:def 12;

          

          hence ((( mid (f,i,(( len f) -' 1))) ^ <*(f /. ( len f))*>) /. j) = (( mid (f,i,(( len f) -' 1))) /. j) by A13, A15, BOOLMARK: 7

          .= (f /. ((j + i) -' 1)) by A5, A12, A16, A17, SPRECT_2: 3

          .= (( mid (f,i,( len f))) /. j) by A2, A12, A11, A18, SPRECT_2: 3;

        end;

          suppose

           A19: j = ( len ( mid (f,i,( len f))));

          

          hence ((( mid (f,i,(( len f) -' 1))) ^ <*(f /. ( len f))*>) /. j) = (f /. ( len f)) by A9, FINSEQ_4: 67

          .= (( mid (f,i,( len f))) /. j) by A12, A11, A19, SPRECT_2: 9;

        end;

      end;

      ( len (( mid (f,i,(( len f) -' 1))) ^ <*(f /. ( len f))*>)) = (( len ( mid (f,i,(( len f) -' 1)))) + 1) by FINSEQ_2: 16;

      hence thesis by A9, A10, FINSEQ_5: 13;

    end;

    theorem :: JORDAN1B:7

    for p,q be Point of ( TOP-REAL 2) st p <> q & ( LSeg (p,q)) is vertical holds <*p, q*> is being_S-Seq

    proof

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

      assume that

       A1: p <> q and

       A2: ( LSeg (p,q)) is vertical;

      (p `1 ) = (q `1 ) by A2, SPPOL_1: 16;

      hence thesis by A1, SPPOL_2: 43;

    end;

    theorem :: JORDAN1B:8

    for p,q be Point of ( TOP-REAL 2) st p <> q & ( LSeg (p,q)) is horizontal holds <*p, q*> is being_S-Seq

    proof

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

      assume that

       A1: p <> q and

       A2: ( LSeg (p,q)) is horizontal;

      (p `2 ) = (q `2 ) by A2, SPPOL_1: 15;

      hence thesis by A1, SPPOL_2: 43;

    end;

    theorem :: JORDAN1B:9

    

     Th9: for p,q be FinSequence of ( TOP-REAL 2) holds for v be Point of ( TOP-REAL 2) st p is_in_the_area_of q holds ( Rotate (p,v)) is_in_the_area_of q

    proof

      let p,q be FinSequence of ( TOP-REAL 2);

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

      assume

       A1: p is_in_the_area_of q;

      per cases ;

        suppose

         A2: v in ( rng p);

        now

          let n;

          assume n in ( dom ( Rotate (p,v)));

          then n in ( dom p) by FINSEQ_6: 180;

          then

           A3: n in ( Seg ( len p)) by FINSEQ_1:def 3;

          then

           A4: n <= ( len p) by FINSEQ_1: 1;

          

           A5: ( 0 + 1) <= n by A3, FINSEQ_1: 1;

          then

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

          per cases ;

            suppose

             A7: n <= ( len (p :- v));

            then n <= ((( len p) - (v .. p)) + 1) by A2, FINSEQ_5: 50;

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

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

            then

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

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

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

            then ((n -' 1) + (v .. p)) in ( Seg ( len p)) by A8, FINSEQ_1: 1;

            then

             A9: ((n -' 1) + (v .. p)) in ( dom p) by FINSEQ_1:def 3;

            

             A10: (( Rotate (p,v)) /. n) = (p /. ((n -' 1) + (v .. p))) by A2, A5, A7, FINSEQ_6: 174;

            hence ( W-bound ( L~ q)) <= ((( Rotate (p,v)) /. n) `1 ) by A1, A9, SPRECT_2:def 1;

            thus ((( Rotate (p,v)) /. n) `1 ) <= ( E-bound ( L~ q)) by A1, A10, A9, SPRECT_2:def 1;

            thus ( S-bound ( L~ q)) <= ((( Rotate (p,v)) /. n) `2 ) by A1, A10, A9, SPRECT_2:def 1;

            thus ((( Rotate (p,v)) /. n) `2 ) <= ( N-bound ( L~ q)) by A1, A10, A9, SPRECT_2:def 1;

          end;

            suppose

             A11: n > ( len (p :- v));

            then n > ((( len p) - (v .. p)) + 1) by A2, FINSEQ_5: 50;

            then n > ((1 + ( len p)) - (v .. p));

            then (n + (v .. p)) > (1 + ( len p)) by XREAL_1: 19;

            then ((n + (v .. p)) - ( len p)) > 1 by XREAL_1: 20;

            then

             A12: 1 <= ((n + (v .. p)) -' ( len p)) by XREAL_0:def 2;

            (v .. p) <= ( len p) by A2, FINSEQ_4: 21;

            then (n + (v .. p)) <= (( len p) + ( len p)) by A4, XREAL_1: 7;

            then ((n + (v .. p)) - ( len p)) <= ( len p) by XREAL_1: 20;

            then ((n + (v .. p)) -' ( len p)) <= ( len p) by XREAL_0:def 2;

            then ((n + (v .. p)) -' ( len p)) in ( Seg ( len p)) by A12, FINSEQ_1: 1;

            then

             A13: ((n + (v .. p)) -' ( len p)) in ( dom p) by FINSEQ_1:def 3;

            

             A14: (( Rotate (p,v)) /. n) = (p /. ((n + (v .. p)) -' ( len p))) by A2, A4, A11, FINSEQ_6: 177;

            hence ( W-bound ( L~ q)) <= ((( Rotate (p,v)) /. n) `1 ) by A1, A13, SPRECT_2:def 1;

            thus ((( Rotate (p,v)) /. n) `1 ) <= ( E-bound ( L~ q)) by A1, A14, A13, SPRECT_2:def 1;

            thus ( S-bound ( L~ q)) <= ((( Rotate (p,v)) /. n) `2 ) by A1, A14, A13, SPRECT_2:def 1;

            thus ((( Rotate (p,v)) /. n) `2 ) <= ( N-bound ( L~ q)) by A1, A14, A13, SPRECT_2:def 1;

          end;

        end;

        hence thesis by SPRECT_2:def 1;

      end;

        suppose not v in ( rng p);

        hence thesis by A1, FINSEQ_6:def 2;

      end;

    end;

    theorem :: JORDAN1B:10

    for p be non trivial FinSequence of ( TOP-REAL 2) holds for v be Point of ( TOP-REAL 2) holds ( Rotate (p,v)) is_in_the_area_of p by Th9, SPRECT_2: 21;

    theorem :: JORDAN1B:11

    

     Th11: for f be FinSequence holds ( Center f) >= 1

    proof

      let f be FinSequence;

      ((( len f) div 2) + 1) >= ( 0 + 1) by XREAL_1: 6;

      hence thesis by JORDAN1A:def 1;

    end;

    theorem :: JORDAN1B:12

    for f be FinSequence st ( len f) >= 1 holds ( Center f) <= ( len f)

    proof

      let f be FinSequence;

      assume ( len f) >= 1;

      then ( 0 + ( len f)) < (( len f) + ( len f)) by XREAL_1: 6;

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

      then (((( len f) + 1) + 1) div 2) <= ( len f) by NAT_2: 25;

      then ((( len f) + (1 + 1)) div 2) <= ( len f);

      then ((( len f) div 2) + 1) <= ( len f) by NAT_2: 14;

      hence thesis by JORDAN1A:def 1;

    end;

    theorem :: JORDAN1B:13

    

     Th13: ( Center G) <= ( len G)

    proof

       0 < ( len G) by GOBRD11: 34;

      then

       A1: (( len G) div 2 qua Integer) < ( len G) by INT_1: 56;

      ( Center G) = ((( len G) div 2) + 1) by JORDAN1A:def 1;

      hence thesis by A1, NAT_1: 13;

    end;

    theorem :: JORDAN1B:14

    

     Th14: for f be FinSequence st ( len f) >= 2 holds ( Center f) > 1

    proof

      let f be FinSequence;

      assume ( len f) >= 2;

      then (( len f) div 2) >= 1 by NAT_2: 13;

      then ((( len f) div 2) + 1) > 1 by NAT_1: 13;

      hence thesis by JORDAN1A:def 1;

    end;

    theorem :: JORDAN1B:15

    

     Th15: for f be FinSequence st ( len f) >= 3 holds ( Center f) < ( len f)

    proof

      let f be FinSequence;

      assume ( len f) >= 3;

      then (( len f) + (2 + 1)) <= (( len f) + ( len f)) by XREAL_1: 6;

      then ((( len f) + 2) + 1) <= (2 * ( len f));

      then ((((( len f) + 2) + 1) + 1) div 2) <= ( len f) by NAT_2: 25;

      then (((( len f) + 2) + (1 + 1)) div 2) <= ( len f);

      then (((( len f) + 2) div 2) + 1) <= ( len f) by NAT_2: 14;

      then ((( len f) + 2) div 2) < ( len f) by NAT_1: 13;

      then ((( len f) div 2) + 1) < ( len f) by NAT_2: 14;

      hence thesis by JORDAN1A:def 1;

    end;

     Lm1:

    now

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

      

      thus (( len ( Gauge (E, 0 ))) -' 1) = (((2 |^ 0 ) + 3) -' 1) by JORDAN8:def 1

      .= ((1 + 3) -' 1) by NEWTON: 4

      .= 3 by NAT_D: 34;

    end;

    theorem :: JORDAN1B:16

    ( Center ( Gauge (E,n))) = ((2 |^ (n -' 1)) + 2)

    proof

      reconsider n as Nat;

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

      per cases ;

        suppose

         A1: n = 0 ;

        

         A2: 4 = ((2 * 2) + 0 );

        

         A3: ( 0 - 1) < 0 ;

        ( Center G) = ((( len G) div 2) + 1) by JORDAN1A:def 1;

        

        then ( Center G) = ((((2 |^ 0 ) + 3) div 2) + 1) by A1, JORDAN8:def 1

        .= (((1 + 3) div 2) + 1) by NEWTON: 4

        .= ((1 + 1) + 1) by A2, NAT_D:def 1

        .= (((2 |^ 0 ) + 1) + 1) by NEWTON: 4

        .= (((2 |^ ( 0 -' 1)) + 1) + 1) by A3, XREAL_0:def 2

        .= ((2 |^ (n -' 1)) + 2) by A1;

        hence thesis;

      end;

        suppose

         A4: n > 0 ;

        then

         A5: ( 0 + 1) <= n by NAT_1: 13;

        

         A6: ((2 |^ n) div 2) = ((2 |^ n) / 2) by A4, PEPIN: 64

        .= ((2 |^ n) / (2 |^ 1))

        .= (2 |^ (n -' 1)) by A5, TOPREAL6: 10;

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

        then

         A7: (3 div 2) = 1 by NAT_D:def 1;

        

         A8: ((2 |^ n) mod 2) = 0 by A4, PEPIN: 36;

        ((( len G) div 2) + 1) = ((((2 |^ n) + 3) div 2) + 1) by JORDAN8:def 1

        .= ((((2 |^ n) div 2) + (3 div 2)) + 1) by A8, NAT_D: 19

        .= (((2 |^ n) div 2) + (1 + 1)) by A7;

        hence thesis by A6, JORDAN1A:def 1;

      end;

    end;

    theorem :: JORDAN1B:17

    

     Th17: E c= ( cell (( Gauge (E, 0 )),2,2))

    proof

      set G = ( Gauge (E, 0 ));

      let x be object;

      

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

      assume

       A2: x in E;

      then

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

      

       A3: 4 <= ( len G) by JORDAN8: 10;

      then

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

      then ((G * (1,2)) `2 ) = ( S-bound E) by JORDAN8: 13;

      then

       A5: ((G * (1,2)) `2 ) <= (x `2 ) by A2, PSCOMP_1: 24;

      2 < ( len G) by A3, XXREAL_0: 2;

      then

       A6: ( cell (G,2,2)) = { |[p, q]| where p,q be Real : ((G * (2,1)) `1 ) <= p & p <= ((G * ((2 + 1),1)) `1 ) & ((G * (1,2)) `2 ) <= q & q <= ((G * (1,(2 + 1))) `2 ) } by A1, GOBRD11: 32;

      ((G * (2,1)) `1 ) = ( W-bound E) by A4, JORDAN8: 11;

      then

       A7: ((G * (2,1)) `1 ) <= (x `1 ) by A2, PSCOMP_1: 24;

      

       A8: (( len G) -' 1) = 3 by Lm1;

      then ((G * ((2 + 1),1)) `1 ) = ( E-bound E) by A4, JORDAN8: 12;

      then

       A9: (x `1 ) <= ((G * ((2 + 1),1)) `1 ) by A2, PSCOMP_1: 24;

      ((G * (1,(2 + 1))) `2 ) = ( N-bound E) by A8, A4, JORDAN8: 14;

      then

       A10: (x `2 ) <= ((G * (1,(2 + 1))) `2 ) by A2, PSCOMP_1: 24;

      x = |[(x `1 ), (x `2 )]| by EUCLID: 53;

      hence thesis by A7, A9, A5, A10, A6;

    end;

    theorem :: JORDAN1B:18

    

     Th18: not ( cell (( Gauge (E, 0 )),2,2)) c= ( BDD E)

    proof

      assume

       A1: ( cell (( Gauge (E, 0 )),2,2)) c= ( BDD E);

      E c= ( cell (( Gauge (E, 0 )),2,2)) by Th17;

      then

       A2: E c= ( BDD E) by A1;

      set e = the Element of E;

      

       A3: ( BDD E) misses E by JORDAN1A: 7;

      e in E;

      hence thesis by A2, A3, XBOOLE_0: 3;

    end;

    theorem :: JORDAN1B:19

    (( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)) = |[((( W-bound C) + ( E-bound C)) / 2), ( S-bound ( L~ ( Cage (C,1))))]|

    proof

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

      1 <= ( len G) by GOBRD11: 34;

      then

       A1: ((G * (( Center G),1)) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by JORDAN1A: 38;

      ( Center G) <= ( len G) by Th13;

      then ((G * (( Center G),1)) `2 ) = ( S-bound ( L~ ( Cage (C,1)))) by Th11, JORDAN1A: 72;

      hence thesis by A1, EUCLID: 53;

    end;

    theorem :: JORDAN1B:20

    (( Gauge (C,1)) * (( Center ( Gauge (C,1))),( len ( Gauge (C,1))))) = |[((( W-bound C) + ( E-bound C)) / 2), ( N-bound ( L~ ( Cage (C,1))))]|

    proof

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

      1 <= ( len G) by GOBRD11: 34;

      then

       A1: ((G * (( Center G),( len G))) `1 ) = ((( W-bound C) + ( E-bound C)) / 2) by JORDAN1A: 38;

      1 <= ( Center G) by Th11;

      then ((G * (( Center G),( len G))) `2 ) = ( N-bound ( L~ ( Cage (C,1)))) by Th13, JORDAN1A: 70;

      hence thesis by A1, EUCLID: 53;

    end;

    

     Lm2: i <= m & m <= (i + 1) implies i = m or i = (m -' 1)

    proof

      assume that

       A1: i <= m and

       A2: m <= (i + 1) and

       A3: i <> m;

      i < m by A1, A3, XXREAL_0: 1;

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

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

      hence thesis by NAT_D: 34;

    end;

    theorem :: JORDAN1B:21

    

     Th21: 1 <= j & j < ( width G) & 1 <= m & m <= ( len G) & 1 <= n & n <= ( width G) & p in ( cell (G,( len G),j)) & (p `1 ) = ((G * (m,n)) `1 ) implies ( len G) = m

    proof

      assume that

       A1: 1 <= j and

       A2: j < ( width G) and

       A3: 1 <= m and

       A4: m <= ( len G) and

       A5: 1 <= n and

       A6: n <= ( width G) and

       A7: p in ( cell (G,( len G),j)) and

       A8: (p `1 ) = ((G * (m,n)) `1 );

      

       A9: ((G * (m,1)) `1 ) = ((G * (m,n)) `1 ) by A3, A4, A5, A6, GOBOARD5: 2;

      

       A10: ( cell (G,( len G),j)) = { |[r, s]| where r,s be Real : ((G * (( len G),1)) `1 ) <= r & ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } by A1, A2, GOBRD11: 29;

      

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

      consider r,s be Real such that

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

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

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

      then ( len G) <= m by A3, A8, A11, A9, A13, GOBOARD5: 3;

      hence thesis by A4, XXREAL_0: 1;

    end;

    theorem :: JORDAN1B:22

    1 <= i & i <= ( len G) & 1 <= j & j < ( width G) & 1 <= m & m <= ( len G) & 1 <= n & n <= ( width G) & p in ( cell (G,i,j)) & (p `1 ) = ((G * (m,n)) `1 ) implies i = m or i = (m -' 1)

    proof

      assume that

       A1: 1 <= i and

       A2: i <= ( len G) and

       A3: 1 <= j and

       A4: j < ( width G) and

       A5: 1 <= m and

       A6: m <= ( len G) and

       A7: 1 <= n and

       A8: n <= ( width G) and

       A9: p in ( cell (G,i,j)) and

       A10: (p `1 ) = ((G * (m,n)) `1 );

      

       A11: ((G * (m,1)) `1 ) = ((G * (m,n)) `1 ) by A5, A6, A7, A8, GOBOARD5: 2;

      

       A12: 1 <= ( width G) by A3, A4, XXREAL_0: 2;

      per cases by A2, XXREAL_0: 1;

        suppose i = ( len G);

        hence thesis by A3, A4, A5, A6, A7, A8, A9, A10, Th21;

      end;

        suppose i < ( len G);

        then ( 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 A1, A3, A4, GOBRD11: 32;

        then

        consider r,s be Real such that

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

         A14: ((G * (i,1)) `1 ) <= r and

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

        

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

        i <= m & m <= (i + 1)

        proof

          assume

           A17: not thesis;

          per cases by A17;

            suppose i > m;

            hence contradiction by A2, A5, A10, A12, A11, A14, A16, GOBOARD5: 3;

          end;

            suppose

             A18: m > (i + 1);

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

            hence contradiction by A6, A10, A12, A11, A15, A16, A18, GOBOARD5: 3;

          end;

        end;

        hence thesis by Lm2;

      end;

    end;

    theorem :: JORDAN1B:23

    

     Th23: 1 <= i & i < ( len G) & 1 <= m & m <= ( len G) & 1 <= n & n <= ( width G) & p in ( cell (G,i,( width G))) & (p `2 ) = ((G * (m,n)) `2 ) implies ( width G) = n

    proof

      assume that

       A1: 1 <= i and

       A2: i < ( len G) and

       A3: 1 <= m and

       A4: m <= ( len G) and

       A5: 1 <= n and

       A6: n <= ( width G) and

       A7: p in ( cell (G,i,( width G))) and

       A8: (p `2 ) = ((G * (m,n)) `2 );

      

       A9: ((G * (1,n)) `2 ) = ((G * (m,n)) `2 ) by A3, A4, A5, A6, GOBOARD5: 1;

      

       A10: ( cell (G,i,( width G))) = { |[r, s]| where r,s be Real : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) & ((G * (1,( width G))) `2 ) <= s } by A1, A2, GOBRD11: 31;

      

       A11: 1 <= ( len G) by A1, A2, XXREAL_0: 2;

      consider r,s be Real such that

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

       A13: ((G * (1,( width G))) `2 ) <= s by A7, A10;

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

      then ( width G) <= n by A5, A8, A11, A9, A13, GOBOARD5: 4;

      hence thesis by A6, XXREAL_0: 1;

    end;

    theorem :: JORDAN1B:24

    1 <= i & i < ( len G) & 1 <= j & j <= ( width G) & 1 <= m & m <= ( len G) & 1 <= n & n <= ( width G) & p in ( cell (G,i,j)) & (p `2 ) = ((G * (m,n)) `2 ) implies j = n or j = (n -' 1)

    proof

      assume that

       A1: 1 <= i and

       A2: i < ( len G) and

       A3: 1 <= j and

       A4: j <= ( width G) and

       A5: 1 <= m and

       A6: m <= ( len G) and

       A7: 1 <= n and

       A8: n <= ( width G) and

       A9: p in ( cell (G,i,j)) and

       A10: (p `2 ) = ((G * (m,n)) `2 );

      

       A11: ((G * (1,n)) `2 ) = ((G * (m,n)) `2 ) by A5, A6, A7, A8, GOBOARD5: 1;

      

       A12: 1 <= ( len G) by A1, A2, XXREAL_0: 2;

      per cases by A4, XXREAL_0: 1;

        suppose j = ( width G);

        hence thesis by A1, A2, A5, A6, A7, A8, A9, A10, Th23;

      end;

        suppose j < ( width G);

        then ( 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 A1, A2, A3, GOBRD11: 32;

        then

        consider r,s be Real such that

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

         A14: ((G * (1,j)) `2 ) <= s and

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

        

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

        j <= n & n <= (j + 1)

        proof

          assume

           A17: not thesis;

          per cases by A17;

            suppose j > n;

            hence contradiction by A4, A7, A10, A12, A11, A14, A16, GOBOARD5: 4;

          end;

            suppose

             A18: n > (j + 1);

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

            hence contradiction by A8, A10, A12, A11, A15, A16, A18, GOBOARD5: 4;

          end;

        end;

        hence thesis by Lm2;

      end;

    end;

    theorem :: JORDAN1B:25

    

     Th25: for C be Simple_closed_curve holds for i be Nat st 1 < i & i < ( len ( Gauge (C,n))) holds ( LSeg ((( Gauge (C,n)) * (i,1)),(( Gauge (C,n)) * (i,( len ( Gauge (C,n))))))) meets ( Upper_Arc C)

    proof

      let C be Simple_closed_curve;

      let i be Nat;

      assume that

       A1: 1 < i and

       A2: i < ( len ( Gauge (C,n)));

      set r = ((( Gauge (C,n)) * (i,2)) `1 );

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

      then

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

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

      then

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

      

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

      then

       A6: (( Gauge (C,n)) * (i,2)) in ( LSeg ((( Gauge (C,n)) * (i,1)),(( Gauge (C,n)) * (i,( len ( Gauge (C,n))))))) by A1, A2, A3, JORDAN1A: 16;

      

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

      then

       A8: (( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) in ( LSeg ((( Gauge (C,n)) * (i,1)),(( Gauge (C,n)) * (i,( len ( Gauge (C,n))))))) by A1, A2, A5, A4, JORDAN1A: 16;

      

       A9: r = ((( Gauge (C,n)) * (i,1)) `1 ) by A1, A2, A5, A3, GOBOARD5: 2

      .= ((( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) `1 ) by A1, A2, A5, A4, A7, GOBOARD5: 2;

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

      then ((( Gauge (C,n)) * (2,2)) `1 ) <= r by A2, A5, A3, SPRECT_3: 13;

      then

       A10: ( W-bound C) <= r by A3, JORDAN8: 11;

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

      then i <= (( len ( Gauge (C,n))) - 1) by XREAL_1: 19;

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

      then r <= ((( Gauge (C,n)) * ((( len ( Gauge (C,n))) -' 1),(( len ( Gauge (C,n))) -' 1))) `1 ) by A1, A5, A4, A7, A9, SPRECT_3: 13;

      then

       A11: r <= ( E-bound C) by A4, JORDAN8: 12, NAT_D: 35;

      

       A12: (( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) = |[((( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) `1 ), ((( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) `2 )]| by EUCLID: 53

      .= |[((( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) `1 ), ( N-bound C)]| by A1, A2, JORDAN8: 14;

      (( Gauge (C,n)) * (i,2)) = |[((( Gauge (C,n)) * (i,2)) `1 ), ((( Gauge (C,n)) * (i,2)) `2 )]| by EUCLID: 53

      .= |[((( Gauge (C,n)) * (i,2)) `1 ), ( S-bound C)]| by A1, A2, JORDAN8: 13;

      then ( LSeg ((( Gauge (C,n)) * (i,2)),(( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))))) meets ( Upper_Arc C) by A12, A9, A10, A11, JORDAN6: 69;

      hence thesis by A6, A8, TOPREAL1: 6, XBOOLE_1: 63;

    end;

    theorem :: JORDAN1B:26

    

     Th26: for C be Simple_closed_curve holds for i be Nat st 1 < i & i < ( len ( Gauge (C,n))) holds ( LSeg ((( Gauge (C,n)) * (i,1)),(( Gauge (C,n)) * (i,( len ( Gauge (C,n))))))) meets ( Lower_Arc C)

    proof

      let C be Simple_closed_curve;

      let i be Nat;

      assume that

       A1: 1 < i and

       A2: i < ( len ( Gauge (C,n)));

      set r = ((( Gauge (C,n)) * (i,2)) `1 );

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

      then

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

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

      then

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

      

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

      then

       A6: (( Gauge (C,n)) * (i,2)) in ( LSeg ((( Gauge (C,n)) * (i,1)),(( Gauge (C,n)) * (i,( len ( Gauge (C,n))))))) by A1, A2, A3, JORDAN1A: 16;

      

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

      then

       A8: (( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) in ( LSeg ((( Gauge (C,n)) * (i,1)),(( Gauge (C,n)) * (i,( len ( Gauge (C,n))))))) by A1, A2, A5, A4, JORDAN1A: 16;

      

       A9: r = ((( Gauge (C,n)) * (i,1)) `1 ) by A1, A2, A5, A3, GOBOARD5: 2

      .= ((( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) `1 ) by A1, A2, A5, A4, A7, GOBOARD5: 2;

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

      then ((( Gauge (C,n)) * (2,2)) `1 ) <= r by A2, A5, A3, SPRECT_3: 13;

      then

       A10: ( W-bound C) <= r by A3, JORDAN8: 11;

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

      then i <= (( len ( Gauge (C,n))) - 1) by XREAL_1: 19;

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

      then r <= ((( Gauge (C,n)) * ((( len ( Gauge (C,n))) -' 1),(( len ( Gauge (C,n))) -' 1))) `1 ) by A1, A5, A4, A7, A9, SPRECT_3: 13;

      then

       A11: r <= ( E-bound C) by A4, JORDAN8: 12, NAT_D: 35;

      

       A12: (( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) = |[((( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) `1 ), ((( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) `2 )]| by EUCLID: 53

      .= |[((( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))) `1 ), ( N-bound C)]| by A1, A2, JORDAN8: 14;

      (( Gauge (C,n)) * (i,2)) = |[((( Gauge (C,n)) * (i,2)) `1 ), ((( Gauge (C,n)) * (i,2)) `2 )]| by EUCLID: 53

      .= |[((( Gauge (C,n)) * (i,2)) `1 ), ( S-bound C)]| by A1, A2, JORDAN8: 13;

      then ( LSeg ((( Gauge (C,n)) * (i,2)),(( Gauge (C,n)) * (i,(( len ( Gauge (C,n))) -' 1))))) meets ( Lower_Arc C) by A12, A9, A10, A11, JORDAN6: 70;

      hence thesis by A6, A8, TOPREAL1: 6, XBOOLE_1: 63;

    end;

    theorem :: JORDAN1B:27

    for C be Simple_closed_curve holds ( LSeg ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),1)),(( Gauge (C,n)) * (( Center ( Gauge (C,n))),( len ( Gauge (C,n))))))) meets ( Upper_Arc C)

    proof

      let C be Simple_closed_curve;

      

       A1: 4 <= ( len ( Gauge (C,n))) by JORDAN8: 10;

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

      then

       A2: 1 < ( Center ( Gauge (C,n))) by Th14;

      ( len ( Gauge (C,n))) >= 3 by A1, XXREAL_0: 2;

      hence thesis by A2, Th15, Th25;

    end;

    theorem :: JORDAN1B:28

    for C be Simple_closed_curve holds ( LSeg ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),1)),(( Gauge (C,n)) * (( Center ( Gauge (C,n))),( len ( Gauge (C,n))))))) meets ( Lower_Arc C)

    proof

      let C be Simple_closed_curve;

      

       A1: 4 <= ( len ( Gauge (C,n))) by JORDAN8: 10;

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

      then

       A2: 1 < ( Center ( Gauge (C,n))) by Th14;

      ( len ( Gauge (C,n))) >= 3 by A1, XXREAL_0: 2;

      hence thesis by A2, Th15, Th26;

    end;

    theorem :: JORDAN1B:29

    

     Th29: for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds for i be Nat st 1 <= i & i <= ( len ( Gauge (C,n))) holds ( LSeg ((( Gauge (C,n)) * (i,1)),(( Gauge (C,n)) * (i,( len ( Gauge (C,n))))))) meets ( Upper_Arc ( L~ ( Cage (C,n))))

    proof

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

      let i be Nat;

      assume that

       A1: 1 <= i and

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

      

       A3: (( Gauge (C,n)) * (i,1)) = |[((( Gauge (C,n)) * (i,1)) `1 ), ((( Gauge (C,n)) * (i,1)) `2 )]| by EUCLID: 53

      .= |[((( Gauge (C,n)) * (i,1)) `1 ), ( S-bound ( L~ ( Cage (C,n))))]| by A1, A2, JORDAN1A: 72;

      

       A4: (( Gauge (C,n)) * (i,( len ( Gauge (C,n))))) = |[((( Gauge (C,n)) * (i,( len ( Gauge (C,n))))) `1 ), ((( Gauge (C,n)) * (i,( len ( Gauge (C,n))))) `2 )]| by EUCLID: 53

      .= |[((( Gauge (C,n)) * (i,( len ( Gauge (C,n))))) `1 ), ( N-bound ( L~ ( Cage (C,n))))]| by A1, A2, JORDAN1A: 70;

      set r = ((( Gauge (C,n)) * (i,1)) `1 );

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

      then

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

      

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

      then ((( Gauge (C,n)) * (1,1)) `1 ) <= r by A1, A2, A5, SPRECT_3: 13;

      then

       A7: ( W-bound ( L~ ( Cage (C,n)))) <= r by A5, JORDAN1A: 73;

      r <= ((( Gauge (C,n)) * (( len ( Gauge (C,n))),1)) `1 ) by A1, A2, A6, A5, SPRECT_3: 13;

      then

       A8: r <= ( E-bound ( L~ ( Cage (C,n)))) by A5, JORDAN1A: 71;

      r = ((( Gauge (C,n)) * (i,( len ( Gauge (C,n))))) `1 ) by A1, A2, A6, A5, GOBOARD5: 2;

      hence thesis by A3, A4, A7, A8, JORDAN6: 69;

    end;

    theorem :: JORDAN1B:30

    

     Th30: for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds for i be Nat st 1 <= i & i <= ( len ( Gauge (C,n))) holds ( LSeg ((( Gauge (C,n)) * (i,1)),(( Gauge (C,n)) * (i,( len ( Gauge (C,n))))))) meets ( Lower_Arc ( L~ ( Cage (C,n))))

    proof

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

      let i be Nat;

      assume that

       A1: 1 <= i and

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

      

       A3: (( Gauge (C,n)) * (i,1)) = |[((( Gauge (C,n)) * (i,1)) `1 ), ((( Gauge (C,n)) * (i,1)) `2 )]| by EUCLID: 53

      .= |[((( Gauge (C,n)) * (i,1)) `1 ), ( S-bound ( L~ ( Cage (C,n))))]| by A1, A2, JORDAN1A: 72;

      

       A4: (( Gauge (C,n)) * (i,( len ( Gauge (C,n))))) = |[((( Gauge (C,n)) * (i,( len ( Gauge (C,n))))) `1 ), ((( Gauge (C,n)) * (i,( len ( Gauge (C,n))))) `2 )]| by EUCLID: 53

      .= |[((( Gauge (C,n)) * (i,( len ( Gauge (C,n))))) `1 ), ( N-bound ( L~ ( Cage (C,n))))]| by A1, A2, JORDAN1A: 70;

      set r = ((( Gauge (C,n)) * (i,1)) `1 );

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

      then

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

      

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

      then ((( Gauge (C,n)) * (1,1)) `1 ) <= r by A1, A2, A5, SPRECT_3: 13;

      then

       A7: ( W-bound ( L~ ( Cage (C,n)))) <= r by A5, JORDAN1A: 73;

      r <= ((( Gauge (C,n)) * (( len ( Gauge (C,n))),1)) `1 ) by A1, A2, A6, A5, SPRECT_3: 13;

      then

       A8: r <= ( E-bound ( L~ ( Cage (C,n)))) by A5, JORDAN1A: 71;

      r = ((( Gauge (C,n)) * (i,( len ( Gauge (C,n))))) `1 ) by A1, A2, A6, A5, GOBOARD5: 2;

      hence thesis by A3, A4, A7, A8, JORDAN6: 70;

    end;

    theorem :: JORDAN1B:31

    for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds ( LSeg ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),1)),(( Gauge (C,n)) * (( Center ( Gauge (C,n))),( len ( Gauge (C,n))))))) meets ( Upper_Arc ( L~ ( Cage (C,n))))

    proof

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

      

       A1: 4 <= ( len ( Gauge (C,n))) by JORDAN8: 10;

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

      then

       A2: ( Center ( Gauge (C,n))) < ( len ( Gauge (C,n))) by Th15;

      ( len ( Gauge (C,n))) >= 2 by A1, XXREAL_0: 2;

      then 1 < ( Center ( Gauge (C,n))) by Th14;

      hence thesis by A2, Th29;

    end;

    theorem :: JORDAN1B:32

    for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds ( LSeg ((( Gauge (C,n)) * (( Center ( Gauge (C,n))),1)),(( Gauge (C,n)) * (( Center ( Gauge (C,n))),( len ( Gauge (C,n))))))) meets ( Lower_Arc ( L~ ( Cage (C,n))))

    proof

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

      

       A1: 4 <= ( len ( Gauge (C,n))) by JORDAN8: 10;

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

      then

       A2: ( Center ( Gauge (C,n))) < ( len ( Gauge (C,n))) by Th15;

      ( len ( Gauge (C,n))) >= 2 by A1, XXREAL_0: 2;

      then 1 < ( Center ( Gauge (C,n))) by Th14;

      hence thesis by A2, Th30;

    end;

    theorem :: JORDAN1B:33

    

     Th33: j <= ( width G) implies not ( cell (G, 0 ,j)) is bounded

    proof

      assume

       A1: j <= ( width G);

      per cases by A1, NAT_1: 14, XXREAL_0: 1;

        suppose j = 0 ;

        then

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

         not ex r be Real st for q be Point of ( TOP-REAL 2) st q in ( cell (G, 0 ,j)) holds |.q.| < r

        proof

          let r be Real;

          take q = |[( min (( - r),((G * (1,1)) `1 ))), ( min (( - r),((G * (1,1)) `2 )))]|;

          

           A3: ( min (( - r),((G * (1,1)) `2 ))) <= ((G * (1,1)) `2 ) by XXREAL_0: 17;

          ( min (( - r),((G * (1,1)) `1 ))) <= ((G * (1,1)) `1 ) by XXREAL_0: 17;

          hence q in ( cell (G, 0 ,j)) by A2, A3;

          

           A4: |.(q `1 ).| <= |.q.| by JGRAPH_1: 33;

          per cases ;

            suppose r <= 0 ;

            hence thesis;

          end;

            suppose

             A5: r > 0 ;

            (q `1 ) = ( min (( - r),((G * (1,1)) `1 ))) by EUCLID: 52;

            then

             A6: |.( - r).| <= |.(q `1 ).| by A5, TOPREAL6: 3, XXREAL_0: 17;

            ( - ( - r)) > 0 by A5;

            then ( - r) < 0 ;

            then ( - ( - r)) <= |.(q `1 ).| by A6, ABSVALUE:def 1;

            hence thesis by A4, XXREAL_0: 2;

          end;

        end;

        hence thesis by JORDAN2C: 34;

      end;

        suppose

         A7: j >= 1 & j < ( width G);

        then

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

         not ex r be Real st for q be Point of ( TOP-REAL 2) st q in ( cell (G, 0 ,j)) holds |.q.| < r

        proof

          ( len G) <> 0 by MATRIX_0:def 10;

          then

           A9: 1 <= ( len G) by NAT_1: 14;

          let r be Real;

          take q = |[( min (( - r),((G * (1,1)) `1 ))), ((G * (1,j)) `2 )]|;

          

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

          

           A11: ( min (( - r),((G * (1,1)) `1 ))) <= ((G * (1,1)) `1 ) by XXREAL_0: 17;

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

          then ((G * (1,j)) `2 ) <= ((G * (1,(j + 1))) `2 ) by A7, A9, A10, GOBOARD5: 4;

          hence q in ( cell (G, 0 ,j)) by A8, A11;

          

           A12: |.(q `1 ).| <= |.q.| by JGRAPH_1: 33;

          per cases ;

            suppose r <= 0 ;

            hence thesis;

          end;

            suppose

             A13: r > 0 ;

            (q `1 ) = ( min (( - r),((G * (1,1)) `1 ))) by EUCLID: 52;

            then

             A14: |.( - r).| <= |.(q `1 ).| by A13, TOPREAL6: 3, XXREAL_0: 17;

            ( - ( - r)) > 0 by A13;

            then ( - r) < 0 ;

            then ( - ( - r)) <= |.(q `1 ).| by A14, ABSVALUE:def 1;

            hence thesis by A12, XXREAL_0: 2;

          end;

        end;

        hence thesis by JORDAN2C: 34;

      end;

        suppose j = ( width G);

        then

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

         not ex r be Real st for q be Point of ( TOP-REAL 2) st q in ( cell (G, 0 ,j)) holds |.q.| < r

        proof

          let r be Real;

          take q = |[((G * (1,1)) `1 ), ( max (r,((G * (1,( width G))) `2 )))]|;

          

           A16: |.(q `2 ).| <= |.q.| by JGRAPH_1: 33;

          ((G * (1,( width G))) `2 ) <= ( max (r,((G * (1,( width G))) `2 ))) by XXREAL_0: 25;

          hence q in ( cell (G, 0 ,j)) by A15;

          per cases ;

            suppose r <= 0 ;

            hence thesis;

          end;

            suppose

             A17: r > 0 ;

            (q `2 ) = ( max (r,((G * (1,( width G))) `2 ))) by EUCLID: 52;

            then r <= (q `2 ) by XXREAL_0: 25;

            then r <= |.(q `2 ).| by A17, ABSVALUE:def 1;

            hence thesis by A16, XXREAL_0: 2;

          end;

        end;

        hence thesis by JORDAN2C: 34;

      end;

    end;

    theorem :: JORDAN1B:34

    

     Th34: i <= ( width G) implies not ( cell (G,( len G),i)) is bounded

    proof

      assume

       A1: i <= ( width G);

      per cases by A1, NAT_1: 14, XXREAL_0: 1;

        suppose

         A2: i = 0 ;

        

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

         not ex r be Real st for q be Point of ( TOP-REAL 2) st q in ( cell (G,( len G), 0 )) holds |.q.| < r

        proof

          let r be Real;

          take q = |[((G * (( len G),1)) `1 ), ( min (( - r),((G * (1,1)) `2 )))]|;

          

           A4: |.(q `2 ).| <= |.q.| by JGRAPH_1: 33;

          ( min (( - r),((G * (1,1)) `2 ))) <= ((G * (1,1)) `2 ) by XXREAL_0: 17;

          hence q in ( cell (G,( len G), 0 )) by A3;

          per cases ;

            suppose r <= 0 ;

            hence thesis;

          end;

            suppose

             A5: r > 0 ;

            (q `2 ) = ( min (( - r),((G * (1,1)) `2 ))) by EUCLID: 52;

            then

             A6: |.( - r).| <= |.(q `2 ).| by A5, TOPREAL6: 3, XXREAL_0: 17;

            ( - ( - r)) > 0 by A5;

            then ( - r) < 0 ;

            then ( - ( - r)) <= |.(q `2 ).| by A6, ABSVALUE:def 1;

            hence thesis by A4, XXREAL_0: 2;

          end;

        end;

        hence thesis by A2, JORDAN2C: 34;

      end;

        suppose

         A7: i >= 1 & i < ( width G);

        then

         A8: ( cell (G,( len G),i)) = { |[r, s]| where r,s be Real : ((G * (( len G),1)) `1 ) <= r & ((G * (1,i)) `2 ) <= s & s <= ((G * (1,(i + 1))) `2 ) } by GOBRD11: 29;

         not ex r be Real st for q be Point of ( TOP-REAL 2) st q in ( cell (G,( len G),i)) holds |.q.| < r

        proof

          ( len G) <> 0 by MATRIX_0:def 10;

          then

           A9: 1 <= ( len G) by NAT_1: 14;

          let r be Real;

          take q = |[( max (r,((G * (( len G),1)) `1 ))), ((G * (1,i)) `2 )]|;

          

           A10: i < (i + 1) by NAT_1: 13;

          

           A11: ( max (r,((G * (( len G),1)) `1 ))) >= ((G * (( len G),1)) `1 ) by XXREAL_0: 25;

          (i + 1) <= ( width G) by A7, NAT_1: 13;

          then ((G * (1,i)) `2 ) <= ((G * (1,(i + 1))) `2 ) by A7, A9, A10, GOBOARD5: 4;

          hence q in ( cell (G,( len G),i)) by A8, A11;

          

           A12: |.(q `1 ).| <= |.q.| by JGRAPH_1: 33;

          per cases ;

            suppose r <= 0 ;

            hence thesis;

          end;

            suppose

             A13: r > 0 ;

            (q `1 ) = ( max (r,((G * (( len G),1)) `1 ))) by EUCLID: 52;

            then (q `1 ) >= r by XXREAL_0: 25;

            then r <= |.(q `1 ).| by A13, ABSVALUE:def 1;

            hence thesis by A12, XXREAL_0: 2;

          end;

        end;

        hence thesis by JORDAN2C: 34;

      end;

        suppose

         A14: i = ( width G);

        

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

         not ex r be Real st for q be Point of ( TOP-REAL 2) st q in ( cell (G,( len G),i)) holds |.q.| < r

        proof

          let r be Real;

          take q = |[((G * (( len G),1)) `1 ), ( max (r,((G * (1,( width G))) `2 )))]|;

          

           A16: |.(q `2 ).| <= |.q.| by JGRAPH_1: 33;

          ((G * (1,( width G))) `2 ) <= ( max (r,((G * (1,( width G))) `2 ))) by XXREAL_0: 25;

          hence q in ( cell (G,( len G),i)) by A14, A15;

          per cases ;

            suppose r <= 0 ;

            hence thesis;

          end;

            suppose

             A17: r > 0 ;

            (q `2 ) = ( max (r,((G * (1,( width G))) `2 ))) by EUCLID: 52;

            then r <= (q `2 ) by XXREAL_0: 25;

            then r <= |.(q `2 ).| by A17, ABSVALUE:def 1;

            hence thesis by A16, XXREAL_0: 2;

          end;

        end;

        hence thesis by JORDAN2C: 34;

      end;

    end;

    theorem :: JORDAN1B:35

    

     Th35: j <= ( width ( Gauge (C,n))) implies ( cell (( Gauge (C,n)), 0 ,j)) c= ( UBD C)

    proof

      assume

       A1: j <= ( width ( Gauge (C,n)));

      

       A2: (C ` ) is non empty by JORDAN2C: 66;

      

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

      then

       A4: ( cell (( Gauge (C,n)), 0 ,j)) is non empty by A1, JORDAN1A: 24;

      ( cell (( Gauge (C,n)), 0 ,j)) misses C by A3, A1, JORDAN8: 18;

      then

       A5: ( cell (( Gauge (C,n)), 0 ,j)) c= (C ` ) by SUBSET_1: 23;

      ( cell (( Gauge (C,n)), 0 ,j)) is connected by A3, A1, JORDAN1A: 25;

      then

      consider W be Subset of ( TOP-REAL 2) such that

       A6: W is_a_component_of (C ` ) and

       A7: ( cell (( Gauge (C,n)), 0 ,j)) c= W by A5, A2, A4, GOBOARD9: 3;

       not W is bounded by A1, A7, Th33, RLTOPSP1: 42;

      then W is_outside_component_of C by A6, JORDAN2C:def 3;

      then W c= ( UBD C) by JORDAN2C: 23;

      hence thesis by A7;

    end;

    theorem :: JORDAN1B:36

    

     Th36: j <= ( len ( Gauge (E,n))) implies ( cell (( Gauge (E,n)),( len ( Gauge (E,n))),j)) c= ( UBD E)

    proof

      

       A1: (E ` ) is non empty by JORDAN2C: 66;

      assume

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

      then ( cell (( Gauge (E,n)),( len ( Gauge (E,n))),j)) misses E by JORDAN8: 16;

      then

       A3: ( cell (( Gauge (E,n)),( len ( Gauge (E,n))),j)) c= (E ` ) by SUBSET_1: 23;

      

       A4: ( width ( Gauge (E,n))) = ( len ( Gauge (E,n))) by JORDAN8:def 1;

      then

       A5: ( cell (( Gauge (E,n)),( len ( Gauge (E,n))),j)) is non empty by A2, JORDAN1A: 24;

      ( cell (( Gauge (E,n)),( len ( Gauge (E,n))),j)) is connected by A4, A2, JORDAN1A: 25;

      then

      consider W be Subset of ( TOP-REAL 2) such that

       A6: W is_a_component_of (E ` ) and

       A7: ( cell (( Gauge (E,n)),( len ( Gauge (E,n))),j)) c= W by A3, A1, A5, GOBOARD9: 3;

       not W is bounded by A4, A2, A7, Th34, RLTOPSP1: 42;

      then W is_outside_component_of E by A6, JORDAN2C:def 3;

      then W c= ( UBD E) by JORDAN2C: 23;

      hence thesis by A7;

    end;

    

     Lm3: j <= ( width ( Gauge (C,n))) & ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) implies i <> 0

    proof

      assume that

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

       A2: ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) and

       A3: i = 0 ;

      

       A4: ( cell (( Gauge (C,n)), 0 ,j)) c= ( UBD C) by A1, Th35;

       0 <= ( len ( Gauge (C,n)));

      then ( cell (( Gauge (C,n)), 0 ,j)) is non empty by A1, JORDAN1A: 24;

      hence contradiction by A2, A3, A4, JORDAN2C: 24, XBOOLE_1: 68;

    end;

    

     Lm4: i <= ( len ( Gauge (C,n))) & ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) implies j <> 0

    proof

      assume that

       A1: i <= ( len ( Gauge (C,n))) and

       A2: ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) and

       A3: j = 0 ;

      

       A4: ( cell (( Gauge (C,n)),i, 0 )) c= ( UBD C) by A1, JORDAN1A: 49;

       0 <= ( width ( Gauge (C,n)));

      then ( cell (( Gauge (C,n)),i, 0 )) is non empty by A1, JORDAN1A: 24;

      hence contradiction by A2, A3, A4, JORDAN2C: 24, XBOOLE_1: 68;

    end;

    

     Lm5: j <= ( width ( Gauge (C,n))) & ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) implies i <> ( len ( Gauge (C,n)))

    proof

      assume that

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

       A2: ( cell (( Gauge (C,n)),i,j)) c= ( BDD C);

      

       A3: ( cell (( Gauge (C,n)),( len ( Gauge (C,n))),j)) is non empty by A1, JORDAN1A: 24;

      assume

       A4: i = ( len ( Gauge (C,n)));

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

      then ( cell (( Gauge (C,n)),( len ( Gauge (C,n))),j)) c= ( UBD C) by A1, Th36;

      hence contradiction by A2, A4, A3, JORDAN2C: 24, XBOOLE_1: 68;

    end;

    

     Lm6: i <= ( len ( Gauge (C,n))) & ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) implies j <> ( width ( Gauge (C,n)))

    proof

      assume that

       A1: i <= ( len ( Gauge (C,n))) and

       A2: ( cell (( Gauge (C,n)),i,j)) c= ( BDD C);

      

       A3: ( cell (( Gauge (C,n)),i,( width ( Gauge (C,n))))) c= ( UBD C) by A1, JORDAN1A: 50;

      assume

       A4: j = ( width ( Gauge (C,n)));

      ( cell (( Gauge (C,n)),i,( width ( Gauge (C,n))))) is non empty by A1, JORDAN1A: 24;

      hence contradiction by A2, A4, A3, JORDAN2C: 24, XBOOLE_1: 68;

    end;

    theorem :: JORDAN1B:37

    

     Th37: i <= ( len ( Gauge (C,n))) & j <= ( width ( Gauge (C,n))) & ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) implies j > 1

    proof

      assume that

       A1: i <= ( len ( Gauge (C,n))) and

       A2: j <= ( width ( Gauge (C,n))) and

       A3: ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) and

       A4: j <= 1;

      per cases by A4, NAT_1: 25;

        suppose j = 0 ;

        hence contradiction by A1, A3, Lm4;

      end;

        suppose

         A5: j = 1;

        ( BDD C) c= (C ` ) by JORDAN2C: 25;

        then

         A6: ( cell (( Gauge (C,n)),i,1)) c= (C ` ) by A3, A5;

        

         A7: i <> 0 by A2, A3, Lm3;

        ( UBD C) is_outside_component_of C by JORDAN2C: 68;

        then

         A8: ( UBD C) is_a_component_of (C ` ) by JORDAN2C:def 3;

        

         A9: ( width ( Gauge (C,n))) <> 0 by MATRIX_0:def 10;

        then

         A10: ( 0 + 1) <= ( width ( Gauge (C,n))) by NAT_1: 14;

        then

         A11: ( cell (( Gauge (C,n)),i,1)) is non empty by A1, JORDAN1A: 24;

        i < ( len ( Gauge (C,n))) by A1, A2, A3, Lm5, XXREAL_0: 1;

        then (( cell (( Gauge (C,n)),i, 0 )) /\ ( cell (( Gauge (C,n)),i,( 0 + 1)))) = ( LSeg ((( Gauge (C,n)) * (i,( 0 + 1))),(( Gauge (C,n)) * ((i + 1),( 0 + 1))))) by A9, A7, GOBOARD5: 26, NAT_1: 14;

        then

         A12: ( cell (( Gauge (C,n)),i, 0 )) meets ( cell (( Gauge (C,n)),i,( 0 + 1))) by XBOOLE_0:def 7;

        ( cell (( Gauge (C,n)),i, 0 )) c= ( UBD C) by A1, JORDAN1A: 49;

        then ( cell (( Gauge (C,n)),i,1)) c= ( UBD C) by A1, A10, A12, A8, A6, GOBOARD9: 4, JORDAN1A: 25;

        hence contradiction by A3, A5, A11, JORDAN2C: 24, XBOOLE_1: 68;

      end;

    end;

    theorem :: JORDAN1B:38

    

     Th38: i <= ( len ( Gauge (C,n))) & j <= ( width ( Gauge (C,n))) & ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) implies i > 1

    proof

      assume that

       A1: i <= ( len ( Gauge (C,n))) and

       A2: j <= ( width ( Gauge (C,n))) and

       A3: ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) and

       A4: i <= 1;

      per cases by A4, NAT_1: 25;

        suppose i = 0 ;

        hence contradiction by A2, A3, Lm3;

      end;

        suppose

         A5: i = 1;

        ( BDD C) c= (C ` ) by JORDAN2C: 25;

        then

         A6: ( cell (( Gauge (C,n)),1,j)) c= (C ` ) by A3, A5;

        

         A7: j <> 0 by A1, A3, Lm4;

        ( UBD C) is_outside_component_of C by JORDAN2C: 68;

        then

         A8: ( UBD C) is_a_component_of (C ` ) by JORDAN2C:def 3;

        

         A9: ( len ( Gauge (C,n))) <> 0 by MATRIX_0:def 10;

        then

         A10: ( 0 + 1) <= ( len ( Gauge (C,n))) by NAT_1: 14;

        then

         A11: ( cell (( Gauge (C,n)),1,j)) is non empty by A2, JORDAN1A: 24;

        j < ( width ( Gauge (C,n))) by A1, A2, A3, Lm6, XXREAL_0: 1;

        then (( cell (( Gauge (C,n)), 0 ,j)) /\ ( cell (( Gauge (C,n)),( 0 + 1),j))) = ( LSeg ((( Gauge (C,n)) * (( 0 + 1),j)),(( Gauge (C,n)) * (( 0 + 1),(j + 1))))) by A9, A7, GOBOARD5: 25, NAT_1: 14;

        then

         A12: ( cell (( Gauge (C,n)), 0 ,j)) meets ( cell (( Gauge (C,n)),( 0 + 1),j)) by XBOOLE_0:def 7;

        ( cell (( Gauge (C,n)), 0 ,j)) c= ( UBD C) by A2, Th35;

        then ( cell (( Gauge (C,n)),1,j)) c= ( UBD C) by A2, A10, A12, A8, A6, GOBOARD9: 4, JORDAN1A: 25;

        hence contradiction by A3, A5, A11, JORDAN2C: 24, XBOOLE_1: 68;

      end;

    end;

    theorem :: JORDAN1B:39

    

     Th39: i <= ( len ( Gauge (C,n))) & j <= ( width ( Gauge (C,n))) & ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) implies (j + 1) < ( width ( Gauge (C,n)))

    proof

      assume that

       A1: i <= ( len ( Gauge (C,n))) and

       A2: j <= ( width ( Gauge (C,n))) and

       A3: ( cell (( Gauge (C,n)),i,j)) c= ( BDD C);

      

       A4: j < ( width ( Gauge (C,n))) or j = ( width ( Gauge (C,n))) by A2, XXREAL_0: 1;

      assume (j + 1) >= ( width ( Gauge (C,n)));

      then

       A5: (j + 1) > ( width ( Gauge (C,n))) or (j + 1) = ( width ( Gauge (C,n))) by XXREAL_0: 1;

      per cases by A5, A4, NAT_1: 13;

        suppose j = ( width ( Gauge (C,n)));

        hence contradiction by A1, A3, Lm6;

      end;

        suppose (j + 1) = ( width ( Gauge (C,n)));

        then

         A6: ( cell (( Gauge (C,n)),i,(( width ( Gauge (C,n))) -' 1))) c= ( BDD C) by A3, NAT_D: 34;

        ( BDD C) c= (C ` ) by JORDAN2C: 25;

        then

         A7: ( cell (( Gauge (C,n)),i,(( width ( Gauge (C,n))) -' 1))) c= (C ` ) by A6;

        

         A8: ( width ( Gauge (C,n))) <> 0 by MATRIX_0:def 10;

        then

         A9: ((( width ( Gauge (C,n))) -' 1) + 1) = ( width ( Gauge (C,n))) by NAT_1: 14, XREAL_1: 235;

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

        then

         A10: ( cell (( Gauge (C,n)),i,(( width ( Gauge (C,n))) -' 1))) is non empty by A1, JORDAN1A: 24;

        

         A11: ( cell (( Gauge (C,n)),i,( width ( Gauge (C,n))))) c= ( UBD C) by A1, JORDAN1A: 50;

        ( UBD C) is_outside_component_of C by JORDAN2C: 68;

        then

         A12: ( UBD C) is_a_component_of (C ` ) by JORDAN2C:def 3;

        

         A13: i <> 0 by A2, A3, Lm3;

        

         A14: (( width ( Gauge (C,n))) - 1) < ( width ( Gauge (C,n))) by XREAL_1: 146;

        i < ( len ( Gauge (C,n))) by A1, A2, A3, Lm5, XXREAL_0: 1;

        then (( cell (( Gauge (C,n)),i,( width ( Gauge (C,n))))) /\ ( cell (( Gauge (C,n)),i,(( width ( Gauge (C,n))) -' 1)))) = ( LSeg ((( Gauge (C,n)) * (i,( width ( Gauge (C,n))))),(( Gauge (C,n)) * ((i + 1),( width ( Gauge (C,n))))))) by A14, A9, A13, GOBOARD5: 26, NAT_1: 14;

        then

         A15: ( cell (( Gauge (C,n)),i,( width ( Gauge (C,n))))) meets ( cell (( Gauge (C,n)),i,(( width ( Gauge (C,n))) -' 1))) by XBOOLE_0:def 7;

        (( width ( Gauge (C,n))) -' 1) < ( width ( Gauge (C,n))) by A8, A14, NAT_1: 14, XREAL_1: 233;

        then ( cell (( Gauge (C,n)),i,(( width ( Gauge (C,n))) -' 1))) c= ( UBD C) by A1, A11, A15, A12, A7, GOBOARD9: 4, JORDAN1A: 25;

        hence contradiction by A6, A10, JORDAN2C: 24, XBOOLE_1: 68;

      end;

    end;

    theorem :: JORDAN1B:40

    

     Th40: i <= ( len ( Gauge (C,n))) & j <= ( width ( Gauge (C,n))) & ( cell (( Gauge (C,n)),i,j)) c= ( BDD C) implies (i + 1) < ( len ( Gauge (C,n)))

    proof

      assume that

       A1: i <= ( len ( Gauge (C,n))) and

       A2: j <= ( width ( Gauge (C,n))) and

       A3: ( cell (( Gauge (C,n)),i,j)) c= ( BDD C);

      

       A4: i < ( len ( Gauge (C,n))) or i = ( len ( Gauge (C,n))) by A1, XXREAL_0: 1;

      assume (i + 1) >= ( len ( Gauge (C,n)));

      then

       A5: (i + 1) > ( len ( Gauge (C,n))) or (i + 1) = ( len ( Gauge (C,n))) by XXREAL_0: 1;

      per cases by A5, A4, NAT_1: 13;

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

        hence contradiction by A2, A3, Lm5;

      end;

        suppose (i + 1) = ( len ( Gauge (C,n)));

        then

         A6: ( cell (( Gauge (C,n)),(( len ( Gauge (C,n))) -' 1),j)) c= ( BDD C) by A3, NAT_D: 34;

        ( BDD C) c= (C ` ) by JORDAN2C: 25;

        then

         A7: ( cell (( Gauge (C,n)),(( len ( Gauge (C,n))) -' 1),j)) c= (C ` ) by A6;

        

         A8: ( len ( Gauge (C,n))) <> 0 by MATRIX_0:def 10;

        then

         A9: ((( len ( Gauge (C,n))) -' 1) + 1) = ( len ( Gauge (C,n))) by NAT_1: 14, XREAL_1: 235;

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

        then

         A10: ( cell (( Gauge (C,n)),(( len ( Gauge (C,n))) -' 1),j)) is non empty by A2, JORDAN1A: 24;

        

         A11: j <> 0 by A1, A3, Lm4;

        ( UBD C) is_outside_component_of C by JORDAN2C: 68;

        then

         A12: ( UBD C) is_a_component_of (C ` ) by JORDAN2C:def 3;

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

        then

         A13: ( cell (( Gauge (C,n)),( len ( Gauge (C,n))),j)) c= ( UBD C) by A2, Th36;

        

         A14: (( len ( Gauge (C,n))) - 1) < ( len ( Gauge (C,n))) by XREAL_1: 146;

        j < ( width ( Gauge (C,n))) by A1, A2, A3, Lm6, XXREAL_0: 1;

        then (( cell (( Gauge (C,n)),( len ( Gauge (C,n))),j)) /\ ( cell (( Gauge (C,n)),(( len ( Gauge (C,n))) -' 1),j))) = ( LSeg ((( Gauge (C,n)) * (( len ( Gauge (C,n))),j)),(( Gauge (C,n)) * (( len ( Gauge (C,n))),(j + 1))))) by A14, A9, A11, GOBOARD5: 25, NAT_1: 14;

        then

         A15: ( cell (( Gauge (C,n)),( len ( Gauge (C,n))),j)) meets ( cell (( Gauge (C,n)),(( len ( Gauge (C,n))) -' 1),j)) by XBOOLE_0:def 7;

        (( len ( Gauge (C,n))) -' 1) < ( len ( Gauge (C,n))) by A8, A14, NAT_1: 14, XREAL_1: 233;

        then ( cell (( Gauge (C,n)),(( len ( Gauge (C,n))) -' 1),j)) c= ( UBD C) by A2, A13, A15, A12, A7, GOBOARD9: 4, JORDAN1A: 25;

        hence contradiction by A6, A10, JORDAN2C: 24, XBOOLE_1: 68;

      end;

    end;

    theorem :: JORDAN1B:41

    (ex i, j st i <= ( len ( Gauge (C,n))) & j <= ( width ( Gauge (C,n))) & ( cell (( Gauge (C,n)),i,j)) c= ( BDD C)) implies n >= 1

    proof

      

       A1: (2 |^ 0 ) = 1 by NEWTON: 4;

      given i, j such that

       A2: i <= ( len ( Gauge (C,n))) and

       A3: j <= ( width ( Gauge (C,n))) and

       A4: ( cell (( Gauge (C,n)),i,j)) c= ( BDD C);

      

       A5: (j + 1) < ( width ( Gauge (C,n))) by A2, A3, A4, Th39;

      

       A6: (i + 1) < ( len ( Gauge (C,n))) by A2, A3, A4, Th40;

      assume

       A7: n < 1;

      ( len ( Gauge (C,n))) = ((2 |^ n) + 3) by JORDAN8:def 1;

      then

       A8: ( len ( Gauge (C,n))) = (1 + 3) by A1, A7, NAT_1: 14;

      ( width ( Gauge (C,n))) = ((2 |^ n) + 3) by JORDAN1A: 28;

      then

       A9: ( width ( Gauge (C,n))) = (1 + 3) by A1, A7, NAT_1: 14;

      i <= 4 by A8, A2;

      then

       A10: i = 0 or ... or i = 4;

      j <= 4 by A3, A9;

      then j = 0 or ... or j = 4;

      per cases by A10;

        suppose j = 0 or j = 1;

        hence thesis by A2, A3, A4, Th37;

      end;

        suppose i = 0 or i = 1;

        hence thesis by A2, A3, A4, Th38;

      end;

        suppose j = 2 & i = 2;

        then ( cell (( Gauge (C, 0 )),2,2)) c= ( BDD C) by A4, A7, NAT_1: 14;

        hence contradiction by Th18;

      end;

        suppose j = 3 or j = 4 or i = 3 or i = 4;

        hence thesis by A5, A6, A9, A8;

      end;

    end;