:: JORDAN1B semantic presentation

begin


theorem :: JORDAN1B:1
for f being FinSequence holds
( f is empty iff Rev f is empty )
proof
let f be FinSequence; ::_thesis: ( f is empty iff Rev f is empty )
thus  ( f is empty implies Rev f is empty ) ; ::_thesis: ( Rev f is empty implies f is empty )
assume  Rev f is empty ; ::_thesis: f is empty
then reconsider g = Rev f as empty FinSequence ;
 Rev g is empty ;
hence  f is empty ; ::_thesis: verum
end;

theorem :: JORDAN1B:2
for D being non empty set
for f being FinSequence of D
for i, j being Element of NAT st 1 <= i & i <= len f & 1 <= j & j <= len f holds
not mid (f,i,j) is empty
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, j being Element of NAT st 1 <= i & i <= len f & 1 <= j & j <= len f holds
not mid (f,i,j) is empty
let f be FinSequence of D; ::_thesis: for i, j being Element of NAT st 1 <= i & i <= len f & 1 <= j & j <= len f holds
not mid (f,i,j) is empty
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i <= len f & 1 <= j & j <= len f implies not mid (f,i,j) is empty )
assume that
A1: 1 <= i and
A2: i <= len f and
A3: 1 <= j and
A4: j <= len f ; ::_thesis: not mid (f,i,j) is empty
A5: j in dom f by A3, A4, FINSEQ_3:25;
 i in dom f by A1, A2, FINSEQ_3:25;
hence  not mid (f,i,j) is empty by A5, SPRECT_2:7; ::_thesis: verum
end;

theorem Th3: :: JORDAN1B:3
for f being FinSequence of (TOP-REAL 2)
for p being 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); ::_thesis: for p being Point of (TOP-REAL 2) st 1 <= len f & p in L~ f holds
(R_Cut (f,p)) . 1 = f . 1
let p be Point of (TOP-REAL 2); ::_thesis: ( 1 <= len f & p in L~ f implies (R_Cut (f,p)) . 1 = f . 1 )
assume that
A1: 1 <= len f and
A2: p in L~ f ; ::_thesis: (R_Cut (f,p)) . 1 = f . 1
A3: 1 <= Index (p,f) by A2, JORDAN3:8;
A4: 1 in dom f by A1, FINSEQ_3:25;
now__::_thesis:_(R_Cut_(f,p))_._1_=_f_._1
percases ( p <> f . 1 or p = f . 1 ) ;
suppose p <> f . 1 ; ::_thesis: (R_Cut (f,p)) . 1 = 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 ;
::_thesis: verum
end;
supposeA7: p = f . 1 ; ::_thesis: (R_Cut (f,p)) . 1 = f . 1
then  R_Cut (f,p) = <*p*> by JORDAN3:def_4;
hence  (R_Cut (f,p)) . 1 = f . 1 by A7, FINSEQ_1:40; ::_thesis: verum
end;
end;
end;
hence  (R_Cut (f,p)) . 1 = f . 1 ; ::_thesis: verum
end;

theorem :: JORDAN1B:4
for f being FinSequence of (TOP-REAL 2)
for p being 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); ::_thesis: for p being 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)
let p be Point of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq & p in L~ f implies (L_Cut (f,p)) . (len (L_Cut (f,p))) = f . (len f) )
assume that
A1: f is being_S-Seq and
A2: p in L~ f ; ::_thesis: (L_Cut (f,p)) . (len (L_Cut (f,p))) = f . (len 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 ;
::_thesis: verum
end;

theorem :: JORDAN1B:5
for P being Simple_closed_curve holds W-max P <> E-max P
proof
let P be Simple_closed_curve; ::_thesis: W-max P <> E-max P
now__::_thesis:_not_W-max_P_=_E-max_P
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 ; ::_thesis: contradiction
then  W-bound P = E-bound P by A2, A1, SPPOL_2:1;
hence  contradiction by TOPREAL5:17; ::_thesis: verum
end;
hence  W-max P <> E-max P ; ::_thesis: verum
end;

theorem :: JORDAN1B:6
for i being Element of NAT
for D being non empty set
for f being 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 i be Element of NAT ; ::_thesis: for D being non empty set
for f being FinSequence of D st 1 <= i & i < len f holds
(mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f))
let D be non empty set ; ::_thesis: for f being FinSequence of D st 1 <= i & i < len f holds
(mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f))
let f be FinSequence of D; ::_thesis: ( 1 <= i & i < len f implies (mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f)) )
assume that
A1: 1 <= i and
A2: i < len f ; ::_thesis: (mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,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__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(mid_(f,i,(len_f)))_holds_
((mid_(f,i,((len_f)_-'_1)))_^_<*(f_/._(len_f))*>)_/._j_=_(mid_(f,i,(len_f)))_/._j
 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; ::_thesis: ( 1 <= j & j <= len (mid (f,i,(len f))) implies ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. b1 = (mid (f,i,(len f))) /. b1 )
assume that
A13: 1 <= j and
A14: j <= len (mid (f,i,(len f))) ; ::_thesis: ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. b1 = (mid (f,i,(len f))) /. b1
percases ( j < len (mid (f,i,(len f))) or j = len (mid (f,i,(len f))) ) by A14, XXREAL_0:1;
suppose j < len (mid (f,i,(len f))) ; ::_thesis: ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. b1 = (mid (f,i,(len f))) /. b1
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 ;
::_thesis: verum
end;
supposeA19: j = len (mid (f,i,(len f))) ; ::_thesis: ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. b1 = (mid (f,i,(len f))) /. b1
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 ;
::_thesis: verum
end;
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  (mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f)) by A9, A10, FINSEQ_5:13; ::_thesis: verum
end;

theorem :: JORDAN1B:7
for p, q being 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); ::_thesis: ( p <> q & LSeg (p,q) is vertical implies <*p,q*> is being_S-Seq )
assume that
A1: p <> q and
A2: LSeg (p,q) is vertical ; ::_thesis: <*p,q*> is being_S-Seq
 p `1 = q `1 by A2, SPPOL_1:16;
hence  <*p,q*> is being_S-Seq by A1, SPPOL_2:43; ::_thesis: verum
end;

theorem :: JORDAN1B:8
for p, q being 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); ::_thesis: ( p <> q & LSeg (p,q) is horizontal implies <*p,q*> is being_S-Seq )
assume that
A1: p <> q and
A2: LSeg (p,q) is horizontal ; ::_thesis: <*p,q*> is being_S-Seq
 p `2 = q `2 by A2, SPPOL_1:15;
hence  <*p,q*> is being_S-Seq by A1, SPPOL_2:43; ::_thesis: verum
end;

theorem Th9: :: JORDAN1B:9
for p, q being FinSequence of (TOP-REAL 2)
for v being 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); ::_thesis: for v being Point of (TOP-REAL 2) st p is_in_the_area_of q holds
Rotate (p,v) is_in_the_area_of q
let v be Point of (TOP-REAL 2); ::_thesis: ( p is_in_the_area_of q implies Rotate (p,v) is_in_the_area_of q )
assume A1: p is_in_the_area_of q ; ::_thesis: Rotate (p,v) is_in_the_area_of q
percases ( v in rng p or not v in rng p ) ;
supposeA2: v in rng p ; ::_thesis: Rotate (p,v) is_in_the_area_of q
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(Rotate_(p,v))_holds_
(_W-bound_(L~_q)_<=_((Rotate_(p,v))_/._n)_`1_&_((Rotate_(p,v))_/._n)_`1_<=_E-bound_(L~_q)_&_S-bound_(L~_q)_<=_((Rotate_(p,v))_/._n)_`2_&_((Rotate_(p,v))_/._n)_`2_<=_N-bound_(L~_q)_)
let n be Element of NAT ; ::_thesis: ( n in dom (Rotate (p,v)) implies ( W-bound (L~ q) <= ((Rotate (p,v)) /. b1) `1 & ((Rotate (p,v)) /. b1) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. b1) `2 & ((Rotate (p,v)) /. b1) `2 <= N-bound (L~ q) ) )
assume  n in dom (Rotate (p,v)) ; ::_thesis: ( W-bound (L~ q) <= ((Rotate (p,v)) /. b1) `1 & ((Rotate (p,v)) /. b1) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. b1) `2 & ((Rotate (p,v)) /. b1) `2 <= N-bound (L~ q) )
then  n in dom p by REVROT_1:15;
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;
percases ( n <= len (p :- v) or n > len (p :- v) ) ;
supposeA7: n <= len (p :- v) ; ::_thesis: ( W-bound (L~ q) <= ((Rotate (p,v)) /. b1) `1 & ((Rotate (p,v)) /. b1) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. b1) `2 & ((Rotate (p,v)) /. b1) `2 <= N-bound (L~ q) )
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, REVROT_1:9;
hence  W-bound (L~ q) <= ((Rotate (p,v)) /. n) `1 by A1, A9, SPRECT_2:def_1; ::_thesis: ( ((Rotate (p,v)) /. n) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 & ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) )
thus  ((Rotate (p,v)) /. n) `1 <= E-bound (L~ q) by A1, A10, A9, SPRECT_2:def_1; ::_thesis: ( S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 & ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) )
thus  S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 by A1, A10, A9, SPRECT_2:def_1; ::_thesis: ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q)
thus  ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) by A1, A10, A9, SPRECT_2:def_1; ::_thesis: verum
end;
supposeA11: n > len (p :- v) ; ::_thesis: ( W-bound (L~ q) <= ((Rotate (p,v)) /. b1) `1 & ((Rotate (p,v)) /. b1) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. b1) `2 & ((Rotate (p,v)) /. b1) `2 <= N-bound (L~ q) )
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, REVROT_1:12;
hence  W-bound (L~ q) <= ((Rotate (p,v)) /. n) `1 by A1, A13, SPRECT_2:def_1; ::_thesis: ( ((Rotate (p,v)) /. n) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 & ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) )
thus  ((Rotate (p,v)) /. n) `1 <= E-bound (L~ q) by A1, A14, A13, SPRECT_2:def_1; ::_thesis: ( S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 & ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) )
thus  S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 by A1, A14, A13, SPRECT_2:def_1; ::_thesis: ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q)
thus  ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) by A1, A14, A13, SPRECT_2:def_1; ::_thesis: verum
end;
end;
end;
hence  Rotate (p,v) is_in_the_area_of q by SPRECT_2:def_1; ::_thesis: verum
end;
suppose not v in rng p ; ::_thesis: Rotate (p,v) is_in_the_area_of q
hence  Rotate (p,v) is_in_the_area_of q by A1, FINSEQ_6:def_2; ::_thesis: verum
end;
end;
end;

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

theorem Th11: :: JORDAN1B:11
for f being FinSequence holds Center f >= 1
proof
let f be FinSequence; ::_thesis: Center f >= 1
 ((len f) div 2) + 1 >= 0 + 1 by XREAL_1:6;
hence  Center f >= 1 by JORDAN1A:def_1; ::_thesis: verum
end;

theorem :: JORDAN1B:12
for f being FinSequence st len f >= 1 holds
Center f <= len f
proof
let f be FinSequence; ::_thesis: ( len f >= 1 implies Center f <= len f )
assume  len f >= 1 ; ::_thesis: Center f <= len f
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  Center f <= len f by JORDAN1A:def_1; ::_thesis: verum
end;

theorem Th13: :: JORDAN1B:13
for G being Go-board holds Center G <= len G
proof
let G be Go-board; ::_thesis: Center G <= len G
 0 < len G by GOBRD11:34;
then A1: (len G) div 2 < len G by INT_1:56;
 Center G = ((len G) div 2) + 1 by JORDAN1A:def_1;
hence  Center G <= len G by A1, NAT_1:13; ::_thesis: verum
end;

theorem Th14: :: JORDAN1B:14
for f being FinSequence st len f >= 2 holds
Center f > 1
proof
let f be FinSequence; ::_thesis: ( len f >= 2 implies Center f > 1 )
assume  len f >= 2 ; ::_thesis: Center f > 1
then  (len f) div 2 >= 1 by NAT_2:13;
then  ((len f) div 2) + 1 > 1 by NAT_1:13;
hence  Center f > 1 by JORDAN1A:def_1; ::_thesis: verum
end;

theorem Th15: :: JORDAN1B:15
for f being FinSequence st len f >= 3 holds
Center f < len f
proof
let f be FinSequence; ::_thesis: ( len f >= 3 implies Center f < len f )
assume  len f >= 3 ; ::_thesis: Center f < len f
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  Center f < len f by JORDAN1A:def_1; ::_thesis: verum
end;

Lm1: now__::_thesis:_for_E_being_non_empty_Subset_of_(TOP-REAL_2)_holds_(len_(Gauge_(E,0)))_-'_1_=_3
let E be non empty Subset of (TOP-REAL 2); ::_thesis: (len (Gauge (E,0))) -' 1 = 3
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 ; ::_thesis: verum
end;

theorem :: JORDAN1B:16
for E being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2
proof
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2
let n be Element of NAT ; ::_thesis: Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2
set G = Gauge (E,n);
percases ( n = 0 or n > 0 ) ;
supposeA1: n = 0 ; ::_thesis: Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2
A2: 4 = (2 * 2) + 0 ;
A3: 0 - 1 < 0 ;
 Center (Gauge (E,n)) = ((len (Gauge (E,n))) div 2) + 1 by JORDAN1A:def_1;
hence  Center (Gauge (E,n)) = (((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 ;
::_thesis: verum
end;
supposeA4: n > 0 ; ::_thesis: Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2
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) by NEWTON:5
.= 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 (Gauge (E,n))) 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  Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2 by A6, JORDAN1A:def_1; ::_thesis: verum
end;
end;
end;

theorem Th17: :: JORDAN1B:17
for E being compact non horizontal non vertical Subset of (TOP-REAL 2) holds E c= cell ((Gauge (E,0)),2,2)
proof
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: E c= cell ((Gauge (E,0)),2,2)
set G = Gauge (E,0);
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E or x in cell ((Gauge (E,0)),2,2) )
A1: len (Gauge (E,0)) = width (Gauge (E,0)) by JORDAN8:def_1;
assume A2: x in E ; ::_thesis: x in cell ((Gauge (E,0)),2,2)
then reconsider x = x as Point of (TOP-REAL 2) ;
A3: 4 <= len (Gauge (E,0)) by JORDAN8:10;
then A4: 1 < len (Gauge (E,0)) by XXREAL_0:2;
then  ((Gauge (E,0)) * (1,2)) `2 = S-bound E by JORDAN8:13;
then A5: ((Gauge (E,0)) * (1,2)) `2 <= x `2 by A2, PSCOMP_1:24;
 2 < len (Gauge (E,0)) by A3, XXREAL_0:2;
then A6: cell ((Gauge (E,0)),2,2) =  {  |[p,q]| where p, q is Real : ( ((Gauge (E,0)) * (2,1)) `1 <= p & p <= ((Gauge (E,0)) * ((2 + 1),1)) `1 & ((Gauge (E,0)) * (1,2)) `2 <= q & q <= ((Gauge (E,0)) * (1,(2 + 1))) `2 )  }  by A1, GOBRD11:32;
 ((Gauge (E,0)) * (2,1)) `1 = W-bound E by A4, JORDAN8:11;
then A7: ((Gauge (E,0)) * (2,1)) `1 <= x `1 by A2, PSCOMP_1:24;
A8: (len (Gauge (E,0))) -' 1 = 3 by Lm1;
then  ((Gauge (E,0)) * ((2 + 1),1)) `1 = E-bound E by A4, JORDAN8:12;
then A9: x `1 <= ((Gauge (E,0)) * ((2 + 1),1)) `1 by A2, PSCOMP_1:24;
 ((Gauge (E,0)) * (1,(2 + 1))) `2 = N-bound E by A8, A4, JORDAN8:14;
then A10: x `2 <= ((Gauge (E,0)) * (1,(2 + 1))) `2 by A2, PSCOMP_1:24;
 x = |[(x `1),(x `2)]| by EUCLID:53;
hence  x in cell ((Gauge (E,0)),2,2) by A7, A9, A5, A10, A6; ::_thesis: verum
end;

theorem Th18: :: JORDAN1B:18
for E being compact non horizontal non vertical Subset of (TOP-REAL 2) holds not cell ((Gauge (E,0)),2,2) c= BDD E
proof
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: not cell ((Gauge (E,0)),2,2) c= BDD E
assume A1: cell ((Gauge (E,0)),2,2) c= BDD E ; ::_thesis: contradiction
 E c= cell ((Gauge (E,0)),2,2) by Th17;
then A2: E c= BDD E by A1, XBOOLE_1:1;
set e = the Element of E;
A3: BDD E misses E by JORDAN1A:7;
 the Element of E in E ;
hence  contradiction by A2, A3, XBOOLE_0:3; ::_thesis: verum
end;

theorem :: JORDAN1B:19
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (Gauge (C,1)) * ((Center (Gauge (C,1))),1) = |[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: (Gauge (C,1)) * ((Center (Gauge (C,1))),1) = |[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|
set G = Gauge (C,1);
 1 <= len (Gauge (C,1)) by GOBRD11:34;
then A1: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((W-bound C) + (E-bound C)) / 2 by JORDAN1A:38;
 Center (Gauge (C,1)) <= len (Gauge (C,1)) by Th13;
then  ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 = S-bound (L~ (Cage (C,1))) by Th11, JORDAN1A:72;
hence  (Gauge (C,1)) * ((Center (Gauge (C,1))),1) = |[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]| by A1, EUCLID:53; ::_thesis: verum
end;

theorem :: JORDAN1B:20
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (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
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: (Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1)))) = |[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|
set G = Gauge (C,1);
 1 <= len (Gauge (C,1)) by GOBRD11:34;
then A1: ((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))) `1 = ((W-bound C) + (E-bound C)) / 2 by JORDAN1A:38;
 1 <= Center (Gauge (C,1)) by Th11;
then  ((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))) `2 = N-bound (L~ (Cage (C,1))) by Th13, JORDAN1A:70;
hence  (Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1)))) = |[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]| by A1, EUCLID:53; ::_thesis: verum
end;

Lm2:  for i, m being Element of NAT st i <= m & m <= i + 1 & not i = m holds
i = m -' 1
proof
let i, m be Element of NAT ; ::_thesis: ( i <= m & m <= i + 1 & not i = m implies i = m -' 1 )
assume that
A1: i <= m and
A2: m <= i + 1 and
A3: i <> m ; ::_thesis: i = m -' 1
 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  i = m -' 1 by NAT_D:34; ::_thesis: verum
end;

theorem Th21: :: JORDAN1B:21
for G being Go-board
for j, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 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 holds
len G = m
proof
let G be Go-board; ::_thesis: for j, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 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 holds
len G = m
let j, m, n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2) st 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 holds
len G = m
let p be Point of (TOP-REAL 2); ::_thesis: ( 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 )
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 ; ::_thesis: len G = m
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 is 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 being 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  len G = m by A4, XXREAL_0:1; ::_thesis: verum
end;

theorem :: JORDAN1B:22
for G being Go-board
for i, j, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 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 & not i = m holds
i = m -' 1
proof
let G be Go-board; ::_thesis: for i, j, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 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 & not i = m holds
i = m -' 1
let i, j, m, n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2) st 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 & not i = m holds
i = m -' 1
let p be Point of (TOP-REAL 2); ::_thesis: ( 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 & not i = m implies i = m -' 1 )
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 ; ::_thesis: ( i = m or i = m -' 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;
percases ( i = len G or i < len G ) by A2, XXREAL_0:1;
suppose i = len G ; ::_thesis: ( i = m or i = m -' 1 )
hence  ( i = m or i = m -' 1 ) by A3, A4, A5, A6, A7, A8, A9, A10, Th21; ::_thesis: verum
end;
suppose i < len G ; ::_thesis: ( i = m or i = m -' 1 )
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, A3, A4, GOBRD11:32;
then consider r, s being 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 i <= m or not m <= i + 1 ) ; ::_thesis: contradiction
percases ( i > m or m > i + 1 ) by A17;
suppose i > m ; ::_thesis: contradiction
hence  contradiction by A2, A5, A10, A12, A11, A14, A16, GOBOARD5:3; ::_thesis: verum
end;
supposeA18: m > i + 1 ; ::_thesis: contradiction
 1 <= i + 1 by NAT_1:11;
hence  contradiction by A6, A10, A12, A11, A15, A16, A18, GOBOARD5:3; ::_thesis: verum
end;
end;
end;
hence  ( i = m or i = m -' 1 ) by Lm2; ::_thesis: verum
end;
end;
end;

theorem Th23: :: JORDAN1B:23
for G being Go-board
for i, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 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 holds
width G = n
proof
let G be Go-board; ::_thesis: for i, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 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 holds
width G = n
let i, m, n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2) st 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 holds
width G = n
let p be Point of (TOP-REAL 2); ::_thesis: ( 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 )
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 ; ::_thesis: width G = n
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 is 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 being 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  width G = n by A6, XXREAL_0:1; ::_thesis: verum
end;

theorem :: JORDAN1B:24
for G being Go-board
for i, j, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 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 & not j = n holds
j = n -' 1
proof
let G be Go-board; ::_thesis: for i, j, m, n being Element of NAT
for p being Point of (TOP-REAL 2) st 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 & not j = n holds
j = n -' 1
let i, j, m, n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2) st 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 & not j = n holds
j = n -' 1
let p be Point of (TOP-REAL 2); ::_thesis: ( 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 & not j = n implies j = n -' 1 )
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 ; ::_thesis: ( j = n or j = n -' 1 )
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;
percases ( j = width G or j < width G ) by A4, XXREAL_0:1;
suppose j = width G ; ::_thesis: ( j = n or j = n -' 1 )
hence  ( j = n or j = n -' 1 ) by A1, A2, A5, A6, A7, A8, A9, A10, Th23; ::_thesis: verum
end;
suppose j < width G ; ::_thesis: ( j = n or j = n -' 1 )
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, A3, GOBRD11:32;
then consider r, s being 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 j <= n or not n <= j + 1 ) ; ::_thesis: contradiction
percases ( j > n or n > j + 1 ) by A17;
suppose j > n ; ::_thesis: contradiction
hence  contradiction by A4, A7, A10, A12, A11, A14, A16, GOBOARD5:4; ::_thesis: verum
end;
supposeA18: n > j + 1 ; ::_thesis: contradiction
 1 <= j + 1 by NAT_1:11;
hence  contradiction by A8, A10, A12, A11, A15, A16, A18, GOBOARD5:4; ::_thesis: verum
end;
end;
end;
hence  ( j = n or j = n -' 1 ) by Lm2; ::_thesis: verum
end;
end;
end;

theorem Th25: :: JORDAN1B:25
for n being Element of NAT
for C being Simple_closed_curve
for i being Element of 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 n be Element of NAT ; ::_thesis: for C being Simple_closed_curve
for i being Element of 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
let C be Simple_closed_curve; ::_thesis: for i being Element of 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
let i be Element of NAT ; ::_thesis: ( 1 < i & i < len (Gauge (C,n)) implies LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Upper_Arc C )
assume that
A1: 1 < i and
A2: i < len (Gauge (C,n)) ; ::_thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Upper_Arc C
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: ((Gauge (C,n)) * (i,2)) `1 = ((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 <= ((Gauge (C,n)) * (i,2)) `1 by A2, A5, A3, SPRECT_3:13;
then A10: W-bound C <= ((Gauge (C,n)) * (i,2)) `1 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  ((Gauge (C,n)) * (i,2)) `1 <= ((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: ((Gauge (C,n)) * (i,2)) `1 <= 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  LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Upper_Arc C by A6, A8, TOPREAL1:6, XBOOLE_1:63; ::_thesis: verum
end;

theorem Th26: :: JORDAN1B:26
for n being Element of NAT
for C being Simple_closed_curve
for i being Element of 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 n be Element of NAT ; ::_thesis: for C being Simple_closed_curve
for i being Element of 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
let C be Simple_closed_curve; ::_thesis: for i being Element of 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
let i be Element of NAT ; ::_thesis: ( 1 < i & i < len (Gauge (C,n)) implies LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Lower_Arc C )
assume that
A1: 1 < i and
A2: i < len (Gauge (C,n)) ; ::_thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Lower_Arc C
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: ((Gauge (C,n)) * (i,2)) `1 = ((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 <= ((Gauge (C,n)) * (i,2)) `1 by A2, A5, A3, SPRECT_3:13;
then A10: W-bound C <= ((Gauge (C,n)) * (i,2)) `1 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  ((Gauge (C,n)) * (i,2)) `1 <= ((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: ((Gauge (C,n)) * (i,2)) `1 <= 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  LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Lower_Arc C by A6, A8, TOPREAL1:6, XBOOLE_1:63; ::_thesis: verum
end;

theorem :: JORDAN1B:27
for n being Element of NAT
for C being 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 n be Element of NAT ; ::_thesis: for C being 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
let C be Simple_closed_curve; ::_thesis: LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc C
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  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, Th15, Th25; ::_thesis: verum
end;

theorem :: JORDAN1B:28
for n being Element of NAT
for C being 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 n be Element of NAT ; ::_thesis: for C being 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
let C be Simple_closed_curve; ::_thesis: LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Lower_Arc C
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  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, Th15, Th26; ::_thesis: verum
end;

theorem Th29: :: JORDAN1B:29
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Element of 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 n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Element of 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)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for i being Element of 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)))
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) implies LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) )
assume that
A1: 1 <= i and
A2: i <= len (Gauge (C,n)) ; ::_thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (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 <= ((Gauge (C,n)) * (i,1)) `1 by A1, A2, A5, SPRECT_3:13;
then A7: W-bound (L~ (Cage (C,n))) <= ((Gauge (C,n)) * (i,1)) `1 by A5, JORDAN1A:73;
 ((Gauge (C,n)) * (i,1)) `1 <= ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 by A1, A2, A6, A5, SPRECT_3:13;
then A8: ((Gauge (C,n)) * (i,1)) `1 <= E-bound (L~ (Cage (C,n))) by A5, JORDAN1A:71;
 ((Gauge (C,n)) * (i,1)) `1 = ((Gauge (C,n)) * (i,(len (Gauge (C,n))))) `1 by A1, A2, A6, A5, GOBOARD5:2;
hence  LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) by A3, A4, A7, A8, JORDAN6:69; ::_thesis: verum
end;

theorem Th30: :: JORDAN1B:30
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Element of 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 n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Element of 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)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for i being Element of 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)))
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) implies LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Lower_Arc (L~ (Cage (C,n))) )
assume that
A1: 1 <= i and
A2: i <= len (Gauge (C,n)) ; ::_thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Lower_Arc (L~ (Cage (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 <= ((Gauge (C,n)) * (i,1)) `1 by A1, A2, A5, SPRECT_3:13;
then A7: W-bound (L~ (Cage (C,n))) <= ((Gauge (C,n)) * (i,1)) `1 by A5, JORDAN1A:73;
 ((Gauge (C,n)) * (i,1)) `1 <= ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 by A1, A2, A6, A5, SPRECT_3:13;
then A8: ((Gauge (C,n)) * (i,1)) `1 <= E-bound (L~ (Cage (C,n))) by A5, JORDAN1A:71;
 ((Gauge (C,n)) * (i,1)) `1 = ((Gauge (C,n)) * (i,(len (Gauge (C,n))))) `1 by A1, A2, A6, A5, GOBOARD5:2;
hence  LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Lower_Arc (L~ (Cage (C,n))) by A3, A4, A7, A8, JORDAN6:70; ::_thesis: verum
end;

theorem :: JORDAN1B:31
for n being Element of NAT
for C being connected compact non horizontal non vertical 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 n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical 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)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: 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)))
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  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, Th29; ::_thesis: verum
end;

theorem :: JORDAN1B:32
for n being Element of NAT
for C being connected compact non horizontal non vertical 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 n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical 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)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: 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)))
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  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, Th30; ::_thesis: verum
end;

theorem Th33: :: JORDAN1B:33
for G being Go-board
for j being Element of NAT st j <= width G holds
not cell (G,0,j) is bounded
proof
let G be Go-board; ::_thesis: for j being Element of NAT st j <= width G holds
not cell (G,0,j) is bounded
let j be Element of NAT ; ::_thesis: ( j <= width G implies not cell (G,0,j) is bounded )
assume A1: j <= width G ; ::_thesis: not cell (G,0,j) is bounded
percases ( j = 0 or ( j >= 1 & j < width G ) or j = width G ) by A1, NAT_1:14, XXREAL_0:1;
suppose j = 0 ; ::_thesis: not cell (G,0,j) is bounded
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;
 for r being Real ex q being Point of (TOP-REAL 2) st
( q in cell (G,0,j) & not |.q.| < r )
proof
let r be Real; ::_thesis: ex q being Point of (TOP-REAL 2) st
( q in cell (G,0,j) & not |.q.| < r )
take q = |[(min ((- r),((G * (1,1)) `1))),(min ((- r),((G * (1,1)) `2)))]|; ::_thesis: ( q in cell (G,0,j) & not |.q.| < r )
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; ::_thesis: not |.q.| < r
A4: abs (q `1) <= |.q.| by JGRAPH_1:33;
percases ( r <= 0 or r > 0 ) ;
suppose r <= 0 ; ::_thesis: not |.q.| < r
hence  not |.q.| < r ; ::_thesis: verum
end;
supposeA5: r > 0 ; ::_thesis: not |.q.| < r
 q `1 = min ((- r),((G * (1,1)) `1)) by EUCLID:52;
then A6: abs (- r) <= abs (q `1) by A5, TOPREAL6:3, XXREAL_0:17;
 - (- r) > 0 by A5;
then  - r < 0 ;
then  - (- r) <= abs (q `1) by A6, ABSVALUE:def_1;
hence  not |.q.| < r by A4, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  not cell (G,0,j) is bounded by JORDAN2C:34; ::_thesis: verum
end;
supposeA7: ( j >= 1 & j < width G ) ; ::_thesis: not cell (G,0,j) is bounded
then A8: cell (G,0,j) =  {  |[r,s]| where r, s is Element of REAL : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 )  }  by GOBRD11:26;
 for r being Real ex q being Point of (TOP-REAL 2) st
( q in cell (G,0,j) & not |.q.| < r )
proof
 len G <> 0 by GOBOARD1:def_3;
then A9: 1 <= len G by NAT_1:14;
let r be Real; ::_thesis: ex q being Point of (TOP-REAL 2) st
( q in cell (G,0,j) & not |.q.| < r )
take q = |[(min ((- r),((G * (1,1)) `1))),((G * (1,j)) `2)]|; ::_thesis: ( q in cell (G,0,j) & not |.q.| < r )
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; ::_thesis: not |.q.| < r
A12: abs (q `1) <= |.q.| by JGRAPH_1:33;
percases ( r <= 0 or r > 0 ) ;
suppose r <= 0 ; ::_thesis: not |.q.| < r
hence  not |.q.| < r ; ::_thesis: verum
end;
supposeA13: r > 0 ; ::_thesis: not |.q.| < r
 q `1 = min ((- r),((G * (1,1)) `1)) by EUCLID:52;
then A14: abs (- r) <= abs (q `1) by A13, TOPREAL6:3, XXREAL_0:17;
 - (- r) > 0 by A13;
then  - r < 0 ;
then  - (- r) <= abs (q `1) by A14, ABSVALUE:def_1;
hence  not |.q.| < r by A12, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  not cell (G,0,j) is bounded by JORDAN2C:34; ::_thesis: verum
end;
suppose j = width G ; ::_thesis: not cell (G,0,j) is bounded
then A15: cell (G,0,j) =  {  |[r,s]| where r, s is Element of REAL : ( r <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s )  }  by GOBRD11:25;
 for r being Real ex q being Point of (TOP-REAL 2) st
( q in cell (G,0,j) & not |.q.| < r )
proof
let r be Real; ::_thesis: ex q being Point of (TOP-REAL 2) st
( q in cell (G,0,j) & not |.q.| < r )
take q = |[((G * (1,1)) `1),(max (r,((G * (1,(width G))) `2)))]|; ::_thesis: ( q in cell (G,0,j) & not |.q.| < r )
A16: abs (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; ::_thesis: not |.q.| < r
percases ( r <= 0 or r > 0 ) ;
suppose r <= 0 ; ::_thesis: not |.q.| < r
hence  not |.q.| < r ; ::_thesis: verum
end;
supposeA17: r > 0 ; ::_thesis: not |.q.| < r
 q `2 = max (r,((G * (1,(width G))) `2)) by EUCLID:52;
then  r <= q `2 by XXREAL_0:25;
then  r <= abs (q `2) by A17, ABSVALUE:def_1;
hence  not |.q.| < r by A16, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  not cell (G,0,j) is bounded by JORDAN2C:34; ::_thesis: verum
end;
end;
end;

theorem Th34: :: JORDAN1B:34
for G being Go-board
for i being Element of NAT st i <= width G holds
not cell (G,(len G),i) is bounded
proof
let G be Go-board; ::_thesis: for i being Element of NAT st i <= width G holds
not cell (G,(len G),i) is bounded
let i be Element of NAT ; ::_thesis: ( i <= width G implies not cell (G,(len G),i) is bounded )
assume A1: i <= width G ; ::_thesis: not cell (G,(len G),i) is bounded
percases ( i = 0 or ( i >= 1 & i < width G ) or i = width G ) by A1, NAT_1:14, XXREAL_0:1;
supposeA2: i = 0 ; ::_thesis: not cell (G,(len G),i) is bounded
A3: cell (G,(len G),0) =  {  |[r,s]| where r, s is Element of REAL : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 )  }  by GOBRD11:27;
 for r being Real ex q being Point of (TOP-REAL 2) st
( q in cell (G,(len G),0) & not |.q.| < r )
proof
let r be Real; ::_thesis: ex q being Point of (TOP-REAL 2) st
( q in cell (G,(len G),0) & not |.q.| < r )
take q = |[((G * ((len G),1)) `1),(min ((- r),((G * (1,1)) `2)))]|; ::_thesis: ( q in cell (G,(len G),0) & not |.q.| < r )
A4: abs (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; ::_thesis: not |.q.| < r
percases ( r <= 0 or r > 0 ) ;
suppose r <= 0 ; ::_thesis: not |.q.| < r
hence  not |.q.| < r ; ::_thesis: verum
end;
supposeA5: r > 0 ; ::_thesis: not |.q.| < r
 q `2 = min ((- r),((G * (1,1)) `2)) by EUCLID:52;
then A6: abs (- r) <= abs (q `2) by A5, TOPREAL6:3, XXREAL_0:17;
 - (- r) > 0 by A5;
then  - r < 0 ;
then  - (- r) <= abs (q `2) by A6, ABSVALUE:def_1;
hence  not |.q.| < r by A4, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  not cell (G,(len G),i) is bounded by A2, JORDAN2C:34; ::_thesis: verum
end;
supposeA7: ( i >= 1 & i < width G ) ; ::_thesis: not cell (G,(len G),i) is bounded
then A8: cell (G,(len G),i) =  {  |[r,s]| where r, 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;
 for r being Real ex q being Point of (TOP-REAL 2) st
( q in cell (G,(len G),i) & not |.q.| < r )
proof
 len G <> 0 by GOBOARD1:def_3;
then A9: 1 <= len G by NAT_1:14;
let r be Real; ::_thesis: ex q being Point of (TOP-REAL 2) st
( q in cell (G,(len G),i) & not |.q.| < r )
take q = |[(max (r,((G * ((len G),1)) `1))),((G * (1,i)) `2)]|; ::_thesis: ( q in cell (G,(len G),i) & not |.q.| < r )
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; ::_thesis: not |.q.| < r
A12: abs (q `1) <= |.q.| by JGRAPH_1:33;
percases ( r <= 0 or r > 0 ) ;
suppose r <= 0 ; ::_thesis: not |.q.| < r
hence  not |.q.| < r ; ::_thesis: verum
end;
supposeA13: r > 0 ; ::_thesis: not |.q.| < r
 q `1 = max (r,((G * ((len G),1)) `1)) by EUCLID:52;
then  q `1 >= r by XXREAL_0:25;
then  r <= abs (q `1) by A13, ABSVALUE:def_1;
hence  not |.q.| < r by A12, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  not cell (G,(len G),i) is bounded by JORDAN2C:34; ::_thesis: verum
end;
supposeA14: i = width G ; ::_thesis: not cell (G,(len G),i) is bounded
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;
 for r being Real ex q being Point of (TOP-REAL 2) st
( q in cell (G,(len G),i) & not |.q.| < r )
proof
let r be Real; ::_thesis: ex q being Point of (TOP-REAL 2) st
( q in cell (G,(len G),i) & not |.q.| < r )
take q = |[((G * ((len G),1)) `1),(max (r,((G * (1,(width G))) `2)))]|; ::_thesis: ( q in cell (G,(len G),i) & not |.q.| < r )
A16: abs (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; ::_thesis: not |.q.| < r
percases ( r <= 0 or r > 0 ) ;
suppose r <= 0 ; ::_thesis: not |.q.| < r
hence  not |.q.| < r ; ::_thesis: verum
end;
supposeA17: r > 0 ; ::_thesis: not |.q.| < r
 q `2 = max (r,((G * (1,(width G))) `2)) by EUCLID:52;
then  r <= q `2 by XXREAL_0:25;
then  r <= abs (q `2) by A17, ABSVALUE:def_1;
hence  not |.q.| < r by A16, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  not cell (G,(len G),i) is bounded by JORDAN2C:34; ::_thesis: verum
end;
end;
end;

theorem Th35: :: JORDAN1B:35
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n being Element of NAT st j <= width (Gauge (C,n)) holds
cell ((Gauge (C,n)),0,j) c= UBD C
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for j, n being Element of NAT st j <= width (Gauge (C,n)) holds
cell ((Gauge (C,n)),0,j) c= UBD C
let j, n be Element of NAT ; ::_thesis: ( j <= width (Gauge (C,n)) implies cell ((Gauge (C,n)),0,j) c= UBD C )
assume A1: j <= width (Gauge (C,n)) ; ::_thesis: cell ((Gauge (C,n)),0,j) c= UBD C
A2: not C ` is empty by JORDAN2C:66;
A3: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
then A4: not cell ((Gauge (C,n)),0,j) is 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 being 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  cell ((Gauge (C,n)),0,j) c= UBD C by A7, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th36: :: JORDAN1B:36
for E being compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n being Element of NAT st j <= len (Gauge (E,n)) holds
cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= UBD E
proof
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for j, n being Element of NAT st j <= len (Gauge (E,n)) holds
cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= UBD E
let j, n be Element of NAT ; ::_thesis: ( j <= len (Gauge (E,n)) implies cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= UBD E )
A1: not E ` is empty by JORDAN2C:66;
assume A2: j <= len (Gauge (E,n)) ; ::_thesis: cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= UBD E
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: not cell ((Gauge (E,n)),(len (Gauge (E,n))),j) is empty by A2, JORDAN1A:24;
 cell ((Gauge (E,n)),(len (Gauge (E,n))),j) is connected by A4, A2, JORDAN1A:25;
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, 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  cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= UBD E by A7, XBOOLE_1:1; ::_thesis: verum
end;

Lm3:  for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n, i being Element of NAT st j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i <> 0
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for j, n, i being Element of NAT st j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i <> 0
let j, n, i be Element of NAT ; ::_thesis: ( j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies i <> 0 )
assume that
A1: j <= width (Gauge (C,n)) and
A2: cell ((Gauge (C,n)),i,j) c= BDD C and
A3: i = 0 ; ::_thesis: contradiction
A4: cell ((Gauge (C,n)),0,j) c= UBD C by A1, Th35;
 0 <= len (Gauge (C,n)) ;
then  not cell ((Gauge (C,n)),0,j) is empty by A1, JORDAN1A:24;
hence  contradiction by A2, A3, A4, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;

Lm4:  for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j <> 0
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j <> 0
let i, n, j be Element of NAT ; ::_thesis: ( i <= len (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies j <> 0 )
assume that
A1: i <= len (Gauge (C,n)) and
A2: cell ((Gauge (C,n)),i,j) c= BDD C and
A3: j = 0 ; ::_thesis: contradiction
A4: cell ((Gauge (C,n)),i,0) c= UBD C by A1, JORDAN1A:49;
 0 <= width (Gauge (C,n)) ;
then  not cell ((Gauge (C,n)),i,0) is empty by A1, JORDAN1A:24;
hence  contradiction by A2, A3, A4, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;

Lm5:  for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n, i being Element of NAT st j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i <> len (Gauge (C,n))
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for j, n, i being Element of NAT st j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i <> len (Gauge (C,n))
let j, n, i be Element of NAT ; ::_thesis: ( j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies i <> len (Gauge (C,n)) )
assume that
A1: j <= width (Gauge (C,n)) and
A2: cell ((Gauge (C,n)),i,j) c= BDD C ; ::_thesis: i <> len (Gauge (C,n))
A3: not cell ((Gauge (C,n)),(len (Gauge (C,n))),j) is empty by A1, JORDAN1A:24;
assume A4: i = len (Gauge (C,n)) ; ::_thesis: contradiction
 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; ::_thesis: verum
end;

Lm6:  for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j <> width (Gauge (C,n))
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j <> width (Gauge (C,n))
let i, n, j be Element of NAT ; ::_thesis: ( i <= len (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies j <> width (Gauge (C,n)) )
assume that
A1: i <= len (Gauge (C,n)) and
A2: cell ((Gauge (C,n)),i,j) c= BDD C ; ::_thesis: j <> width (Gauge (C,n))
A3: cell ((Gauge (C,n)),i,(width (Gauge (C,n)))) c= UBD C by A1, JORDAN1A:50;
assume A4: j = width (Gauge (C,n)) ; ::_thesis: contradiction
 not cell ((Gauge (C,n)),i,(width (Gauge (C,n)))) is empty by A1, JORDAN1A:24;
hence  contradiction by A2, A4, A3, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;

theorem Th37: :: JORDAN1B:37
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j > 1
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j > 1
let i, n, j be Element of NAT ; ::_thesis: ( i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies j > 1 )
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 ; ::_thesis: contradiction
percases ( j = 0 or j = 1 ) by A4, NAT_1:25;
suppose j = 0 ; ::_thesis: contradiction
hence  contradiction by A1, A3, Lm4; ::_thesis: verum
end;
supposeA5: j = 1 ; ::_thesis: contradiction
 BDD C c= C ` by JORDAN2C:25;
then A6: cell ((Gauge (C,n)),i,1) c= C ` by A3, A5, XBOOLE_1:1;
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 GOBOARD1:def_3;
then A10: 0 + 1 <= width (Gauge (C,n)) by NAT_1:14;
then A11: not cell ((Gauge (C,n)),i,1) is 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; ::_thesis: verum
end;
end;
end;

theorem Th38: :: JORDAN1B:38
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i > 1
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i > 1
let i, n, j be Element of NAT ; ::_thesis: ( i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies i > 1 )
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 ; ::_thesis: contradiction
percases ( i = 0 or i = 1 ) by A4, NAT_1:25;
suppose i = 0 ; ::_thesis: contradiction
hence  contradiction by A2, A3, Lm3; ::_thesis: verum
end;
supposeA5: i = 1 ; ::_thesis: contradiction
 BDD C c= C ` by JORDAN2C:25;
then A6: cell ((Gauge (C,n)),1,j) c= C ` by A3, A5, XBOOLE_1:1;
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 GOBOARD1:def_3;
then A10: 0 + 1 <= len (Gauge (C,n)) by NAT_1:14;
then A11: not cell ((Gauge (C,n)),1,j) is 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; ::_thesis: verum
end;
end;
end;

theorem Th39: :: JORDAN1B:39
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j + 1 < width (Gauge (C,n))
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j + 1 < width (Gauge (C,n))
let i, n, j be Element of NAT ; ::_thesis: ( 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)) )
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 ; ::_thesis: j + 1 < width (Gauge (C,n))
A4: ( j < width (Gauge (C,n)) or j = width (Gauge (C,n)) ) by A2, XXREAL_0:1;
assume  j + 1 >= width (Gauge (C,n)) ; ::_thesis: contradiction
then A5: ( j + 1 > width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) ) by XXREAL_0:1;
percases ( j = width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) ) by A5, A4, NAT_1:13;
suppose j = width (Gauge (C,n)) ; ::_thesis: contradiction
hence  contradiction by A1, A3, Lm6; ::_thesis: verum
end;
suppose j + 1 = width (Gauge (C,n)) ; ::_thesis: contradiction
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, XBOOLE_1:1;
A8: width (Gauge (C,n)) <> 0 by GOBOARD1:def_3;
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: not cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) is 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; ::_thesis: verum
end;
end;
end;

theorem Th40: :: JORDAN1B:40
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i + 1 < len (Gauge (C,n))
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i + 1 < len (Gauge (C,n))
let i, n, j be Element of NAT ; ::_thesis: ( 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)) )
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 ; ::_thesis: i + 1 < len (Gauge (C,n))
A4: ( i < len (Gauge (C,n)) or i = len (Gauge (C,n)) ) by A1, XXREAL_0:1;
assume  i + 1 >= len (Gauge (C,n)) ; ::_thesis: contradiction
then A5: ( i + 1 > len (Gauge (C,n)) or i + 1 = len (Gauge (C,n)) ) by XXREAL_0:1;
percases ( i = len (Gauge (C,n)) or i + 1 = len (Gauge (C,n)) ) by A5, A4, NAT_1:13;
suppose i = len (Gauge (C,n)) ; ::_thesis: contradiction
hence  contradiction by A2, A3, Lm5; ::_thesis: verum
end;
suppose i + 1 = len (Gauge (C,n)) ; ::_thesis: contradiction
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, XBOOLE_1:1;
A8: len (Gauge (C,n)) <> 0 by GOBOARD1:def_3;
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: not cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),j) is 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; ::_thesis: verum
end;
end;
end;

theorem :: JORDAN1B:41
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT st ex i, j being Element of NAT st
( i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C ) holds
n >= 1
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT st ex i, j being Element of NAT st
( i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C ) holds
n >= 1
let n be Element of NAT ; ::_thesis: ( ex i, j being Element of NAT st
( i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C ) implies n >= 1 )
A1: 2 |^ 0 = 1 by NEWTON:4;
given i, j being Element of NAT  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 ; ::_thesis: n >= 1
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 ; ::_thesis: contradiction
 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;
percases ( j = 0 or j = 1 or i = 0 or i = 1 or ( j = 2 & i = 2 ) or j = 3 or j = 4 or i = 3 or i = 4 ) by A2, A3, A9, A8, NAT_1:28;
suppose ( j = 0 or j = 1 ) ; ::_thesis: contradiction
hence  contradiction by A2, A3, A4, Th37; ::_thesis: verum
end;
suppose ( i = 0 or i = 1 ) ; ::_thesis: contradiction
hence  contradiction by A2, A3, A4, Th38; ::_thesis: verum
end;
suppose ( j = 2 & i = 2 ) ; ::_thesis: contradiction
then  cell ((Gauge (C,0)),2,2) c= BDD C by A4, A7, NAT_1:14;
hence  contradiction by Th18; ::_thesis: verum
end;
suppose ( j = 3 or j = 4 or i = 3 or i = 4 ) ; ::_thesis: contradiction
hence  contradiction by A5, A6, A9, A8; ::_thesis: verum
end;
end;
end;