The Mizar article:

Some Properties of Cells and Arcs

by
Robert Milewski,
Andrzej Trybulec,
Artur Kornilowicz, and
Adam Naumowicz

Received October 6, 2000

Copyright (c) 2000 Association of Mizar Users

MML identifier: JORDAN1B
[ MML identifier index ]


environ

 vocabulary COMPTS_1, SPPOL_1, EUCLID, RELAT_2, GOBOARD1, PRE_TOPC, TOPREAL2,
      RELAT_1, TOPREAL1, TOPS_2, SUBSET_1, BOOLE, MCART_1, CONNSP_3, CONNSP_1,
      SETFAM_1, TARSKI, FINSEQ_1, JORDAN3, ARYTM_1, FINSEQ_5, FUNCT_1, GROUP_2,
      PSCOMP_1, ORDINAL2, FUNCT_5, REALSET1, FINSEQ_4, SPRECT_2, FINSEQ_6,
      JORDAN1A, NAT_1, INT_1, JORDAN8, GROUP_1, ARYTM_3, GOBOARD5, TREES_1,
      JORDAN2C, JORDAN9, JORDAN6, COMPLEX1, SQUARE_1, ABSVALUE, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1,
      INT_1, NAT_1, ABSVALUE, SQUARE_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_4,
      FINSEQ_5, MATRIX_1, REALSET1, FINSEQ_6, STRUCT_0, PRE_TOPC, TOPS_2,
      JGRAPH_1, TOPREAL2, CARD_4, BINARITH, CONNSP_1, CONNSP_3, COMPTS_1,
      EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD5, SPPOL_1,
      JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A;
 constructors JORDAN8, REALSET1, JORDAN6, REAL_1, CARD_4, PSCOMP_1, BINARITH,
      JORDAN2C, CONNSP_1, JORDAN9, JORDAN1A, WSIERP_1, SQUARE_1, ABSVALUE,
      FINSEQ_4, JORDAN1, JORDAN3, RFINSEQ, TOPS_2, TOPREAL2, JORDAN5C,
      CONNSP_3, TOPREAL4, SPRECT_1, FINSEQ_5, GOBOARD1, TOPRNS_1, INT_1;
 clusters XREAL_0, TOPREAL6, JORDAN8, INT_1, RELSET_1, STRUCT_0, EUCLID,
      SPRECT_3, FINSEQ_1, FINSEQ_5, JORDAN1A, PRE_TOPC, JORDAN3, MEMBERED;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
 definitions TARSKI, XBOOLE_0;
 theorems AXIOMS, BINARITH, EUCLID, GOBRD11, JORDAN8, NEWTON, PSCOMP_1,
      JORDAN1A, NAT_1, SCMFSA9A, GROUP_4, TOPREAL6, REAL_1, GOBOARD5, SQUARE_1,
      NAT_2, FINSEQ_1, FINSEQ_2, JORDAN4, JORDAN6, SPRECT_2, FINSEQ_4,
      FINSEQ_5, FINSEQ_6, GOBOARD7, GOBOARD9, SPPOL_1, SPPOL_2, TOPREAL4,
      REVROT_1, TOPREAL1, SPRECT_3, BOOLMARK, JORDAN5B, AMI_5, JORDAN3,
      RLVECT_1, JORDAN2C, SUBSET_1, CQC_THE1, JGRAPH_1, ABSVALUE, GOBOARD1,
      RELAT_1, PRE_TOPC, TOPREAL5, XREAL_0, TOPREAL2, TOPS_2, CONNSP_3,
      ORDERS_1, ZFMISC_1, TARSKI, CONNSP_1, SCMFSA_7, FINSEQ_3, XBOOLE_0,
      XBOOLE_1, INT_1, XCMPLX_0, XCMPLX_1;

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;

  definition
   cluster -> non vertical non horizontal Simple_closed_curve;
   coherence
   proof
   let S be Simple_closed_curve;
   consider f being map of (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|S
   such that
A1: f is_homeomorphism by TOPREAL2:def 1;
     dom f = [#]((TOP-REAL 2)|R^2-unit_square) by A1,TOPS_2:def 5
   .= R^2-unit_square by PRE_TOPC:def 10;
   then rng f <> {} by RELAT_1:65;
   then [#]((TOP-REAL 2)|S) <> {} by A1,TOPS_2:def 5;
   then A2: S is non empty by PRE_TOPC:def 10;
   then consider p1 be set such that
    A3: p1 in S by XBOOLE_0:def 1;
   reconsider p1 as Point of TOP-REAL 2 by A3;
     ex p2 be Point of TOP-REAL 2 st p2 in S & p2`1 <> p1`1 by A2,TOPREAL5:21;
   hence S is non vertical by A3,SPPOL_1:def 3;
     ex p2 be Point of TOP-REAL 2 st p2 in S & p2`2 <> p1`2 by A2,TOPREAL5:20;
   hence S is non horizontal by A3,SPPOL_1:def 2;
   end;
  end;

  definition
   let T be non empty TopSpace;
   cluster non empty a_union_of_components of T;
   existence
   proof
      [#]T = the carrier of T by PRE_TOPC:12;
    then reconsider A = [#]T as a_union_of_components of T by CONNSP_3:20;
      A is non empty;
    hence thesis;
   end;
  end;

  theorem
     for T being non empty TopSpace
   for A being non empty a_union_of_components of T st A is connected holds
    A is_a_component_of T
 proof
  let T be non empty TopSpace;
  let A be non empty a_union_of_components of T;
  consider F being Subset-Family of T such that
A1:  (for B being Subset of T st B in F holds B is_a_component_of T) &
    A = union F by CONNSP_3:def 2;
  consider X being set such that
A2: X <> {} & X in F by A1,ORDERS_1:91;
  reconsider X as Subset of T by A2;
  assume A3: A is connected;
    F={X}
   proof
    thus F c= {X}
     proof
      let x be set; assume A4: x in F;
      then reconsider Y=x as Subset of T;
A5:   Y is_a_component_of T & X is_a_component_of T by A1,A2,A4;
A6:   X c= A by A1,A2,ZFMISC_1:92;
        Y c= A by A1,A4,ZFMISC_1:92;
      then Y = A by A3,A5,CONNSP_1:def 5
       .= X by A3,A5,A6,CONNSP_1:def 5;
      hence x in {X} by TARSKI:def 1;
     end;
    let x be set; assume x in {X};
    hence x in F by A2,TARSKI:def 1;
   end;
  then A = X by A1,ZFMISC_1:31;
  hence A is_a_component_of T by A1,A2;
 end;

Lm1:
 for D being non empty set, f being FinSequence of D
 for i,j st 1 <= i & i <= j & j <= len f
  holds mid(f,i,j) is non empty
proof let D be non empty set, f be FinSequence of D, i,j;
 assume 1 <= i & i <= j & j <= len f;
  then len mid(f,i,j) = j-'i+1 by JORDAN4:20;
  then len mid(f,i,j) <> 0 by NAT_1:29;
 hence mid(f,i,j) is non empty by FINSEQ_1:25;
end;

theorem Th2:
 for f being FinSequence holds
  f is empty iff Rev f is empty
proof let f be FinSequence;
 hereby assume f is empty;
   then reconsider g=f as empty FinSequence;
     Rev g is empty;
  hence Rev f is empty;
 end;
 assume Rev f is empty;
  then reconsider g=Rev f as empty FinSequence;
    Rev g is empty;
 hence f is empty by FINSEQ_6:29;
end;

theorem
   for D being non empty set, f being FinSequence of D
 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 such that
A1: 1 <= i and
A2: i <= len f and
A3: 1 <= j and
A4: j <= len f;
 per cases;
 suppose i <= j;
 hence mid(f,i,j) is non empty by A1,A4,Lm1;
 suppose j <= i;
  then A5: mid(f,j,i) is non empty by A2,A3,Lm1;
    mid(f,i,j) = Rev mid(f,j,i) by JORDAN4:30;
 hence mid(f,i,j) is non empty by A5,Th2;
end;

theorem Th4:
   for f be non empty FinSequence of TOP-REAL 2
   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 non empty 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 in dom f by FINSEQ_5:6;
A4: 1 <= Index(p,f) by A2,JORDAN3:41;
       now per cases;
     suppose
A5:    p<>f.1;
A6:   Index(p,f) < len f by A2,JORDAN3:41;
then Index(p,f) in dom f by A4,FINSEQ_3:27;
      then A7: len mid(f,1,Index(p,f)) >= 1 by A3,SPRECT_2:9;
        R_Cut(f,p) = mid(f,1,Index(p,f))^<*p*> by A5,JORDAN3:def 5;
      hence R_Cut(f,p).1 = mid(f,1,Index(p,f)).1 by A7,JORDAN3:17
         .= f.1 by A1,A4,A6,JORDAN3:27;
     suppose
A8:   p = f.1;
       then R_Cut(f,p) = <*p*> by JORDAN3:def 5;
      hence R_Cut(f,p).1 = f.1 by A8,FINSEQ_1:57;
    end;
    hence R_Cut(f,p).1 = f.1;
   end;

  theorem
     for f be non empty FinSequence of TOP-REAL 2
   for p be Point of TOP-REAL 2 st f is_S-Seq & p in L~f holds
    L_Cut(f,p).(len L_Cut(f,p)) = f.(len f)
   proof let f be non empty FinSequence of TOP-REAL 2;
    let p be Point of TOP-REAL 2 such that
A1:  f is_S-Seq and
A2:  p in L~f;
A3:  Rev f is_S-Seq by A1,SPPOL_2:47;
A4:  p in L~Rev f by A2,SPPOL_2:22;
then A5:  L_Cut(Rev Rev f,p) = Rev R_Cut(Rev f,p) by A3,JORDAN3:57;
       2 <= len Rev f by A3,TOPREAL1:def 10;
     then A6:   1 <= len Rev f by AXIOMS:22;
       Rev Rev f = f by FINSEQ_6:29;
    hence L_Cut(f,p).(len L_Cut(f,p))
         = Rev R_Cut(Rev f,p).(len R_Cut(Rev f,p)) by A5,FINSEQ_5:def 3
        .= R_Cut(Rev f,p).1 by FINSEQ_5:65
        .= Rev f.1 by A4,A6,Th4
        .= f.(len f) by FINSEQ_5:65;
   end;

  theorem
     for P be Simple_closed_curve holds W-max(P) <> E-max(P)
   proof
    let P be Simple_closed_curve;
      now assume A1: W-max(P) = E-max(P);
     A2:|[W-bound P, sup (proj2||W-most P)]|=W-max(P) by PSCOMP_1:def 43;
       |[E-bound P, sup (proj2||E-most P)]|=E-max(P) by PSCOMP_1:def 46;
     then W-bound P= E-bound P by A1,A2,SPPOL_2:1;
     hence contradiction by TOPREAL5:23;
    end;
    hence W-max(P) <> E-max(P);
   end;

  theorem
     for D be non empty set
   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 A1: 1 <= i & i < len f;
    then A2: i+1 <= len f by NAT_1:38;
    then i+1-1 <= len f-1 by REAL_1:49;
    then A3: 0+i <= len f-1 by XCMPLX_1:26;
    then len f-1 >= 1 by A1,AXIOMS:22;
    then A4: len f-1 >= 0 by AXIOMS:22;
    then A5: i <= len f-'1 by A3,BINARITH:def 3;
      len f <= len f+1 by NAT_1:29;
    then len f-1 <= len f+1-1 by REAL_1:49;
    then len f-1 <= len f by XCMPLX_1:26;
    then A6: len f-'1 <= len f by A4,BINARITH:def 3;
      len f-i >= 1 by A2,REAL_1:84;
    then A7: len f-i >= 0 by AXIOMS:22;
      len f-1-i >= 0 by A3,REAL_1:84;
    then A8: len f-'1-i >= 0 by A4,BINARITH:def 3;
    A9: len (mid(f,i,len f-'1)^<*f/.(len f)*>) = len mid(f,i,len f-'1) + 1
                                                              by FINSEQ_2:19;
    A10: len mid(f,i,len f-'1) + 1 = len f-'1-'i+1+1 by A1,A5,A6,JORDAN4:20
       .= len f-'1-i+1+1 by A8,BINARITH:def 3
       .= len f-1-i+1+1 by A4,BINARITH:def 3
       .= len f-i-1+1+1 by XCMPLX_1:21
       .= len f-i+-1+1+1 by XCMPLX_0:def 8
       .= len f-i+1 by XCMPLX_1:139
       .= len f-'i+1 by A7,BINARITH:def 3
       .= len mid(f,i,len f) by A1,JORDAN4:20;
      now let j;
     assume A11: 1 <= j & j <= len mid(f,i,len f);
       1 < len f by A1,AXIOMS:22;
     then i in Seg len f & len f in Seg len f by A1,FINSEQ_1:3;
     then A12: i in dom f & len f in dom f by FINSEQ_1:def 3;
     per cases by A11,REAL_1:def 5;
      suppose j < len mid(f,i,len f);
       then A13: j <= len mid(f,i,len f-'1) by A10,NAT_1:38;
       then j in Seg len mid(f,i,len f-'1) by A11,FINSEQ_1:3;
       then A14: j in dom mid(f,i,len f-'1) by FINSEQ_1:def 3;
         j in Seg len mid(f,i,len f) by A11,FINSEQ_1:3;
       then A15: j in dom mid(f,i,len f) by FINSEQ_1:def 3;
         1 <= len f-'1 by A1,A5,AXIOMS:22;
       then len f-'1 in Seg len f by A6,FINSEQ_1:3;
       then A16: len f-'1 in dom f by FINSEQ_1:def 3;
       thus (mid(f,i,len f-'1)^<*f/.(len f)*>)/.j = mid(f,i,len f-'1)/.j
                                                          by A11,A13,BOOLMARK:8
          .= f/.(j+i-'1) by A5,A12,A14,A16,SPRECT_2:7
          .= mid(f,i,len f)/.j by A1,A12,A15,SPRECT_2:7;
      suppose A17: j = len mid(f,i,len f);
       hence (mid(f,i,len f-'1)^<*f/.(len f)*>)/.j = f/.(len f)
                                                            by A10,TOPREAL4:1
          .= mid(f,i,len f)/.j by A12,A17,SPRECT_2:13;
    end;
    hence mid(f,i,len f-'1)^<*f/.(len f)*> = mid(f,i,len f)
                                                       by A9,A10,FINSEQ_5:14;
   end;

  theorem
     for p,q be Point of TOP-REAL 2 st p <> q & LSeg(p,q) is vertical holds
    <*p,q*> is_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:37;
    hence <*p,q*> is_S-Seq by A1,SPPOL_2:46;
   end;

  theorem
     for p,q be Point of TOP-REAL 2 st p <> q & LSeg(p,q) is horizontal holds
    <*p,q*> is_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:36;
    hence <*p,q*> is_S-Seq by A1,SPPOL_2:46;
   end;

  theorem Th10:
   for p,q be FinSequence of TOP-REAL 2
   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 REVROT_1:15;
       then n in Seg len p by FINSEQ_1:def 3;
       then A3: 0+1 <= n & n <= len p by FINSEQ_1:3;
       then A4: n-1 >= 0 by REAL_1:84;
       per cases;
        suppose A5: n <= len(p:-v);
         then A6: Rotate(p,v)/.n = p/.(n-'1+v..p) by A2,A3,REVROT_1:9;
           n <= len p-v..p+1 by A2,A5,FINSEQ_5:53;
         then n-1 <= len p-v..p by REAL_1:86;
         then n-1+v..p <= len p by REAL_1:84;
         then A7: n-'1+v..p <= len p by A4,BINARITH:def 3;
         A8: n-'1 >= 0 by NAT_1:18;
           1 <= v..p by A2,FINSEQ_4:31;
         then 0+1 <= n-'1+v..p by A8,REAL_1:55;
         then n-'1+v..p in Seg len p by A7,FINSEQ_1:3;
         then A9: n-'1+v..p in dom p by FINSEQ_1:def 3;
         hence W-bound L~q <= (Rotate(p,v)/.n)`1 by A1,A6,SPRECT_2:def 1;
         thus (Rotate(p,v)/.n)`1 <= E-bound L~q by A1,A6,A9,SPRECT_2:def 1;
         thus S-bound L~q <= (Rotate(p,v)/.n)`2 by A1,A6,A9,SPRECT_2:def 1;
         thus (Rotate(p,v)/.n)`2 <= N-bound L~q by A1,A6,A9,SPRECT_2:def 1;
        suppose A10: n > len(p:-v);
         then A11: Rotate(p,v)/.n = p/.(n+v..p-'len p) by A2,A3,REVROT_1:12;
           n > len p-v..p+1 by A2,A10,FINSEQ_5:53;
         then n > 1+len p-v..p by XCMPLX_1:29;
         then n+v..p > 1+len p by REAL_1:84;
         then A12: n+v..p-len p > 1 by REAL_1:86;
         then A13: n+v..p-len p >= 0 by AXIOMS:22;
           v..p <= len p by A2,FINSEQ_4:31;
         then n+v..p <= len p+len p by A3,REAL_1:55;
         then n+v..p-len p <= len p by REAL_1:86;
         then A14: n+v..p-'len p <= len p by A13,BINARITH:def 3;
           1 <= n+v..p-'len p by A12,A13,BINARITH:def 3;
         then n+v..p-'len p in Seg len p by A14,FINSEQ_1:3;
         then A15: n+v..p-'len p in dom p by FINSEQ_1:def 3;
         hence W-bound L~q <= (Rotate(p,v)/.n)`1 by A1,A11,SPRECT_2:def 1;
         thus (Rotate(p,v)/.n)`1 <= E-bound L~q by A1,A11,A15,SPRECT_2:def 1;
         thus S-bound L~q <= (Rotate(p,v)/.n)`2 by A1,A11,A15,SPRECT_2:def 1;
         thus (Rotate(p,v)/.n)`2 <= N-bound L~q by A1,A11,A15,SPRECT_2:def 1;
      end;
      hence Rotate(p,v) is_in_the_area_of q by SPRECT_2:def 1;
     suppose not v in rng p;
      hence Rotate(p,v) is_in_the_area_of q by A1,FINSEQ_6:def 2;
   end;

  theorem
     for p be non trivial FinSequence of TOP-REAL 2
   for v be Point of TOP-REAL 2 holds
    Rotate(p,v) is_in_the_area_of p
   proof
    let p be non trivial FinSequence of TOP-REAL 2;
    let v be Point of TOP-REAL 2;
      p is_in_the_area_of p by SPRECT_2:25;
    hence Rotate(p,v) is_in_the_area_of p by Th10;
   end;

  theorem Th12:
   for f be FinSequence holds
    Center f >= 1
   proof
    let f be FinSequence;
      len f div 2 >= 0 by NAT_1:19;
    then len f div 2 + 1 >= 0+1 by AXIOMS:24;
    hence thesis by JORDAN1A:def 1;
   end;

  theorem
     for f be FinSequence st len f >= 1 holds
    Center f <= len f
   proof
    let f be FinSequence;
    assume len f >= 1;
    then len f >= 0+1;
    then len f > 0 by NAT_1:38;
    then 0 + len f < len f + len f by REAL_1:53;
    then len f < 2*len f by XCMPLX_1:11;
    then len f+1 <= 2*len f by NAT_1:38;
    then (len f+1+1) div 2 <= len f by NAT_2:27;
    then (len f+(1+1)) div 2 <= len f by XCMPLX_1:1;
    then len f div 2+1 <= len f by NAT_2:16;
    hence thesis by JORDAN1A:def 1;
   end;

  theorem Th14:
   Center G <= len G
   proof
    A1: Center G = len G div 2 + 1 by JORDAN1A:def 1;
      1 <= len G by GOBRD11:34;
    then 0 < len G by AXIOMS:22;
    then len G div (2 qua Integer) < len G by SCMFSA9A:4;
    then len G div 2 < len G by SCMFSA9A:5;
    hence thesis by A1,NAT_1:38;
   end;

  theorem Th15:
   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:15;
    then len f div 2 + 1 > 1 by NAT_1:38;
    hence thesis by JORDAN1A:def 1;
   end;

  theorem Th16:
   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 AXIOMS:24;
    then len f+2+1 <= len f+len f by XCMPLX_1:1;
    then len f+2+1 <= 2*len f by XCMPLX_1:11;
    then (len f+2+1+1) div 2 <= len f by NAT_2:27;
    then (len f+2+(1+1)) div 2 <= len f by XCMPLX_1:1;
    then (len f+2) div 2+1 <= len f by NAT_2:16;
    then (len f+2) div 2 < len f by NAT_1:38;
    then len f div 2 + 1 < len f by NAT_2:16;
    hence thesis by JORDAN1A:def 1;
   end;

Lm2:
  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:9
        .= 3 by BINARITH:39;
  end;

theorem
   Center Gauge(E,n) = 2|^(n-'1) + 2
  proof
    set G = Gauge(E,n);
    per cases by NAT_1:19;
    suppose
A1:   n = 0;
A2: 0-1 < 0;
A3: 4 = 2 * 2 + 0;
      Center G = len G div 2 + 1 by JORDAN1A:def 1;
    hence Center G = (2|^0 + 3) div 2 + 1 by A1,JORDAN8:def 1
      .= (1+3) div 2 + 1 by NEWTON:9
      .= 1 + 1 + 1 by A3,NAT_1:def 1
      .= 2|^0 + 1 + 1 by NEWTON:9
      .= 2|^(0-'1) + 1 + 1 by A2,BINARITH:def 3
      .= 2|^(0-'1) + (1 + 1) by XCMPLX_1:1
      .= 2|^(n-'1) + 2 by A1;
    suppose
A4:   n > 0;
then A5: 2|^n mod 2 = 0 by JORDAN1A:3;
      3 = 2 * 1 + 1;
then A6: 3 div 2 = 1 by NAT_1:def 1;
A7: len G div 2 + 1 = (2|^n + 3) div 2 + 1 by JORDAN8:def 1
       .= (2|^n div 2) + (3 div 2) + 1 by A5,GROUP_4:106
       .= (2|^n div 2) + (1 + 1) by A6,XCMPLX_1:1;
A8: 0+1 <= n by A4,NAT_1:38;
      2|^n div 2 = 2|^n / 2 by A4,JORDAN1A:5
      .= 2|^n / 2|^1 by NEWTON:10
      .= 2|^(n-'1) by A8,TOPREAL6:15;
    hence thesis by A7,JORDAN1A:def 1;
  end;

theorem Th18:
 E c= cell(Gauge(E,0),2,2)
  proof
    set G = Gauge(E,0);
    let x be set;
    assume
A1:   x in E;
    then reconsider x as Point of TOP-REAL 2;
A2: x = |[x`1,x`2]| by EUCLID:57;
A3: len G = width G by JORDAN8:def 1;
A4: len G-'1 = 3 by Lm2;
A5: 4 <= len G by JORDAN8:13;
    then 1 < len G by AXIOMS:22;
    then G*(2+1,1)`1 = E-bound E & G*(1,2)`2 = S-bound E &
    G*(1,2+1)`2 = N-bound E & G*(2,1)`1 = W-bound E
      by A4,JORDAN8:14,15,16,17;
then A6: G*(2,1)`1 <= x`1 & x`1 <= G*(2+1,1)`1 &
     G*(1,2)`2 <= x`2 & x`2 <= G*(1,2+1)`2 by A1,PSCOMP_1:71;
      2 < len G by A5,AXIOMS:22;
    then cell(G,2,2) =
      { |[p,q]| where p, q is Real: G*(2,1)`1 <= p & p <= G*(2+1,1)`1 &
        G*(1,2)`2 <= q & q <= G*(1,2+1)`2 } by A3,GOBRD11:32;
    hence thesis by A2,A6;
  end;

theorem Th19:
 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 Th18;
then A2: E c= BDD E by A1,XBOOLE_1:1;
    consider e being Element of E;
A3: e in E;
      BDD E misses E by JORDAN1A:15;
    hence thesis by A2,A3,XBOOLE_0:3;
  end;

theorem
   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:59;
      1 <= Center G & Center G <= len G by Th12,Th14;
    then G*(Center G,1)`2 = S-bound L~Cage(C,1) by JORDAN1A:93;
    hence thesis by A1,EUCLID:57;
  end;

theorem
   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:59;
      1 <= Center G & Center G <= len G by Th12,Th14;
    then G*(Center G,len G)`2 = N-bound L~Cage(C,1) by JORDAN1A:91;
    hence thesis by A1,EUCLID:57;
  end;

Lm3:
 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,REAL_1:def 5;
    then i+1 <= m by NAT_1:38;
    then m = i+1 by A2,AXIOMS:21;
    hence i = m -' 1 by BINARITH:39;
  end;

theorem Th22:
 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 & j < width G and
A2:   1 <= m & m <= len G and
A3:   1 <= n & n <= width G and
A4:   p in cell(G,len G,j) and
A5:   p`1 = G*(m,n)`1;
A6: 1 <= width G by A1,AXIOMS:22;
A7: G*(m,1)`1 = G*(m,n)`1 by A2,A3,GOBOARD5:3;
      cell(G,len G,j) =
      { |[r,s]| where r, s is Real:
        G*(len G,1)`1 <= r & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }
        by A1,GOBRD11:29;
    then consider r, s being Real such that
A8:   p = |[r,s]| and
A9:   G*(len G,1)`1 <= r and G*(1,j)`2 <= s & s <= G*(1,j+1)`2 by A4;
      p`1 = r by A8,EUCLID:56;
    then len G <= m by A2,A5,A6,A7,A9,GOBOARD5:4;
    hence thesis by A2,AXIOMS:21;
  end;

theorem
   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 & i <= len G and
A2:   1 <= j & j < width G and
A3:   1 <= m & m <= len G and
A4:   1 <= n & n <= width G and
A5:   p in cell(G,i,j) and
A6:   p`1 = G*(m,n)`1;
A7: 1 <= width G by A2,AXIOMS:22;
A8: G*(m,1)`1 = G*(m,n)`1 by A3,A4,GOBOARD5:3;
    per cases by A1,REAL_1:def 5;
    suppose i = len G;
    hence thesis by A2,A3,A4,A5,A6,Th22;
    suppose i < len G;
    then cell(G,i,j) =
      { |[r,s]| where r, s is 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,GOBRD11:32;
    then consider r, s being Real such that
A9:   p = |[r,s]| and
A10:   G*(i,1)`1 <= r & r <= G*(i+1,1)`1 and
        G*(1,j)`2 <= s & s <= G*(1,j+1)`2 by A5;
A11: p`1 = r by A9,EUCLID:56;
      i <= m & m <= i+1
    proof
      assume
A12:     not thesis;
      per cases by A12;
      suppose i > m;
      hence contradiction by A1,A3,A6,A7,A8,A10,A11,GOBOARD5:4;
      suppose
A13:     m > i+1;
        1 <= i+1 by NAT_1:29;
      hence contradiction by A3,A6,A7,A8,A10,A11,A13,GOBOARD5:4;
    end;
    hence thesis by Lm3;
  end;

theorem Th24:
 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 & i < len G and
A2:   1 <= m & m <= len G and
A3:   1 <= n & n <= width G and
A4:   p in cell(G,i,width G) and
A5:   p`2 = G*(m,n)`2;
A6: 1 <= len G by A1,AXIOMS:22;
A7: G*(1,n)`2 = G*(m,n)`2 by A2,A3,GOBOARD5:2;
      cell(G,i,width G) =
      { |[r,s]| where r, s is Real:
        G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,width G)`2 <= s }
        by A1,GOBRD11:31;
    then consider r, s being Real such that
A8:   p = |[r,s]| and
        G*(i,1)`1 <= r and
A9:   r <= G*(i+1,1)`1 & G*(1,width G)`2 <= s by A4;
      p`2 = s by A8,EUCLID:56;
    then width G <= n by A3,A5,A6,A7,A9,GOBOARD5:5;
    hence thesis by A3,AXIOMS:21;
  end;

theorem
   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 & i < len G and
A2:   1 <= j & j <= width G and
A3:   1 <= m & m <= len G and
A4:   1 <= n & n <= width G and
A5:   p in cell(G,i,j) and
A6:   p`2 = G*(m,n)`2;
A7: 1 <= len G by A1,AXIOMS:22;
A8: G*(1,n)`2 = G*(m,n)`2 by A3,A4,GOBOARD5:2;
    per cases by A2,REAL_1:def 5;
    suppose j = width G;
    hence thesis by A1,A3,A4,A5,A6,Th24;
    suppose j < width G;
    then cell(G,i,j) =
      { |[r,s]| where r, s is 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,GOBRD11:32;
    then consider r, s being Real such that
A9:   p = |[r,s]| and
        G*(i,1)`1 <= r & r <= G*(i+1,1)`1 and
A10:   G*(1,j)`2 <= s & s <= G*(1,j+1)`2 by A5;
A11: p`2 = s by A9,EUCLID:56;
      j <= n & n <= j+1
    proof
      assume
A12:     not thesis;
      per cases by A12;
      suppose j > n;
      hence contradiction by A2,A4,A6,A7,A8,A10,A11,GOBOARD5:5;
      suppose
A13:     n > j+1;
        1 <= j+1 by NAT_1:29;
      hence contradiction by A4,A6,A7,A8,A10,A11,A13,GOBOARD5:5;
    end;
    hence thesis by Lm3;
  end;

  theorem Th26:
   for C be Simple_closed_curve
   for r be real number st W-bound C <= r & r <= E-bound C holds
    LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Upper_Arc C
   proof
    let C be Simple_closed_curve;
    let r be real number;
    A1: (W-min C)`1 = W-bound C by PSCOMP_1:84;
    A2: (E-max C)`1 = E-bound C by PSCOMP_1:104;
    A3: r is Real by XREAL_0:def 1;
    assume A4: W-bound C <= r & r <= E-bound C;
      Upper_Arc C is_an_arc_of W-min(C),E-max(C) by JORDAN6:def 8;
    then Upper_Arc C meets Vertical_Line(r) by A1,A2,A3,A4,JORDAN6:64;
    then consider x be set such that
     A5: x in Upper_Arc C /\ Vertical_Line(r) by XBOOLE_0:4;
    A6: x in Upper_Arc C & x in Vertical_Line(r) by A5,XBOOLE_0:def 3;
    reconsider fs = x as Point of TOP-REAL 2 by A5;
      Upper_Arc C c= C by JORDAN1A:16;
    then A7: S-bound C <= fs`2 & fs`2 <= N-bound C by A6,PSCOMP_1:71;
    A8: |[r,S-bound C]|`1 = r by EUCLID:56
       .= fs`1 by A6,JORDAN6:34;
    A9: |[r,N-bound C]|`1 = r by EUCLID:56
       .= fs`1 by A6,JORDAN6:34;
      |[r,S-bound C]|`2 = S-bound C & |[r,N-bound C]|`2 = N-bound C by EUCLID:
56
;
    then x in LSeg(|[r,S-bound C]|,|[r,N-bound C]|) by A7,A8,A9,GOBOARD7:8;
    hence LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Upper_Arc C
                                                          by A6,XBOOLE_0:3;
   end;

  theorem Th27:
   for C be Simple_closed_curve
   for r be real number st W-bound C <= r & r <= E-bound C holds
    LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Lower_Arc C
   proof
    let C be Simple_closed_curve;
    let r be real number;
    A1: (W-min C)`1 = W-bound C by PSCOMP_1:84;
    A2: (E-max C)`1 = E-bound C by PSCOMP_1:104;
    A3: r is Real by XREAL_0:def 1;
    assume A4: W-bound C <= r & r <= E-bound C;
      Lower_Arc C is_an_arc_of E-max(C),W-min(C) by JORDAN6:def 9;
    then Lower_Arc C is_an_arc_of W-min(C),E-max(C) by JORDAN5B:14;
    then Lower_Arc C meets Vertical_Line(r) by A1,A2,A3,A4,JORDAN6:64;
    then consider x be set such that
     A5: x in Lower_Arc C /\ Vertical_Line(r) by XBOOLE_0:4;
    A6: x in Lower_Arc C & x in Vertical_Line(r) by A5,XBOOLE_0:def 3;
    reconsider fs = x as Point of TOP-REAL 2 by A5;
      Lower_Arc C c= C by JORDAN1A:16;
    then A7: S-bound C <= fs`2 & fs`2 <= N-bound C by A6,PSCOMP_1:71;
    A8: |[r,S-bound C]|`1 = r by EUCLID:56
       .= fs`1 by A6,JORDAN6:34;
    A9: |[r,N-bound C]|`1 = r by EUCLID:56
       .= fs`1 by A6,JORDAN6:34;
      |[r,S-bound C]|`2 = S-bound C & |[r,N-bound C]|`2 = N-bound C by EUCLID:
56
;
    then x in LSeg(|[r,S-bound C]|,|[r,N-bound C]|) by A7,A8,A9,GOBOARD7:8;
    hence LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Lower_Arc C
                                                          by A6,XBOOLE_0:3;
   end;

  theorem Th28:
   for C be Simple_closed_curve
   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 A1: 1 < i & i < len Gauge(C,n);
    A2: Gauge(C,n)*(i,2) = |[(Gauge(C,n)*(i,2))`1,(Gauge(C,n)*(i,2))`2]|
                                                                 by EUCLID:57
       .= |[(Gauge(C,n)*(i,2))`1,S-bound C]| by A1,JORDAN8:16;
    A3: 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:57
       .= |[(Gauge(C,n)*(i,len Gauge(C,n)-'1))`1,N-bound C]| by A1,JORDAN8:17;
    set r = (Gauge(C,n)*(i,2))`1;
    A4: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
    A5: 4 <= len Gauge(C,n) by JORDAN8:13;
    then len Gauge(C,n) >= 0+1 by AXIOMS:22;
    then A6: len Gauge(C,n)-1 >= 0 by REAL_1:84;
    A7: 1+1 <= len Gauge(C,n) by A5,AXIOMS:22;
    then 1 <= len Gauge(C,n)-1 by REAL_1:84;
    then A8: 1 <= len Gauge(C,n)-'1 by A6,BINARITH:def 3;
    A9: len Gauge(C,n)-'1 <= len Gauge(C,n) by GOBOARD9:2;
    A10: r = (Gauge(C,n)*(i,1))`1 by A1,A4,A7,GOBOARD5:3
       .= (Gauge(C,n)*(i,len Gauge(C,n)-'1))`1 by A1,A4,A8,A9,GOBOARD5:3;
      1+1 <= i by A1,NAT_1:38;
    then (Gauge(C,n)*(2,2))`1 <= r by A1,A4,A7,SPRECT_3:25;
    then A11: W-bound C <= r by A7,JORDAN8:14;
      i+1 <= len Gauge(C,n) by A1,NAT_1:38;
    then i <= len Gauge(C,n)-1 by REAL_1:84;
    then i <= len Gauge(C,n)-'1 by A6,BINARITH:def 3;
    then r <= Gauge(C,n)*(len Gauge(C,n)-'1,len Gauge(C,n)-'1)`1
                                              by A1,A4,A8,A9,A10,SPRECT_3:25;
    then r <= E-bound C by A8,A9,JORDAN8:15;
    then A12: LSeg(Gauge(C,n)*(i,2),Gauge(C,n)*(i,len Gauge(C,n)-'1))
     meets Upper_Arc C by A2,A3,A10,A11,Th26;
    A13: Gauge(C,n)*(i,2) in
     LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
                                                     by A1,A4,A7,JORDAN1A:37;
      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,A4,A8,A9,JORDAN1A:37;
    then LSeg(Gauge(C,n)*(i,2),Gauge(C,n)*(i,len Gauge(C,n)-'1)) c=
     LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) by A13,TOPREAL1:12;
    hence LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
     meets Upper_Arc C by A12,XBOOLE_1:63;
   end;

  theorem Th29:
   for C be Simple_closed_curve
   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 A1: 1 < i & i < len Gauge(C,n);
    A2: Gauge(C,n)*(i,2) = |[(Gauge(C,n)*(i,2))`1,(Gauge(C,n)*(i,2))`2]|
                                                                 by EUCLID:57
       .= |[(Gauge(C,n)*(i,2))`1,S-bound C]| by A1,JORDAN8:16;
    A3: 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:57
       .= |[(Gauge(C,n)*(i,len Gauge(C,n)-'1))`1,N-bound C]| by A1,JORDAN8:17;
    set r = (Gauge(C,n)*(i,2))`1;
    A4: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
    A5: 4 <= len Gauge(C,n) by JORDAN8:13;
    then len Gauge(C,n) >= 0+1 by AXIOMS:22;
    then A6: len Gauge(C,n)-1 >= 0 by REAL_1:84;
    A7: 1+1 <= len Gauge(C,n) by A5,AXIOMS:22;
    then 1 <= len Gauge(C,n)-1 by REAL_1:84;
    then A8: 1 <= len Gauge(C,n)-'1 by A6,BINARITH:def 3;
    A9: len Gauge(C,n)-'1 <= len Gauge(C,n) by GOBOARD9:2;
    A10: r = (Gauge(C,n)*(i,1))`1 by A1,A4,A7,GOBOARD5:3
       .= (Gauge(C,n)*(i,len Gauge(C,n)-'1))`1 by A1,A4,A8,A9,GOBOARD5:3;
      1+1 <= i by A1,NAT_1:38;
    then (Gauge(C,n)*(2,2))`1 <= r by A1,A4,A7,SPRECT_3:25;
    then A11: W-bound C <= r by A7,JORDAN8:14;
      i+1 <= len Gauge(C,n) by A1,NAT_1:38;
    then i <= len Gauge(C,n)-1 by REAL_1:84;
    then i <= len Gauge(C,n)-'1 by A6,BINARITH:def 3;
    then r <= Gauge(C,n)*(len Gauge(C,n)-'1,len Gauge(C,n)-'1)`1
                                              by A1,A4,A8,A9,A10,SPRECT_3:25;
    then r <= E-bound C by A8,A9,JORDAN8:15;
    then A12: LSeg(Gauge(C,n)*(i,2),Gauge(C,n)*(i,len Gauge(C,n)-'1))
     meets Lower_Arc C by A2,A3,A10,A11,Th27;
    A13: Gauge(C,n)*(i,2) in
     LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
                                                     by A1,A4,A7,JORDAN1A:37;
      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,A4,A8,A9,JORDAN1A:37;
    then LSeg(Gauge(C,n)*(i,2),Gauge(C,n)*(i,len Gauge(C,n)-'1)) c=
     LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) by A13,TOPREAL1:12;
    hence LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
     meets Lower_Arc C by A12,XBOOLE_1:63;
   end;

  theorem
     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:13;
    then len Gauge(C,n) >= 2 by AXIOMS:22;
    then A2: 1 < Center Gauge(C,n) by Th15;
      len Gauge(C,n) >= 3 by A1,AXIOMS:22;
    then Center Gauge(C,n) < len Gauge(C,n) by Th16;
    hence LSeg(Gauge(C,n)*(Center Gauge(C,n),1),
         Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Upper_Arc C
                                                              by A2,Th28;
   end;

  theorem
     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:13;
    then len Gauge(C,n) >= 2 by AXIOMS:22;
    then A2: 1 < Center Gauge(C,n) by Th15;
      len Gauge(C,n) >= 3 by A1,AXIOMS:22;
    then Center Gauge(C,n) < len Gauge(C,n) by Th16;
    hence LSeg(Gauge(C,n)*(Center Gauge(C,n),1),
         Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Lower_Arc C
                                                              by A2,Th29;
   end;

  theorem Th32:
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   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 A1: 1 <= i & i <= len Gauge(C,n);
    A2: Gauge(C,n)*(i,1) = |[(Gauge(C,n)*(i,1))`1,(Gauge(C,n)*(i,1))`2]|
                                                                 by EUCLID:57
       .= |[(Gauge(C,n)*(i,1))`1,S-bound L~Cage(C,n)]| by A1,JORDAN1A:93;
    A3: 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:57
       .= |[(Gauge(C,n)*(i,len Gauge(C,n)))`1,
             N-bound L~Cage(C,n)]| by A1,JORDAN1A:91;
    set r = (Gauge(C,n)*(i,1))`1;
    A4: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
      4 <= len Gauge(C,n) by JORDAN8:13;
    then A5: 1 <= len Gauge(C,n) by AXIOMS:22;
    then A6: r = (Gauge(C,n)*(i,len Gauge(C,n)))`1 by A1,A4,GOBOARD5:3;
      (Gauge(C,n)*(1,1))`1 <= r by A1,A4,A5,SPRECT_3:25;
    then A7: W-bound L~Cage(C,n) <= r by A5,JORDAN1A:94;
      r <= Gauge(C,n)*(len Gauge(C,n),1)`1 by A1,A4,A5,SPRECT_3:25;
    then r <= E-bound L~Cage(C,n) by A5,JORDAN1A:92;
    hence LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
     meets Upper_Arc L~Cage(C,n) by A2,A3,A6,A7,Th26;
   end;

  theorem Th33:
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   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 A1: 1 <= i & i <= len Gauge(C,n);
    A2: Gauge(C,n)*(i,1) = |[(Gauge(C,n)*(i,1))`1,(Gauge(C,n)*(i,1))`2]|
                                                                 by EUCLID:57
       .= |[(Gauge(C,n)*(i,1))`1,S-bound L~Cage(C,n)]| by A1,JORDAN1A:93;
    A3: 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:57
       .= |[(Gauge(C,n)*(i,len Gauge(C,n)))`1,
             N-bound L~Cage(C,n)]| by A1,JORDAN1A:91;
    set r = (Gauge(C,n)*(i,1))`1;
    A4: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
      4 <= len Gauge(C,n) by JORDAN8:13;
    then A5: 1 <= len Gauge(C,n) by AXIOMS:22;
    then A6: r = (Gauge(C,n)*(i,len Gauge(C,n)))`1 by A1,A4,GOBOARD5:3;
      (Gauge(C,n)*(1,1))`1 <= r by A1,A4,A5,SPRECT_3:25;
    then A7: W-bound L~Cage(C,n) <= r by A5,JORDAN1A:94;
      r <= Gauge(C,n)*(len Gauge(C,n),1)`1 by A1,A4,A5,SPRECT_3:25;
    then r <= E-bound L~Cage(C,n) by A5,JORDAN1A:92;
    hence LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
     meets Lower_Arc L~Cage(C,n) by A2,A3,A6,A7,Th27;
   end;

  theorem
     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:13;
    then len Gauge(C,n) >= 2 by AXIOMS:22;
    then A2: 1 < Center Gauge(C,n) by Th15;
      len Gauge(C,n) >= 3 by A1,AXIOMS:22;
    then Center Gauge(C,n) < len Gauge(C,n) by Th16;
    hence 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) by A2,Th32;
   end;

  theorem
     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:13;
    then len Gauge(C,n) >= 2 by AXIOMS:22;
    then A2: 1 < Center Gauge(C,n) by Th15;
      len Gauge(C,n) >= 3 by A1,AXIOMS:22;
    then Center Gauge(C,n) < len Gauge(C,n) by Th16;
    hence 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) by A2,Th33;
   end;

theorem Th36:
 j <= width G implies cell(G,0,j) is not Bounded
proof assume
A1: j <= width G;
 per cases by A1,AXIOMS:21,RLVECT_1:99;
 suppose j = 0;
  then A2: cell(G,0,j) = { |[r,s]| where r, s is Real :
        r <= G*(1,1)`1 & s <= G*(1,1)`2 } by GOBRD11:24;
    not ex r being Real st for q being 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)]|;
       min(-r,G*(1,1)`1) <= G*(1,1)`1 & min(-r,G*(1,1)`2) <= G*(1,1)`2
                                  by SQUARE_1:35;
    hence q in cell(G,0,j) by A2;
A3:   abs(q`1)<=|.q.| by JGRAPH_1:50;
     per cases;
     suppose
A4:    r <= 0;
        abs(q`1) >= 0 by ABSVALUE:5;
    hence thesis by A4,JGRAPH_1:50;
     suppose r > 0;
    then --r > 0;
    then A5:    -r < 0 by REAL_1:66;
       q`1 = min(-r,G*(1,1)`1) by EUCLID:56;
     then q`1 <= -r by SQUARE_1:35;
     then abs(-r) <= abs(q`1) by A5,TOPREAL6:8;
     then --r <= abs(q`1) by A5,ABSVALUE:def 1;
    hence thesis by A3,AXIOMS:22;
   end;
 hence cell(G,0,j) is not Bounded by JORDAN2C:40;
 suppose
A6: j >= 1 & j < width G;
  then A7: cell(G,0,j) =
       { |[r,s]| where r is Element of REAL, s is Element of REAL:
          r <= G*(1,1)`1 & G*(1,j)`2 <= s & s <= G*
(1,j+1)`2 } by GOBRD11:26;
    not ex r being Real st for q being 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),G*(1,j)`2]|;
       len G <> 0 by GOBOARD1:def 5;
     then A8:   1 <= len G by RLVECT_1:99;
       j < j+1 & j+1 <= width G by A6,NAT_1:38;
     then A9:   G*(1,j)`2 <= G*(1,j+1)`2 by A6,A8,GOBOARD5:5;
       min(-r,G*(1,1)`1) <= G*(1,1)`1 by SQUARE_1:35;
    hence q in cell(G,0,j) by A7,A9;
A10:   abs(q`1)<=|.q.| by JGRAPH_1:50;
     per cases;
     suppose
A11:    r <= 0;
        abs(q`1) >= 0 by ABSVALUE:5;
    hence thesis by A11,JGRAPH_1:50;
     suppose r > 0;
    then --r > 0;
    then A12:    -r < 0 by REAL_1:66;
       q`1 = min(-r,G*(1,1)`1) by EUCLID:56;
     then q`1 <= -r by SQUARE_1:35;
     then abs(-r) <= abs(q`1) by A12,TOPREAL6:8;
     then --r <= abs(q`1) by A12,ABSVALUE:def 1;
    hence thesis by A10,AXIOMS:22;
   end;
 hence cell(G,0,j) is not Bounded by JORDAN2C:40;
 suppose j = width G;
  then A13: cell(G,0,j) = { |[r,s]| where r is Element of REAL, s is Element of
REAL :
      r <= G*(1,1)`1 & G*(1,width G)`2 <= s }
     by GOBRD11:25;
    not ex r being Real st for q being 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)]|;
       G*(1, width G)`2 <= max(r,G*(1,width G)`2) by SQUARE_1:46;
    hence q in cell(G,0,j) by A13;
A14:   abs(q`2)<=|.q.| by JGRAPH_1:50;
     per cases;
     suppose
A15:    r <= 0;
        abs(q`2) >= 0 by ABSVALUE:5;
    hence thesis by A15,JGRAPH_1:50;
     suppose
A16:     r > 0;
      A17: q`2 = max(r,G*(1,width G)`2) by EUCLID:56;
     then A18:    r <= q`2 by SQUARE_1:46;
      q`2 > 0 by A16,A17,SQUARE_1:46;
     then r <= abs(q`2) by A18,ABSVALUE:def 1;
    hence thesis by A14,AXIOMS:22;
   end;
 hence cell(G,0,j) is not Bounded by JORDAN2C:40;
end;

theorem Th37:
 i <= width G implies cell(G,len G,i) is not Bounded
proof assume
A1: i <= width G;
 per cases by A1,AXIOMS:21,RLVECT_1:99;
 suppose
A2: i = 0;
A3: cell(G,len G,0) =
     { |[r,s]| where r is Element of REAL, s is Element of REAL :
      G*(len G,1)`1 <= r & s <= G*(1,1)`2 }
                              by GOBRD11:27;
    not ex r being Real st for q being 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)]|;
       min(-r,G*(1,1)`2) <= G*(1,1)`2 by SQUARE_1:35;
    hence q in cell(G,len G,0) by A3;
A4:   abs(q`2)<=|.q.| by JGRAPH_1:50;
     per cases;
     suppose
A5:    r <= 0;
        abs(q`2) >= 0 by ABSVALUE:5;
    hence thesis by A5,JGRAPH_1:50;
     suppose r > 0;
    then --r > 0;
    then A6:    -r < 0 by REAL_1:66;
       q`2 = min(-r,G*(1,1)`2) by EUCLID:56;
     then q`2 <= -r by SQUARE_1:35;
     then abs(-r) <= abs(q`2) by A6,TOPREAL6:8;
     then --r <= abs(q`2) by A6,ABSVALUE:def 1;
    hence thesis by A4,AXIOMS:22;
   end;
 hence cell(G,len G,i) is not Bounded by A2,JORDAN2C:40;
 suppose
A7: i >= 1 & i < width G;
  then A8: cell(G,len G,i) =
       { |[r,s]| where r is Element of REAL, s is Element of REAL:
          G*(len G,1)`1 <= r & G*(1,i)`2 <=s & s <= G*(1,i+1)`2 }
                              by GOBRD11:29;
    not ex r being Real st for q being Point of TOP-REAL 2 st
     q in cell(G,len G,i) holds |.q.| < r
   proof let r be Real;
    take q = |[max(r,G*(len G,1)`1),G*(1,i)`2]|;
       len G <> 0 by GOBOARD1:def 5;
     then A9:   1 <= len G by RLVECT_1:99;
       i < i+1 & i+1 <= width G by A7,NAT_1:38;
     then A10:   G*(1,i)`2 <= G*(1,i+1)`2 by A7,A9,GOBOARD5:5;
       max(r,G*(len G,1)`1) >= G*(len G,1)`1 by SQUARE_1:46;
    hence q in cell(G,len G,i) by A8,A10;
A11:   abs(q`1)<=|.q.| by JGRAPH_1:50;
     per cases;
     suppose
A12:    r <= 0;
        abs(q`1) >= 0 by ABSVALUE:5;
    hence thesis by A12,JGRAPH_1:50;
     suppose
A13:    r > 0;
       q`1 = max(r,G*(len G,1)`1) by EUCLID:56;
     then q`1 >= r by SQUARE_1:46;
     then abs(r) <= abs(q`1) by A13,TOPREAL6:7;
     then r <= abs(q`1) by A13,ABSVALUE:def 1;
    hence thesis by A11,AXIOMS:22;
   end;
 hence cell(G,len G,i) is not Bounded by JORDAN2C:40;
 suppose
A14: i = width G;
A15:  cell(G,len G,width G)
      = { |[r,s]| where r, s is Real :
           G*(len G,1)`1 <= r & G*(1,width G)`2 <= s } by GOBRD11:28;
    not ex r being Real st for q being 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)]|;
       G*(1,width G)`2 <= max(r,G*(1,width G)`2) by SQUARE_1:46;
    hence q in cell(G,len G,i) by A14,A15;
A16:   abs(q`2)<=|.q.| by JGRAPH_1:50;
     per cases;
     suppose
A17:    r <= 0;
        abs(q`2) >= 0 by ABSVALUE:5;
    hence thesis by A17,JGRAPH_1:50;
     suppose
A18:     r > 0;
      A19: q`2 = max(r,G*(1,width G)`2) by EUCLID:56;
     then A20:    r <= q`2 by SQUARE_1:46;
      q`2 > 0 by A18,A19,SQUARE_1:46;
     then r <= abs(q`2) by A20,ABSVALUE:def 1;
    hence thesis by A16,AXIOMS:22;
   end;
 hence cell(G,len G,i) is not Bounded by JORDAN2C:40;
end;

theorem Th38:
 j <= width Gauge(C,n) implies cell(Gauge(C,n),0,j) c= UBD C
proof
A1: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
 assume
A2: j <= width Gauge(C,n);
  then cell(Gauge(C,n),0,j) misses C by A1,JORDAN8:21;
  then A3: cell(Gauge(C,n),0,j) c= C` by SUBSET_1:43;
A4: 0 <= width Gauge(C,n) by NAT_1:18;
  then A5: cell(Gauge(C,n),0,j) is connected by A1,A2,JORDAN1A:46;
     C is Bounded by JORDAN2C:73;
  then A6: C` is non empty by JORDAN2C:74;
    cell(Gauge(C,n),0,j) is non empty by A1,A2,A4,JORDAN1A:45;
  then consider W being Subset of TOP-REAL 2 such that
A7: W is_a_component_of C` and
A8: cell(Gauge(C,n),0,j) c= W by A3,A5,A6,GOBOARD9:5;
    cell(Gauge(C,n),0,j) is not Bounded by A2,Th36;
  then W is not Bounded by A8,JORDAN2C:16;
  then W is_outside_component_of C by A7,JORDAN2C:def 4;
  then W c= UBD C by JORDAN2C:27;
 hence cell(Gauge(C,n),0,j) c= UBD C by A8,XBOOLE_1:1;
end;

theorem Th39:
 j <= len Gauge(E,n) implies cell(Gauge(E,n),len Gauge(E,n),j) c= UBD E
proof
A1: width Gauge(E,n) = len Gauge(E,n) by JORDAN8:def 1;
 assume
A2: j <= len Gauge(E,n);
  then cell(Gauge(E,n),len Gauge(E,n),j) misses E by JORDAN8:19;
  then A3: cell(Gauge(E,n),len Gauge(E,n),j) c= E` by SUBSET_1:43;
A4: cell(Gauge(E,n),len Gauge(E,n),j) is connected by A1,A2,JORDAN1A:46;
     E is Bounded by JORDAN2C:73;
  then A5: E` is non empty by JORDAN2C:74;
    cell(Gauge(E,n),len Gauge(E,n),j) is non empty by A1,A2,JORDAN1A:45;
  then consider W being 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,A4,A5,GOBOARD9:5;
    cell(Gauge(E,n),len Gauge(E,n),j) is not Bounded by A1,A2,Th37;
  then W is not Bounded by A7,JORDAN2C:16;
  then W is_outside_component_of E by A6,JORDAN2C:def 4;
  then W c= UBD E by JORDAN2C:27;
 hence cell(Gauge(E,n),len Gauge(E,n),j) c= UBD E by A7,XBOOLE_1:1;
end;

Lm4:
  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;
     0 <= len Gauge(C,n) by NAT_1:18;
   then A4: cell(Gauge(C,n),0,j) is non empty by A1,JORDAN1A:45;
     cell(Gauge(C,n),0,j) c= UBD C by A1,Th38;
   then UBD C meets BDD C by A2,A3,A4,XBOOLE_1:68;
  hence contradiction by JORDAN2C:28;
 end;

Lm5:
 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;
     0 <= width Gauge(C,n) by NAT_1:18;
   then A4: cell(Gauge(C,n),i,0) is non empty by A1,JORDAN1A:45;
     cell(Gauge(C,n),i,0) c= UBD C by A1,JORDAN1A:70;
   then UBD C meets BDD C by A2,A3,A4,XBOOLE_1:68;
  hence contradiction by JORDAN2C:28;
 end;

Lm6:
 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: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
  assume
A4: i = len Gauge(C,n);
A5: cell(Gauge(C,n),len Gauge(C,n),j) is non empty
                            by A1,JORDAN1A:45;
    cell(Gauge(C,n),len Gauge(C,n),j) c= UBD C by A1,A3,Th39;
  then UBD C meets BDD C by A2,A4,A5,XBOOLE_1:68;
 hence contradiction by JORDAN2C:28;
 end;

Lm7:
 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;
  assume
A3: j = width Gauge(C,n);
A4: cell(Gauge(C,n),i,width Gauge(C,n)) is non empty
                            by A1,JORDAN1A:45;
    cell(Gauge(C,n),i,width Gauge(C,n)) c= UBD C by A1,JORDAN1A:71;
  then UBD C meets BDD C by A2,A3,A4,XBOOLE_1:68;
 hence contradiction by JORDAN2C:28;
 end;

theorem Th40:
 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,CQC_THE1:2;
   suppose j = 0;
   hence contradiction by A1,A3,Lm5;
   suppose
A5:  j = 1;
     width Gauge(C,n) <> 0 by GOBOARD1:def 5;
   then A6: 0+1 <= width Gauge(C,n) by RLVECT_1:99;
   then A7: cell(Gauge(C,n),i,1) is non empty by A1,JORDAN1A:45;
 A8: cell(Gauge(C,n),i,0) c= UBD C by A1,JORDAN1A:70;
 A9: C is Bounded by JORDAN2C:73;
     i <> len Gauge(C,n) by A2,A3,Lm6;
   then A10: i < len Gauge(C,n) by A1,AXIOMS:21;
 A11:  0 < width Gauge(C,n) by A6,NAT_1:38;
      i <> 0 by A2,A3,Lm4;
    then 1 <= i by RLVECT_1:99;
    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 A10,A11,GOBOARD5:27;
     then A12:   cell(Gauge(C,n),i,0) meets cell(Gauge(C,n),i,0+1) by XBOOLE_0:
def 7;
      ex B being Subset of TOP-REAL 2 st B is_outside_component_of C & B=UBD C
                           by A9,JORDAN2C:76;
    then A13:  UBD C is_a_component_of C` by JORDAN2C:def 4;
 A14:  cell(Gauge(C,n),i,1) is connected by A1,A6,JORDAN1A:46;
     BDD C c= C` by JORDAN2C:29;
   then cell(Gauge(C,n),i,1) c= C` by A3,A5,XBOOLE_1:1;
   then cell(Gauge(C,n),i,1) c= UBD C by A8,A12,A13,A14,GOBOARD9:6;
   then UBD C meets BDD C by A3,A5,A7,XBOOLE_1:68;
  hence contradiction by JORDAN2C:28;
 end;

theorem Th41:
 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,CQC_THE1:2;
   suppose i = 0;
   hence contradiction by A2,A3,Lm4;
   suppose
A5:  i = 1;
     len Gauge(C,n) <> 0 by GOBOARD1:def 5;
   then A6: 0+1 <= len Gauge(C,n) by RLVECT_1:99;
   then A7: cell(Gauge(C,n),1,j) is non empty by A2,JORDAN1A:45;
 A8: cell(Gauge(C,n),0,j) c= UBD C by A2,Th38;
 A9: C is Bounded by JORDAN2C:73;
     j <> width Gauge(C,n) by A1,A3,Lm7;
   then A10: j < width Gauge(C,n) by A2,AXIOMS:21;
 A11:  0 < len Gauge(C,n) by A6,NAT_1:38;
      j <> 0 by A1,A3,Lm5;
    then 1 <= j by RLVECT_1:99;
    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 A10,A11,GOBOARD5:26;
     then A12:   cell(Gauge(C,n),0,j) meets cell(Gauge(C,n),0+1,j) by XBOOLE_0:
def 7;
      ex B being Subset of TOP-REAL 2 st B is_outside_component_of C & B=UBD C
                           by A9,JORDAN2C:76;
    then A13:  UBD C is_a_component_of C` by JORDAN2C:def 4;
 A14:  cell(Gauge(C,n),1,j) is connected by A2,A6,JORDAN1A:46;
     BDD C c= C` by JORDAN2C:29;
   then cell(Gauge(C,n),1,j) c= C` by A3,A5,XBOOLE_1:1;
   then cell(Gauge(C,n),1,j) c= UBD C by A8,A12,A13,A14,GOBOARD9:6;
   then UBD C meets BDD C by A3,A5,A7,XBOOLE_1:68;
  hence contradiction by JORDAN2C:28;
 end;

theorem Th42:
 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;
 assume j + 1 >= width Gauge(C,n);
  then A4: j + 1 > width Gauge(C,n) or
    j + 1 = width Gauge(C,n) by AXIOMS:21;
A5: j < width Gauge(C,n) or j = width Gauge(C,n) by A2,AXIOMS:21;
  per cases by A4,A5,NAT_1:38;
  suppose j = width Gauge(C,n);
  hence contradiction by A1,A3,Lm7;
  suppose j + 1 = width Gauge(C,n);
   then A6:  cell(Gauge(C,n),i,width Gauge(C,n)-'1) c= BDD C by A3,BINARITH:39;
    width Gauge(C,n)-'1 <= width Gauge(C,n) by JORDAN3:7;
  then A7: cell(Gauge(C,n),i,width Gauge(C,n)-'1) is non empty
                                         by A1,JORDAN1A:45;
A8: cell(Gauge(C,n),i,width Gauge(C,n)) c= UBD C by A1,JORDAN1A:71;
A9: C is Bounded by JORDAN2C:73;
    width Gauge(C,n) <> 0 by GOBOARD1:def 5;
  then A10: 0+1 <= width Gauge(C,n) by RLVECT_1:99;
      i <> len Gauge(C,n) by A2,A3,Lm6;
    then A11: i < len Gauge(C,n) by A1,AXIOMS:21;
      width Gauge(C,n)-1 < width Gauge(C,n) by INT_1:26;
    then A12: width Gauge(C,n)-'1 < width Gauge(C,n) by A10,SCMFSA_7:3;
A13: width Gauge(C,n)-'1+1 = width Gauge(C,n) by A10,AMI_5:4;
     i <> 0 by A2,A3,Lm4;
   then 1 <= i by RLVECT_1:99;
   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 A11,A12,A13,GOBOARD5:27;
    then A14:   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;
     ex B being Subset of TOP-REAL 2 st B is_outside_component_of C & B=UBD C
                          by A9,JORDAN2C:76;
   then A15:  UBD C is_a_component_of C` by JORDAN2C:def 4;
A16:  cell(Gauge(C,n),i,width Gauge(C,n)-'1) is connected
                              by A1,A12,JORDAN1A:46;
    BDD C c= C` by JORDAN2C:29;
  then cell(Gauge(C,n),i,width Gauge(C,n)-'1) c= C`
                               by A6,XBOOLE_1:1;
  then cell(Gauge(C,n),i,width Gauge(C,n)-'1)
                        c= UBD C by A8,A14,A15,A16,GOBOARD9:6;
  then UBD C meets BDD C by A6,A7,XBOOLE_1:68;
 hence contradiction by JORDAN2C:28;
end;

theorem Th43:
 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;
 assume i + 1 >= len Gauge(C,n);
  then A4: i + 1 > len Gauge(C,n) or
    i + 1 = len Gauge(C,n) by AXIOMS:21;
A5: i < len Gauge(C,n) or i = len Gauge(C,n) by A1,AXIOMS:21;
  per cases by A4,A5,NAT_1:38;
  suppose i = len Gauge(C,n);
  hence contradiction by A2,A3,Lm6;
  suppose i + 1 = len Gauge(C,n);
   then A6:  cell(Gauge(C,n),len Gauge(C,n)-'1,j) c= BDD C by A3,BINARITH:39;
    len Gauge(C,n)-'1 <= len Gauge(C,n) by JORDAN3:7;
  then A7: cell(Gauge(C,n),len Gauge(C,n)-'1,j) is non empty
                                         by A2,JORDAN1A:45;
      len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
   then A8: cell(Gauge(C,n),len Gauge(C,n),j) c= UBD C by A2,Th39;
A9: C is Bounded by JORDAN2C:73;
    len Gauge(C,n) <> 0 by GOBOARD1:def 5;
  then A10: 0+1 <= len Gauge(C,n) by RLVECT_1:99;
      j <> width Gauge(C,n) by A1,A3,Lm7;
    then A11: j < width Gauge(C,n) by A2,AXIOMS:21;
      len Gauge(C,n)-1 < len Gauge(C,n) by INT_1:26;
    then A12: len Gauge(C,n)-'1 < len Gauge(C,n) by A10,SCMFSA_7:3;
A13: len Gauge(C,n)-'1+1 = len Gauge(C,n) by A10,AMI_5:4;
     j <> 0 by A1,A3,Lm5;
   then 1 <= j by RLVECT_1:99;
   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 A11,A12,A13,GOBOARD5:26;
    then A14:   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;
     ex B being Subset of TOP-REAL 2 st B is_outside_component_of C & B=UBD C
                          by A9,JORDAN2C:76;
   then A15:  UBD C is_a_component_of C` by JORDAN2C:def 4;
A16:  cell(Gauge(C,n),len Gauge(C,n)-'1,j) is connected
                              by A2,A12,JORDAN1A:46;
    BDD C c= C` by JORDAN2C:29;
  then cell(Gauge(C,n),len Gauge(C,n)-'1,j) c= C`
                               by A6,XBOOLE_1:1;
  then cell(Gauge(C,n),len Gauge(C,n)-'1,j)
                        c= UBD C by A8,A14,A15,A16,GOBOARD9:6;
  then UBD C meets BDD C by A6,A7,XBOOLE_1:68;
 hence contradiction by JORDAN2C:28;
end;

theorem
    (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 given i,j such 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: width Gauge(C,n) = 2|^n + 3 by JORDAN1A:49;
A5: len Gauge(C,n) = 2|^n + 3 by JORDAN8:def 1;
A6: j + 1 < width Gauge(C,n) by A1,A2,A3,Th42;
A7: i + 1 < len Gauge(C,n) by A1,A2,A3,Th43;
A8: 2|^0 = 1 by NEWTON:9;
 assume
A9: n < 1;
  then A10: width Gauge(C,n) = 1 + 3 by A4,A8,RLVECT_1:99;
A11: len Gauge(C,n) = 1 + 3 by A5,A8,A9,RLVECT_1:99;
  per cases by A1,A2,A10,A11,CQC_THE1:5;
  suppose j= 0 or j=1;
   hence thesis by A1,A2,A3,Th40;
  suppose i= 0 or i=1;
   hence thesis by A1,A2,A3,Th41;
  suppose j=2 & i=2;
   then cell(Gauge(C,0),2,2) c= BDD C by A3,A9,RLVECT_1:99;
  hence contradiction by Th19;
  suppose j=3 or j=4 or i=3 or i=4;
 hence thesis by A6,A7,A10,A11;
end;

Back to top