:: JORDAN11 semantic presentation

begin

     Lm1:  for i, j, k being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st i > 0 & 1 <= j & j <= width (Gauge (C,i)) & k <= j & 1 <= k & k <= width (Gauge (C,i)) & (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Upper_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} & (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} holds
LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= Cl (RightComp (Cage (C,i)))
proof
let i, j, k be Element of NAT ; ::_thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st i > 0 & 1 <= j & j <= width (Gauge (C,i)) & k <= j & 1 <= k & k <= width (Gauge (C,i)) & (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Upper_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} & (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} holds
LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= Cl (RightComp (Cage (C,i)))
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ( i > 0 & 1 <= j & j <= width (Gauge (C,i)) & k <= j & 1 <= k & k <= width (Gauge (C,i)) & (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Upper_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} & (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} implies LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= Cl (RightComp (Cage (C,i))) )
assume that
A1: i > 0 and
A2: 1 <= j and
A3: j <= width (Gauge (C,i)) and
A4: k <= j and
A5: 1 <= k and
A6: k <= width (Gauge (C,i)) and
A7: (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Upper_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} and
A8: (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))) = {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} ; ::_thesis: LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= Cl (RightComp (Cage (C,i)))
set p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j);
set q = (Gauge (C,i)) * ((Center (Gauge (C,i))),k);
set S = RightComp (Cage (C,i));
A9: {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} c= Lower_Arc (L~ (Cage (C,i))) by A8, XBOOLE_1:17;
A10: X-SpanStart (C,i) = Center (Gauge (C,i)) by JORDAN1B:16;
then A11: 1 < Center (Gauge (C,i)) by JORDAN1H:49, XXREAL_0:2;
A12: Center (Gauge (C,i)) < len (Gauge (C,i)) by A10, JORDAN1H:49;
then A13: [(Center (Gauge (C,i))),j] in Indices (Gauge (C,i)) by A2, A3, A11, MATRIX_1:36;
 (Gauge (C,i)) * ((Center (Gauge (C,i))),j) in {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} by TARSKI:def_1;
then  (Gauge (C,i)) * ((Center (Gauge (C,i))),j) in Upper_Arc (L~ (Cage (C,i))) by A7, XBOOLE_0:def_4;
then A14: (Gauge (C,i)) * ((Center (Gauge (C,i))),j) in L~ (Upper_Seq (C,i)) by A1, JORDAN1G:55;
A15: [(Center (Gauge (C,i))),k] in Indices (Gauge (C,i)) by A5, A6, A11, A12, MATRIX_1:36;
 (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} by TARSKI:def_1;
then  (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Lower_Arc (L~ (Cage (C,i))) by A8, XBOOLE_0:def_4;
then  (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in L~ (Lower_Seq (C,i)) by A1, JORDAN1G:56;
then  j <> k by A2, A6, A11, A12, A14, JORDAN1J:57;
then A16: (Gauge (C,i)) * ((Center (Gauge (C,i))),j) <> (Gauge (C,i)) * ((Center (Gauge (C,i))),k) by A13, A15, JORDAN1H:26;
set A = (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) \ {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))};
(LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Cage (C,i))) = (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ ((Upper_Arc (L~ (Cage (C,i)))) \/ (Lower_Arc (L~ (Cage (C,i))))) by JORDAN6:50
.= ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Upper_Arc (L~ (Cage (C,i))))) \/ ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i))))) by XBOOLE_1:23
.= {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} by A7, A8, ENUMSET1:1 ;
then  (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) \ {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} misses L~ (Cage (C,i)) by XBOOLE_1:90;
then A17: (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) \ {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} c= (L~ (Cage (C,i))) ` by SUBSET_1:23;
A18: C c= RightComp (Cage (C,i)) by JORDAN10:11;
 LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),k)),((Gauge (C,i)) * ((Center (Gauge (C,i))),j))) meets Upper_Arc C by A1, A3, A4, A5, A7, A8, A11, A12, JORDAN1J:61;
then A19: LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),k)),((Gauge (C,i)) * ((Center (Gauge (C,i))),j))) meets C by JORDAN6:61, XBOOLE_1:63;
 {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} c= Upper_Arc (L~ (Cage (C,i))) by A7, XBOOLE_1:17;
then  {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} \/ {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} c= (Upper_Arc (L~ (Cage (C,i)))) \/ (Lower_Arc (L~ (Cage (C,i)))) by A9, XBOOLE_1:13;
then  {((Gauge (C,i)) * ((Center (Gauge (C,i))),j))} \/ {((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} c= L~ (Cage (C,i)) by JORDAN6:50;
then A20: {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} c= L~ (Cage (C,i)) by ENUMSET1:1;
 L~ (Cage (C,i)) misses C by JORDAN10:5;
then  {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} misses C by A20, XBOOLE_1:63;
then A21: (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) \ {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} meets C by A19, XBOOLE_1:84;
A22: (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) \ {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} is convex by JORDAN1:46;
 RightComp (Cage (C,i)) is_a_component_of (L~ (Cage (C,i))) ` by GOBOARD9:def_2;
then  (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) \ {((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))} c= RightComp (Cage (C,i)) by A17, A21, A18, A22, GOBOARD9:4;
hence  LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),j)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= Cl (RightComp (Cage (C,i))) by A16, JORDAN1H:3; ::_thesis: verum
end;

Lm2:  for C being being_simple_closed_curve Subset of (TOP-REAL 2) ex n being Element of NAT st n is_sufficiently_large_for C
proof
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ex n being Element of NAT st n is_sufficiently_large_for C
set s = ((W-bound C) + (E-bound C)) / 2;
set e = (Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))));
set f = (Gauge (C,1)) * ((X-SpanStart (C,1)),1);
A1: len (Gauge (C,1)) = width (Gauge (C,1)) by JORDAN8:def_1;
A2: X-SpanStart (C,1) = Center (Gauge (C,1)) by JORDAN1B:16;
then  X-SpanStart (C,1) = ((len (Gauge (C,1))) div 2) + 1 by JORDAN1A:def_1;
then A3: 1 <= X-SpanStart (C,1) by NAT_1:11;
 len (Gauge (C,1)) >= 4 by JORDAN8:10;
then A4: 1 < len (Gauge (C,1)) by XXREAL_0:2;
then A5: ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `1 = ((W-bound C) + (E-bound C)) / 2 by A2, JORDAN1A:38;
then A6: (Gauge (C,1)) * ((X-SpanStart (C,1)),1) in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN1A:8;
 0 < len (Gauge (C,1)) by JORDAN8:10;
then  (len (Gauge (C,1))) div 2 < len (Gauge (C,1)) by INT_1:56;
then  ((len (Gauge (C,1))) div 2) + 1 <= len (Gauge (C,1)) by NAT_1:13;
then  X-SpanStart (C,1) <= len (Gauge (C,1)) by A2, JORDAN1A:def_1;
then A7: ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `2 < ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))) `2 by A3, A4, A1, GOBOARD5:4;
set e1 = proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))));
set f1 = proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1));
A8: proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))) = ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))) `2 by PSCOMP_1:def_6;
 4 <= len (Gauge (C,1)) by JORDAN8:10;
then A9: 1 <= len (Gauge (C,1)) by XXREAL_0:2;
set AA = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc C);
set BB = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Lower_Arc C);
deffunc H1( Element of NAT ) ->  Element of REAL = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,($1 + 1)))))));
consider Es being Real_Sequence such that
A10: for i being Element of NAT holds Es . i = H1(i) from FUNCT_2:sch_4();
reconsider A = proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc C)), B = proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Lower_Arc C)) as compact Subset of REAL by JCT_MISC:15;
deffunc H2( Element of NAT ) ->  Element of the carrier of (TOP-REAL 2) = |[(((W-bound C) + (E-bound C)) / 2),(Es . $1)]|;
consider E being Function of NAT, the carrier of (TOP-REAL 2) such that
A11: for i being Element of NAT holds E . i = H2(i) from FUNCT_2:sch_4();
A12: ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))) `1 = ((W-bound C) + (E-bound C)) / 2 by A2, A4, JORDAN1A:38;
then  (Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))) in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN1A:8;
then A13: LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) c= Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A6, JORDAN1A:13;
A14: A misses B
proof
assume  A meets B ; ::_thesis: contradiction
then consider z being set  such that
A15: z in A and
A16: z in B by XBOOLE_0:3;
reconsider z = z as Real by A15;
consider p being Point of (TOP-REAL 2) such that
A17: p in (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc C) and
A18: z = proj2 . p by A15, FUNCT_2:65;
A19: p in Upper_Arc C by A17, XBOOLE_0:def_4;
consider q being Point of (TOP-REAL 2) such that
A20: q in (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Lower_Arc C) and
A21: z = proj2 . q by A16, FUNCT_2:65;
A22: p `2 = proj2 . q by A18, A21, PSCOMP_1:def_6
.= q `2 by PSCOMP_1:def_6 ;
A23: q in Lower_Arc C by A20, XBOOLE_0:def_4;
A24: q in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A20, XBOOLE_0:def_4;
A25: p in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A17, XBOOLE_0:def_4;
then p `1 = ((W-bound C) + (E-bound C)) / 2 by A13, JORDAN6:31
.= q `1 by A13, A24, JORDAN6:31 ;
then  p = q by A22, TOPREAL3:6;
then  p in (Upper_Arc C) /\ (Lower_Arc C) by A19, A23, XBOOLE_0:def_4;
then A26: p in {(W-min C),(E-max C)} by JORDAN6:50;
percases ( p = W-min C or p = E-max C ) by A26, TARSKI:def_2;
supposeA27: p = W-min C ; ::_thesis: contradiction
A28: (W-min C) `1 = W-bound C by EUCLID:52;
 (W-min C) `1 = ((W-bound C) + (E-bound C)) / 2 by A13, A25, A27, JORDAN6:31;
hence  contradiction by A28, SPRECT_1:31; ::_thesis: verum
end;
supposeA29: p = E-max C ; ::_thesis: contradiction
A30: (E-max C) `1 = E-bound C by EUCLID:52;
 (E-max C) `1 = ((W-bound C) + (E-bound C)) / 2 by A13, A25, A29, JORDAN6:31;
hence  contradiction by A30, SPRECT_1:31; ::_thesis: verum
end;
end;
end;
deffunc H3( Element of NAT ) ->  Element of REAL = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . $1))) /\ (Lower_Arc (L~ (Cage (C,($1 + 1)))))));
consider Fs being Real_Sequence such that
A31: for i being Element of NAT holds Fs . i = H3(i) from FUNCT_2:sch_4();
deffunc H4( Element of NAT ) ->  Element of the carrier of (TOP-REAL 2) = |[(((W-bound C) + (E-bound C)) / 2),(Fs . $1)]|;
consider F being Function of NAT, the carrier of (TOP-REAL 2) such that
A32: for i being Element of NAT holds F . i = H4(i) from FUNCT_2:sch_4();
deffunc H5( Element of NAT ) ->  Element of K6(REAL) = proj2 .: (LSeg ((E . $1),(F . $1)));
consider S being Function of NAT,(bool REAL) such that
A33: for i being Element of NAT holds S . i = H5(i) from FUNCT_2:sch_4();
A34: for i being Element of NAT holds E . i in Upper_Arc (L~ (Cage (C,(i + 1))))
proof
let i be Element of NAT ; ::_thesis: E . i in Upper_Arc (L~ (Cage (C,(i + 1))))
set p = E . i;
A35: i + 1 >= 1 by NAT_1:11;
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
 DD c= the carrier of (TOP-REAL 2) ;
then  DD c= dom proj2 by FUNCT_2:def_1;
then A36: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A37: X-SpanStart (C,(i + 1)) = Center (Gauge (C,(i + 1))) by JORDAN1B:16;
then  LSeg (((Gauge (C,(i + 1))) * ((X-SpanStart (C,(i + 1))),1)),((Gauge (C,(i + 1))) * ((X-SpanStart (C,(i + 1))),(len (Gauge (C,(i + 1))))))) meets Upper_Arc (L~ (Cage (C,(i + 1)))) by JORDAN1B:31;
then  LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) meets Upper_Arc (L~ (Cage (C,(i + 1)))) by A2, A37, A35, JORDAN1A:44, XBOOLE_1:63;
then  DD <> {} by XBOOLE_0:def_7;
then  dom proj2 meets DD by A36, XBOOLE_0:def_7;
then A38: D <> {} by RELAT_1:118;
 Es . i = lower_bound D by A10;
then consider dd being Point of (TOP-REAL 2) such that
A39: dd in DD and
A40: Es . i = proj2 . dd by A38, FUNCT_2:65, RCOMP_1:14;
A41: dd in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A39, XBOOLE_0:def_4;
A42: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A11;
then  (E . i) `2 = Es . i by EUCLID:52;
then A43: dd `2 = (E . i) `2 by A40, PSCOMP_1:def_6;
 (E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by A42, EUCLID:52;
then A44: dd `1 = (E . i) `1 by A13, A41, JORDAN6:31;
 dd in Upper_Arc (L~ (Cage (C,(i + 1)))) by A39, XBOOLE_0:def_4;
hence  E . i in Upper_Arc (L~ (Cage (C,(i + 1)))) by A44, A43, TOPREAL3:6; ::_thesis: verum
end;
A45: for i being Element of NAT holds F . i in Lower_Arc (L~ (Cage (C,(i + 1))))
proof
let i be Element of NAT ; ::_thesis: F . i in Lower_Arc (L~ (Cage (C,(i + 1))))
set p = F . i;
A46: X-SpanStart (C,(i + 1)) = Center (Gauge (C,(i + 1))) by JORDAN1B:16;
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
A47: E . i in Upper_Arc (L~ (Cage (C,(i + 1)))) by A34;
 DD c= the carrier of (TOP-REAL 2) ;
then  DD c= dom proj2 by FUNCT_2:def_1;
then A48: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A49: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A11;
then A50: (E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
then  E . i in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN1A:8;
then A51: LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) c= Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A6, JORDAN1A:13;
(E . i) `2 = Es . i by A49, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) by A10 ;
then  ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & E . i = (Gauge (C,(i + 1))) * ((X-SpanStart (C,(i + 1))),j) ) by A2, A1, A46, A50, JORDAN1F:13;
then  LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i)) meets Lower_Arc (L~ (Cage (C,(i + 1)))) by A2, A46, A47, JORDAN1J:62;
then  DD <> {} by XBOOLE_0:def_7;
then  dom proj2 meets DD by A48, XBOOLE_0:def_7;
then A52: D <> {} by RELAT_1:118;
 Fs . i = upper_bound D by A31;
then consider dd being Point of (TOP-REAL 2) such that
A53: dd in DD and
A54: Fs . i = proj2 . dd by A52, FUNCT_2:65, RCOMP_1:14;
A55: dd in Lower_Arc (L~ (Cage (C,(i + 1)))) by A53, XBOOLE_0:def_4;
A56: F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A32;
then  (F . i) `2 = Fs . i by EUCLID:52;
then A57: dd `2 = (F . i) `2 by A54, PSCOMP_1:def_6;
A58: dd in LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A53, XBOOLE_0:def_4;
 (F . i) `1 = ((W-bound C) + (E-bound C)) / 2 by A56, EUCLID:52;
then  dd `1 = (F . i) `1 by A58, A51, JORDAN6:31;
hence  F . i in Lower_Arc (L~ (Cage (C,(i + 1)))) by A55, A57, TOPREAL3:6; ::_thesis: verum
end;
A59: for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B )
proof
let i be Element of NAT ; ::_thesis: ( S . i is interval & S . i meets A & S . i meets B )
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
A60: X-SpanStart (C,(i + 1)) = Center (Gauge (C,(i + 1))) by JORDAN1B:16;
 DD c= the carrier of (TOP-REAL 2) ;
then  DD c= dom proj2 by FUNCT_2:def_1;
then A61: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A62: 1 <= i + 1 by NAT_1:11;
 LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(len (Gauge (C,(i + 1))))))) meets Upper_Arc (L~ (Cage (C,(i + 1)))) by JORDAN1B:31;
then  LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) meets Upper_Arc (L~ (Cage (C,(i + 1)))) by A2, A62, JORDAN1A:44, XBOOLE_1:63;
then  DD <> {} by XBOOLE_0:def_7;
then  dom proj2 meets DD by A61, XBOOLE_0:def_7;
then A63: D <> {} by RELAT_1:118;
 Es . i = lower_bound D by A10;
then consider dd being Point of (TOP-REAL 2) such that
A64: dd in DD and
A65: Es . i = proj2 . dd by A63, FUNCT_2:65, RCOMP_1:14;
A66: dd in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) by A64, XBOOLE_0:def_4;
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
 DD c= the carrier of (TOP-REAL 2) ;
then  DD c= dom proj2 by FUNCT_2:def_1;
then A67: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A68: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A11;
then A69: (E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A70: F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A32;
then A71: (F . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A72: (F . i) `2 = Fs . i by A70, EUCLID:52
.= upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))))) by A31 ;
(E . i) `2 = Es . i by A68, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) by A10 ;
then consider j being Element of NAT  such that
A73: 1 <= j and
A74: j <= width (Gauge (C,(i + 1))) and
A75: E . i = (Gauge (C,(i + 1))) * ((X-SpanStart (C,(i + 1))),j) by A2, A1, A69, A60, JORDAN1F:13;
A76: E . i in Upper_Arc (L~ (Cage (C,(i + 1)))) by A34;
then consider k being Element of NAT  such that
A77: 1 <= k and
A78: k <= width (Gauge (C,(i + 1))) and
A79: F . i = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k) by A2, A60, A71, A73, A74, A75, A72, JORDAN1I:28;
(E . i) `2 = Es . i by A68, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) by A10 ;
then  ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & E . i = (Gauge (C,(i + 1))) * ((X-SpanStart (C,(i + 1))),j) ) by A2, A1, A69, A60, JORDAN1F:13;
then  LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i)) meets Lower_Arc (L~ (Cage (C,(i + 1)))) by A2, A60, A76, JORDAN1J:62;
then  DD <> {} by XBOOLE_0:def_7;
then  dom proj2 meets DD by A67, XBOOLE_0:def_7;
then A80: D <> {} by RELAT_1:118;
A81: (E . i) `2 = Es . i by A68, EUCLID:52
.= dd `2 by A65, PSCOMP_1:def_6 ;
 for p being real number st p in D holds
p <= (E . i) `2
proof
let p be real number ; ::_thesis: ( p in D implies p <= (E . i) `2 )
assume  p in D ; ::_thesis: p <= (E . i) `2
then consider x being set  such that
 x in dom proj2 and
A82: x in DD and
A83: p = proj2 . x by FUNCT_1:def_6;
A84: ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `2 <= (E . i) `2 by A7, A66, A81, TOPREAL1:4;
reconsider x = x as Point of (TOP-REAL 2) by A82;
 x in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i)) by A82, XBOOLE_0:def_4;
then  x `2 <= (E . i) `2 by A84, TOPREAL1:4;
hence  p <= (E . i) `2 by A83, PSCOMP_1:def_6; ::_thesis: verum
end;
then A85: upper_bound D <= (E . i) `2 by A80, SEQ_4:45;
 dd `1 = (E . i) `1 by A13, A69, A66, JORDAN6:31;
then A86: E . i in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A66, A81, TOPREAL3:6;
 Fs . i = upper_bound D by A31;
then consider dd being Point of (TOP-REAL 2) such that
A87: dd in DD and
A88: Fs . i = proj2 . dd by A80, FUNCT_2:65, RCOMP_1:14;
A89: (F . i) `2 = Fs . i by A70, EUCLID:52
.= dd `2 by A88, PSCOMP_1:def_6 ;
A90: dd in LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A87, XBOOLE_0:def_4;
 E . i in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A69, JORDAN1A:8;
then  LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) c= Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A6, JORDAN1A:13;
then  dd `1 = (F . i) `1 by A71, A90, JORDAN6:31;
then A91: F . i in LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A90, A89, TOPREAL3:6;
 (Gauge (C,1)) * ((X-SpanStart (C,1)),1) in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by RLTOPSP1:68;
then  LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i)) c= LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A86, TOPREAL1:6;
then A92: LSeg ((E . i),(F . i)) c= LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A86, A91, TOPREAL1:6;
A93: for x being set st x in (LSeg ((E . i),(F . i))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) holds
x = E . i
proof
let x be set ; ::_thesis: ( x in (LSeg ((E . i),(F . i))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) implies x = E . i )
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
assume A94: x in (LSeg ((E . i),(F . i))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) ; ::_thesis: x = E . i
then reconsider p = x as Point of (TOP-REAL 2) ;
A95: p in LSeg ((E . i),(F . i)) by A94, XBOOLE_0:def_4;
 p in Upper_Arc (L~ (Cage (C,(i + 1)))) by A94, XBOOLE_0:def_4;
then  p in DD by A92, A95, XBOOLE_0:def_4;
then  proj2 . p in D by FUNCT_2:35;
then A96: p `2 in D by PSCOMP_1:def_6;
 E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A11;
then A97: (E . i) `2 = Es . i by EUCLID:52
.= lower_bound D by A10 ;
 D is real-bounded by RCOMP_1:10;
then A98: (E . i) `2 <= p `2 by A97, A96, SEQ_4:def_2;
 p `2 <= (E . i) `2 by A72, A85, A95, TOPREAL1:4;
then A99: p `2 = (E . i) `2 by A98, XXREAL_0:1;
 p `1 = (E . i) `1 by A69, A71, A95, GOBOARD7:5;
hence  x = E . i by A99, TOPREAL3:6; ::_thesis: verum
end;
A100: (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) in LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))) by RLTOPSP1:68;
A101: (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) = {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))}
proof
thus  (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) c= {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} :: according to XBOOLE_0:def_10 ::_thesis: {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} c= (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1)))))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) or x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} )
assume  x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) ; ::_thesis: x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))}
then  x = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) by A60, A75, A79, A93;
hence  x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} or x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) )
assume  x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} ; ::_thesis: x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1)))))
then  x = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) by TARSKI:def_1;
hence  x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) by A60, A76, A75, A100, XBOOLE_0:def_4; ::_thesis: verum
end;
 E . i in LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by RLTOPSP1:68;
then A102: LSeg ((E . i),(F . i)) c= LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A91, TOPREAL1:6;
A103: for x being set st x in (LSeg ((E . i),(F . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) holds
x = F . i
proof
let x be set ; ::_thesis: ( x in (LSeg ((E . i),(F . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) implies x = F . i )
reconsider EE = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider E0 = proj2 .: EE as compact Subset of REAL by JCT_MISC:15;
assume A104: x in (LSeg ((E . i),(F . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) ; ::_thesis: x = F . i
then reconsider p = x as Point of (TOP-REAL 2) ;
A105: p in LSeg ((E . i),(F . i)) by A104, XBOOLE_0:def_4;
 p in Lower_Arc (L~ (Cage (C,(i + 1)))) by A104, XBOOLE_0:def_4;
then  p in EE by A102, A105, XBOOLE_0:def_4;
then  proj2 . p in E0 by FUNCT_2:35;
then A106: p `2 in E0 by PSCOMP_1:def_6;
 F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A32;
then A107: (F . i) `2 = Fs . i by EUCLID:52
.= upper_bound E0 by A31 ;
 E0 is real-bounded by RCOMP_1:10;
then A108: (F . i) `2 >= p `2 by A107, A106, SEQ_4:def_1;
 p `2 >= (F . i) `2 by A72, A85, A105, TOPREAL1:4;
then A109: p `2 = (F . i) `2 by A108, XXREAL_0:1;
 p `1 = (F . i) `1 by A69, A71, A105, GOBOARD7:5;
hence  x = F . i by A109, TOPREAL3:6; ::_thesis: verum
end;
A110: F . i in Lower_Arc (L~ (Cage (C,(i + 1)))) by A45;
A111: S . i = proj2 .: (LSeg ((E . i),(F . i))) by A33;
hence  S . i is interval by JCT_MISC:6; ::_thesis: ( S . i meets A & S . i meets B )
A112: Center (Gauge (C,(i + 1))) <= len (Gauge (C,(i + 1))) by JORDAN1B:13;
A113: (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k) in LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))) by RLTOPSP1:68;
A114: (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) = {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))}
proof
thus  (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) c= {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} :: according to XBOOLE_0:def_10 ::_thesis: {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} c= (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1)))))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) or x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} )
assume  x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) ; ::_thesis: x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))}
then  x = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k) by A60, A75, A79, A103;
hence  x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} or x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) )
assume  x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} ; ::_thesis: x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1)))))
then  x = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k) by TARSKI:def_1;
hence  x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) by A79, A110, A113, XBOOLE_0:def_4; ::_thesis: verum
end;
 1 <= Center (Gauge (C,(i + 1))) by JORDAN1B:11;
then A115: k <= j by A60, A73, A75, A72, A78, A79, A112, A85, GOBOARD5:4;
then  LSeg ((E . i),(F . i)) meets (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc C) by A60, A92, A74, A75, A77, A79, A101, A114, JORDAN1J:64, XBOOLE_1:77;
hence  S . i meets A by A111, JORDAN1A:14; ::_thesis: S . i meets B
 LSeg ((E . i),(F . i)) meets (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Lower_Arc C) by A60, A92, A74, A75, A77, A79, A115, A101, A114, JORDAN1J:63, XBOOLE_1:77;
hence  S . i meets B by A111, JORDAN1A:14; ::_thesis: verum
end;
 proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) = ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `2 by PSCOMP_1:def_6;
then A116: proj2 .: (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) = [.(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1))),(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))).] by A7, A8, SPRECT_1:53;
then A117: B c= [.(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1))),(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))).] by RELAT_1:123, XBOOLE_1:17;
 A c= [.(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1))),(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))).] by A116, RELAT_1:123, XBOOLE_1:17;
then consider r being real number  such that
A118: r in [.(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1))),(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))).] and
A119: not r in A \/ B and
A120: for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) by A14, A117, A59, JCT_MISC:12;
reconsider r = r as Real by XREAL_0:def_1;
set p = |[(((W-bound C) + (E-bound C)) / 2),r]|;
A121: |[(((W-bound C) + (E-bound C)) / 2),r]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
 for Y being set st Y in BDD-Family C holds
|[(((W-bound C) + (E-bound C)) / 2),r]| in Y
proof
let Y be set ; ::_thesis: ( Y in BDD-Family C implies |[(((W-bound C) + (E-bound C)) / 2),r]| in Y )
A122: BDD-Family C =  {  (Cl (BDD (L~ (Cage (C,k1))))) where k1 is Element of NAT : verum  }  by JORDAN10:def_2;
assume  Y in BDD-Family C ; ::_thesis: |[(((W-bound C) + (E-bound C)) / 2),r]| in Y
then consider k1 being Element of NAT  such that
A123: Y = Cl (BDD (L~ (Cage (C,k1)))) by A122;
consider k0 being Element of NAT  such that
A124: k1 <= k0 and
A125: r in S . k0 by A120;
A126: proj2 . (F . k0) = (F . k0) `2 by PSCOMP_1:def_6;
reconsider EE = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider CC = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider W = proj2 .: CC as compact Subset of REAL by JCT_MISC:15;
A127: Center (Gauge (C,(k0 + 1))) <= len (Gauge (C,(k0 + 1))) by JORDAN1B:13;
reconsider E0 = proj2 .: EE as compact Subset of REAL by JCT_MISC:15;
 CC c= the carrier of (TOP-REAL 2) ;
then  CC c= dom proj2 by FUNCT_2:def_1;
then A128: (dom proj2) /\ CC = CC by XBOOLE_1:28;
A129: RightComp (Cage (C,(k0 + 1))) c= RightComp (Cage (C,k0)) by JORDAN1H:48, NAT_1:11;
 RightComp (Cage (C,k0)) c= RightComp (Cage (C,k1)) by A124, JORDAN1H:48;
then  RightComp (Cage (C,(k0 + 1))) c= RightComp (Cage (C,k1)) by A129, XBOOLE_1:1;
then A130: Cl (RightComp (Cage (C,(k0 + 1)))) c= Cl (RightComp (Cage (C,k1))) by PRE_TOPC:19;
A131: E . k0 in Upper_Arc (L~ (Cage (C,(k0 + 1)))) by A34;
A132: 1 + 0 <= k0 + 1 by NAT_1:11;
A133: E . k0 in Upper_Arc (L~ (Cage (C,(k0 + 1)))) by A34;
A134: X-SpanStart (C,(k0 + 1)) = Center (Gauge (C,(k0 + 1))) by JORDAN1B:16;
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) as compact Subset of (TOP-REAL 2) ;
A135: proj2 . (E . k0) = (E . k0) `2 by PSCOMP_1:def_6;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
A136: Fs . k0 = upper_bound D by A31;
 DD c= the carrier of (TOP-REAL 2) ;
then  DD c= dom proj2 by FUNCT_2:def_1;
then A137: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A138: E . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Es . k0)]| by A11;
then A139: (E . k0) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
(E . k0) `2 = Es . k0 by A138, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))))) by A10 ;
then  ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(k0 + 1))) & E . k0 = (Gauge (C,(k0 + 1))) * ((X-SpanStart (C,(k0 + 1))),j) ) by A2, A1, A139, A134, JORDAN1F:13;
then A140: LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) meets Lower_Arc (L~ (Cage (C,(k0 + 1)))) by A2, A134, A133, JORDAN1J:62;
then  DD <> {} by XBOOLE_0:def_7;
then  dom proj2 meets DD by A137, XBOOLE_0:def_7;
then  D <> {} by RELAT_1:118;
then consider dd being Point of (TOP-REAL 2) such that
A141: dd in DD and
A142: Fs . k0 = proj2 . dd by A136, FUNCT_2:65, RCOMP_1:14;
A143: dd in LSeg ((E . k0),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A141, XBOOLE_0:def_4;
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
 DD c= the carrier of (TOP-REAL 2) ;
then  DD c= dom proj2 by FUNCT_2:def_1;
then A144: (dom proj2) /\ DD = DD by XBOOLE_1:28;
 LSeg (((Gauge (C,(k0 + 1))) * ((Center (Gauge (C,(k0 + 1)))),1)),((Gauge (C,(k0 + 1))) * ((Center (Gauge (C,(k0 + 1)))),(len (Gauge (C,(k0 + 1))))))) meets Upper_Arc (L~ (Cage (C,(k0 + 1)))) by JORDAN1B:31;
then  LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) meets Upper_Arc (L~ (Cage (C,(k0 + 1)))) by A2, A132, JORDAN1A:44, XBOOLE_1:63;
then  DD <> {} by XBOOLE_0:def_7;
then  dom proj2 meets DD by A144, XBOOLE_0:def_7;
then A145: D <> {} by RELAT_1:118;
A146: F . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Fs . k0)]| by A32;
then A147: (F . k0) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A148: (F . k0) `2 = Fs . k0 by A146, EUCLID:52
.= dd `2 by A142, PSCOMP_1:def_6 ;
 E . k0 in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A139, JORDAN1A:8;
then  LSeg ((E . k0),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) c= Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A6, JORDAN1A:13;
then  dd `1 = (F . k0) `1 by A147, A143, JORDAN6:31;
then A149: F . k0 in LSeg ((E . k0),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A143, A148, TOPREAL3:6;
 Es . k0 = lower_bound D by A10;
then consider dd being Point of (TOP-REAL 2) such that
A150: dd in DD and
A151: Es . k0 = proj2 . dd by A145, FUNCT_2:65, RCOMP_1:14;
A152: dd in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) by A150, XBOOLE_0:def_4;
A153: (E . k0) `2 = Es . k0 by A138, EUCLID:52
.= dd `2 by A151, PSCOMP_1:def_6 ;
then A154: ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `2 <= (E . k0) `2 by A7, A152, TOPREAL1:4;
then A155: (F . k0) `2 <= (E . k0) `2 by A143, A148, TOPREAL1:4;
 r in proj2 .: (LSeg ((E . k0),(F . k0))) by A33, A125;
then  r in [.(proj2 . (F . k0)),(proj2 . (E . k0)).] by A135, A126, A155, SPRECT_1:53;
then A156: |[(((W-bound C) + (E-bound C)) / 2),r]| in LSeg ((E . k0),(F . k0)) by A139, A147, JORDAN1A:11;
A157: F . k0 in Lower_Arc (L~ (Cage (C,(k0 + 1)))) by A45;
A158: (Gauge (C,1)) * ((X-SpanStart (C,1)),1) in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) by RLTOPSP1:68;
A159: E . k0 in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) by RLTOPSP1:68;
then A160: LSeg ((E . k0),(F . k0)) c= LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) by A149, TOPREAL1:6;
 for x being set holds
( x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) iff x = F . k0 )
proof
let x be set ; ::_thesis: ( x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) iff x = F . k0 )
thus  ( x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) implies x = F . k0 ) ::_thesis: ( x = F . k0 implies x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) )
proof
 F . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Fs . k0)]| by A32;
then A161: (F . k0) `2 = Fs . k0 by EUCLID:52
.= upper_bound E0 by A31 ;
assume A162: x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) ; ::_thesis: x = F . k0
then reconsider p = x as Point of (TOP-REAL 2) ;
A163: p in LSeg ((E . k0),(F . k0)) by A162, XBOOLE_0:def_4;
then A164: p `2 >= (F . k0) `2 by A155, TOPREAL1:4;
 p in Lower_Arc (L~ (Cage (C,(k0 + 1)))) by A162, XBOOLE_0:def_4;
then  p in EE by A160, A163, XBOOLE_0:def_4;
then  proj2 . p in E0 by FUNCT_2:35;
then A165: p `2 in E0 by PSCOMP_1:def_6;
 E0 is real-bounded by RCOMP_1:10;
then  (F . k0) `2 >= p `2 by A161, A165, SEQ_4:def_1;
then A166: p `2 = (F . k0) `2 by A164, XXREAL_0:1;
 p `1 = (F . k0) `1 by A139, A147, A163, GOBOARD7:5;
hence  x = F . k0 by A166, TOPREAL3:6; ::_thesis: verum
end;
assume A167: x = F . k0 ; ::_thesis: x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1)))))
then  x in LSeg ((E . k0),(F . k0)) by RLTOPSP1:68;
hence  x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) by A157, A167, XBOOLE_0:def_4; ::_thesis: verum
end;
then A168: (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) = {(F . k0)} by TARSKI:def_1;
A169: for p being real number st p in W holds
p <= (E . k0) `2
proof
let p be real number ; ::_thesis: ( p in W implies p <= (E . k0) `2 )
assume  p in W ; ::_thesis: p <= (E . k0) `2
then consider x being set  such that
 x in dom proj2 and
A170: x in CC and
A171: p = proj2 . x by FUNCT_1:def_6;
reconsider x = x as Point of (TOP-REAL 2) by A170;
 x in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) by A170, XBOOLE_0:def_4;
then  x `2 <= (E . k0) `2 by A154, TOPREAL1:4;
hence  p <= (E . k0) `2 by A171, PSCOMP_1:def_6; ::_thesis: verum
end;
 CC <> {} by A140, XBOOLE_0:def_7;
then  dom proj2 meets CC by A128, XBOOLE_0:def_7;
then  W <> {} by RELAT_1:118;
then A172: upper_bound W <= (E . k0) `2 by A169, SEQ_4:45;
 dd `1 = (E . k0) `1 by A13, A139, A152, JORDAN6:31;
then  E . k0 in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) by A152, A153, TOPREAL3:6;
then  LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) c= LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A158, TOPREAL1:6;
then A173: LSeg ((E . k0),(F . k0)) c= LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A149, A159, TOPREAL1:6;
 for x being set holds
( x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) iff x = E . k0 )
proof
let x be set ; ::_thesis: ( x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) iff x = E . k0 )
thus  ( x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) implies x = E . k0 ) ::_thesis: ( x = E . k0 implies x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) )
proof
 E . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Es . k0)]| by A11;
then A174: (E . k0) `2 = Es . k0 by EUCLID:52
.= lower_bound D by A10 ;
assume A175: x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) ; ::_thesis: x = E . k0
then reconsider p = x as Point of (TOP-REAL 2) ;
A176: p in LSeg ((E . k0),(F . k0)) by A175, XBOOLE_0:def_4;
then A177: p `2 <= (E . k0) `2 by A155, TOPREAL1:4;
 p in Upper_Arc (L~ (Cage (C,(k0 + 1)))) by A175, XBOOLE_0:def_4;
then  p in DD by A173, A176, XBOOLE_0:def_4;
then  proj2 . p in D by FUNCT_2:35;
then A178: p `2 in D by PSCOMP_1:def_6;
 D is real-bounded by RCOMP_1:10;
then  (E . k0) `2 <= p `2 by A174, A178, SEQ_4:def_2;
then A179: p `2 = (E . k0) `2 by A177, XXREAL_0:1;
 p `1 = (E . k0) `1 by A139, A147, A176, GOBOARD7:5;
hence  x = E . k0 by A179, TOPREAL3:6; ::_thesis: verum
end;
assume A180: x = E . k0 ; ::_thesis: x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1)))))
then  x in LSeg ((E . k0),(F . k0)) by RLTOPSP1:68;
hence  x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) by A131, A180, XBOOLE_0:def_4; ::_thesis: verum
end;
then A181: (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) = {(E . k0)} by TARSKI:def_1;
(E . k0) `2 = Es . k0 by A138, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))))) by A10 ;
then consider j being Element of NAT  such that
A182: 1 <= j and
A183: j <= width (Gauge (C,(k0 + 1))) and
A184: E . k0 = (Gauge (C,(k0 + 1))) * ((X-SpanStart (C,(k0 + 1))),j) by A2, A1, A139, A134, JORDAN1F:13;
A185: (F . k0) `2 = Fs . k0 by A146, EUCLID:52
.= upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))))) by A31 ;
then consider k being Element of NAT  such that
A186: 1 <= k and
A187: k <= width (Gauge (C,(k0 + 1))) and
A188: F . k0 = (Gauge (C,(k0 + 1))) * ((X-SpanStart (C,(k0 + 1))),k) by A2, A147, A134, A182, A183, A184, A131, JORDAN1I:28;
 1 <= Center (Gauge (C,(k0 + 1))) by JORDAN1B:11;
then  k <= j by A134, A182, A184, A185, A187, A188, A127, A172, GOBOARD5:4;
then  LSeg ((E . k0),(F . k0)) c= Cl (RightComp (Cage (C,(k0 + 1)))) by A134, A182, A183, A184, A186, A187, A188, A181, A168, Lm1;
then  |[(((W-bound C) + (E-bound C)) / 2),r]| in Cl (RightComp (Cage (C,(k0 + 1)))) by A156;
then  |[(((W-bound C) + (E-bound C)) / 2),r]| in Cl (RightComp (Cage (C,k1))) by A130;
hence  |[(((W-bound C) + (E-bound C)) / 2),r]| in Y by A123, GOBRD14:37; ::_thesis: verum
end;
then A189: |[(((W-bound C) + (E-bound C)) / 2),r]| in meet (BDD-Family C) by SETFAM_1:def_1;
A190: |[(((W-bound C) + (E-bound C)) / 2),r]| in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A5, A12, A118, JORDAN1A:11;
A191: now__::_thesis:_not_|[(((W-bound_C)_+_(E-bound_C))_/_2),r]|_in_C
assume  |[(((W-bound C) + (E-bound C)) / 2),r]| in C ; ::_thesis: contradiction
then  |[(((W-bound C) + (E-bound C)) / 2),r]| in (Lower_Arc C) \/ (Upper_Arc C) by JORDAN6:50;
then  |[(((W-bound C) + (E-bound C)) / 2),r]| in ((Lower_Arc C) \/ (Upper_Arc C)) /\ (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) by A190, XBOOLE_0:def_4;
then  |[(((W-bound C) + (E-bound C)) / 2),r]| in ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc C)) \/ ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Lower_Arc C)) by XBOOLE_1:23;
then  proj2 . |[(((W-bound C) + (E-bound C)) / 2),r]| in proj2 .: (((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc C)) \/ ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Lower_Arc C))) by FUNCT_2:35;
then  r in proj2 .: (((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc C)) \/ ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Lower_Arc C))) by PSCOMP_1:65;
hence  contradiction by A119, RELAT_1:120; ::_thesis: verum
end;
 meet (BDD-Family C) = C \/ (BDD C) by JORDAN10:21;
then  |[(((W-bound C) + (E-bound C)) / 2),r]| in BDD C by A191, A189, XBOOLE_0:def_3;
then consider n, i, j being Element of NAT  such that
A192: 1 < i and
A193: i < len (Gauge (C,n)) and
A194: 1 < j and
A195: j < width (Gauge (C,n)) and
A196: |[(((W-bound C) + (E-bound C)) / 2),r]| `1 <> ((Gauge (C,n)) * (i,j)) `1 and
A197: |[(((W-bound C) + (E-bound C)) / 2),r]| in cell ((Gauge (C,n)),i,j) and
A198: cell ((Gauge (C,n)),i,j) c= BDD C by JORDAN1C:23;
take  n ; ::_thesis: n is_sufficiently_large_for C
take  j ; :: according to JORDAN1H:def_3 ::_thesis: ( not width (Gauge (C,n)) <= j & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C )
thus  j < width (Gauge (C,n)) by A195; ::_thesis: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C
A199: X-SpanStart (C,n) = Center (Gauge (C,n)) by JORDAN1B:16;
A200: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A201: X-SpanStart (C,n) <= len (Gauge (C,n)) by JORDAN1H:49;
A202: 1 <= X-SpanStart (C,n) by JORDAN1H:49, XXREAL_0:2;
 n > 0 by A193, A195, A198, JORDAN1B:41;
then  ((Gauge (C,n)) * ((X-SpanStart (C,n)),j)) `1 = ((W-bound C) + (E-bound C)) / 2 by A2, A5, A194, A195, A199, A9, A200, JORDAN1A:36;
hence  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C by A121, A192, A193, A194, A195, A196, A197, A198, A202, A201, JORDAN1B:22; ::_thesis: verum
end;

definition
let C be being_simple_closed_curve Subset of (TOP-REAL 2);
func ApproxIndex C ->  Element of NAT  means :Def1: :: JORDAN11:def 1
( it is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds
j >= it ) );
existence
 ex b1 being Element of NAT st
( b1 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds
j >= b1 ) )
proof
defpred S1[ Element of NAT ] means $1 is_sufficiently_large_for C;
set X =  {  i where i is Element of NAT : S1[i]  }  ;
A1:  {  i where i is Element of NAT : S1[i]  }  is Subset of NAT from DOMAIN_1:sch_7();
consider i being Element of NAT  such that
A2: i is_sufficiently_large_for C by Lm2;
 i in  {  i where i is Element of NAT : S1[i]  }  by A2;
then reconsider X =  {  i where i is Element of NAT : S1[i]  }  as non empty Subset of NAT by A1;
take  min X ; ::_thesis: ( min X is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds
j >= min X ) )
 min X in X by XXREAL_2:def_7;
then  ex i being Element of NAT st
( i = min X & i is_sufficiently_large_for C ) ;
hence  min X is_sufficiently_large_for C ; ::_thesis: for j being Element of NAT st j is_sufficiently_large_for C holds
j >= min X
let j be Element of NAT ; ::_thesis: ( j is_sufficiently_large_for C implies j >= min X )
assume  j is_sufficiently_large_for C ; ::_thesis: j >= min X
then  j in X ;
hence  j >= min X by XXREAL_2:def_7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st b1 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds
j >= b1 ) & b2 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds
j >= b2 ) holds
b1 = b2
proof
let it1, it2 be Element of NAT ; ::_thesis: ( it1 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds
j >= it1 ) & it2 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds
j >= it2 ) implies it1 = it2 )
assume that
A3: it1 is_sufficiently_large_for C and
A4: for j being Element of NAT st j is_sufficiently_large_for C holds
j >= it1 and
A5: it2 is_sufficiently_large_for C and
A6: for j being Element of NAT st j is_sufficiently_large_for C holds
j >= it2 ; ::_thesis: it1 = it2
A7: it2 <= it1 by A3, A6;
 it1 <= it2 by A4, A5;
hence  it1 = it2 by A7, XXREAL_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines ApproxIndex JORDAN11:def_1_:_
 for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for b2 being Element of NAT holds
( b2 = ApproxIndex C iff ( b2 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds
j >= b2 ) ) );

theorem Th1: :: JORDAN11:1
for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds ApproxIndex C >= 1
proof
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ApproxIndex C >= 1
 ApproxIndex C is_sufficiently_large_for C by Def1;
hence  ApproxIndex C >= 1 by JORDAN1H:51; ::_thesis: verum
end;

definition
let C be being_simple_closed_curve Subset of (TOP-REAL 2);
func Y-InitStart C ->  Element of NAT  means :Def2: :: JORDAN11:def 2
( it < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= it ) );
existence
 ex b1 being Element of NAT st
( b1 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b1) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= b1 ) )
proof
set n = ApproxIndex C;
defpred S1[ Element of NAT ] means ( $1 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),$1) c= BDD C );
set X =  {  i where i is Element of NAT : S1[i]  }  ;
A1:  {  i where i is Element of NAT : S1[i]  }  is Subset of NAT from DOMAIN_1:sch_7();
 ApproxIndex C is_sufficiently_large_for C by Def1;
then consider j being Element of NAT  such that
A2: S1[j] by JORDAN1H:def_3;
 j in  {  i where i is Element of NAT : S1[i]  }  by A2;
then reconsider X =  {  i where i is Element of NAT : S1[i]  }  as non empty Subset of NAT by A1;
take  min X ; ::_thesis: ( min X < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(min X)) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= min X ) )
 min X in X by XXREAL_2:def_7;
then  ex i being Element of NAT st
( i = min X & S1[i] ) ;
hence  S1[ min X] ; ::_thesis: for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= min X
let i be Element of NAT ; ::_thesis: ( i < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),i) c= BDD C implies i >= min X )
assume  S1[i] ; ::_thesis: i >= min X
then  i in X ;
hence  i >= min X by XXREAL_2:def_7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st b1 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b1) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= b1 ) & b2 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b2) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= b2 ) holds
b1 = b2
proof
let it1, it2 be Element of NAT ; ::_thesis: ( it1 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it1) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= it1 ) & it2 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it2) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= it2 ) implies it1 = it2 )
assume that
A3: it1 < width (Gauge (C,(ApproxIndex C))) and
A4: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it1) c= BDD C and
A5: for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= it1 and
A6: it2 < width (Gauge (C,(ApproxIndex C))) and
A7: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it2) c= BDD C and
A8: for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= it2 ; ::_thesis: it1 = it2
A9: it2 <= it1 by A3, A4, A8;
 it1 <= it2 by A5, A6, A7;
hence  it1 = it2 by A9, XXREAL_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Y-InitStart JORDAN11:def_2_:_
 for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for b2 being Element of NAT holds
( b2 = Y-InitStart C iff ( b2 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b2) c= BDD C & ( for j being Element of NAT st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= b2 ) ) );

theorem Th2: :: JORDAN11:2
for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds Y-InitStart C > 1
proof
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: Y-InitStart C > 1
set m = ApproxIndex C;
A1: (X-SpanStart (C,(ApproxIndex C))) -' 1 <= len (Gauge (C,(ApproxIndex C))) by JORDAN1H:50;
assume A2: Y-InitStart C <= 1 ; ::_thesis: contradiction
percases ( Y-InitStart C = 0 or Y-InitStart C = 1 ) by A2, NAT_1:25;
supposeA3: Y-InitStart C = 0 ; ::_thesis: contradiction
A4: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),0) c= UBD C by A1, JORDAN1A:49;
 0 <= width (Gauge (C,(ApproxIndex C))) ;
then A5: not cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),0) is empty by A1, JORDAN1A:24;
 cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),0) c= BDD C by A3, Def2;
hence  contradiction by A5, A4, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
suppose Y-InitStart C = 1 ; ::_thesis: contradiction
then A6: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),1) c= BDD C by Def2;
set i1 = X-SpanStart (C,(ApproxIndex C));
A7: (X-SpanStart (C,(ApproxIndex C))) -' 1 <= X-SpanStart (C,(ApproxIndex C)) by NAT_D:44;
 X-SpanStart (C,(ApproxIndex C)) < len (Gauge (C,(ApproxIndex C))) by JORDAN1H:49;
then A8: (X-SpanStart (C,(ApproxIndex C))) -' 1 < len (Gauge (C,(ApproxIndex C))) by A7, XXREAL_0:2;
 BDD C c= C ` by JORDAN2C:25;
then A9: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),1) c= C ` by A6, XBOOLE_1:1;
 UBD C is_outside_component_of C by JORDAN2C:68;
then A10: UBD C is_a_component_of C ` by JORDAN2C:def_3;
A11: width (Gauge (C,(ApproxIndex C))) <> 0 by GOBOARD1:def_3;
then A12: 0 + 1 <= width (Gauge (C,(ApproxIndex C))) by NAT_1:14;
then A13: not cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),1) is empty by A1, JORDAN1A:24;
 1 <= (X-SpanStart (C,(ApproxIndex C))) -' 1 by JORDAN1H:50;
then  (cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),0)) /\ (cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(0 + 1))) = LSeg (((Gauge (C,(ApproxIndex C))) * (((X-SpanStart (C,(ApproxIndex C))) -' 1),(0 + 1))),((Gauge (C,(ApproxIndex C))) * ((((X-SpanStart (C,(ApproxIndex C))) -' 1) + 1),(0 + 1)))) by A11, A8, GOBOARD5:26;
then A14: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),0) meets cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(0 + 1)) by XBOOLE_0:def_7;
 cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),0) c= UBD C by A1, JORDAN1A:49;
then  cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),1) c= UBD C by A12, A8, A14, A10, A9, GOBOARD9:4, JORDAN1A:25;
hence  contradiction by A6, A13, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
end;
end;

theorem Th3: :: JORDAN11:3
for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds (Y-InitStart C) + 1 < width (Gauge (C,(ApproxIndex C)))
proof
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: (Y-InitStart C) + 1 < width (Gauge (C,(ApproxIndex C)))
set m = ApproxIndex C;
A1: (X-SpanStart (C,(ApproxIndex C))) -' 1 <= len (Gauge (C,(ApproxIndex C))) by JORDAN1H:50;
assume  (Y-InitStart C) + 1 >= width (Gauge (C,(ApproxIndex C))) ; ::_thesis: contradiction
then A2: ( (Y-InitStart C) + 1 > width (Gauge (C,(ApproxIndex C))) or (Y-InitStart C) + 1 = width (Gauge (C,(ApproxIndex C))) ) by XXREAL_0:1;
A3: ( Y-InitStart C < width (Gauge (C,(ApproxIndex C))) or Y-InitStart C = width (Gauge (C,(ApproxIndex C))) ) by Def2;
percases ( Y-InitStart C = width (Gauge (C,(ApproxIndex C))) or (Y-InitStart C) + 1 = width (Gauge (C,(ApproxIndex C))) ) by A2, A3, NAT_1:13;
suppose Y-InitStart C = width (Gauge (C,(ApproxIndex C))) ; ::_thesis: contradiction
hence  contradiction by Def2; ::_thesis: verum
end;
suppose (Y-InitStart C) + 1 = width (Gauge (C,(ApproxIndex C))) ; ::_thesis: contradiction
then  Y-InitStart C = (width (Gauge (C,(ApproxIndex C)))) -' 1 by NAT_D:34;
then A4: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),((width (Gauge (C,(ApproxIndex C)))) -' 1)) c= BDD C by Def2;
 BDD C c= C ` by JORDAN2C:25;
then A5: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),((width (Gauge (C,(ApproxIndex C)))) -' 1)) c= C ` by A4, XBOOLE_1:1;
A6: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(width (Gauge (C,(ApproxIndex C))))) c= UBD C by A1, JORDAN1A:50;
set i1 = X-SpanStart (C,(ApproxIndex C));
A7: (X-SpanStart (C,(ApproxIndex C))) -' 1 <= X-SpanStart (C,(ApproxIndex C)) by NAT_D:44;
 X-SpanStart (C,(ApproxIndex C)) < len (Gauge (C,(ApproxIndex C))) by JORDAN1H:49;
then A8: (X-SpanStart (C,(ApproxIndex C))) -' 1 < len (Gauge (C,(ApproxIndex C))) by A7, XXREAL_0:2;
 UBD C is_outside_component_of C by JORDAN2C:68;
then A9: UBD C is_a_component_of C ` by JORDAN2C:def_3;
 (width (Gauge (C,(ApproxIndex C)))) -' 1 <= width (Gauge (C,(ApproxIndex C))) by NAT_D:44;
then A10: not cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),((width (Gauge (C,(ApproxIndex C)))) -' 1)) is empty by A1, JORDAN1A:24;
A11: (width (Gauge (C,(ApproxIndex C)))) - 1 < width (Gauge (C,(ApproxIndex C))) by XREAL_1:146;
A12: 1 <= (X-SpanStart (C,(ApproxIndex C))) -' 1 by JORDAN1H:50;
A13: width (Gauge (C,(ApproxIndex C))) <> 0 by GOBOARD1:def_3;
then  ((width (Gauge (C,(ApproxIndex C)))) -' 1) + 1 = width (Gauge (C,(ApproxIndex C))) by NAT_1:14, XREAL_1:235;
then  (cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(width (Gauge (C,(ApproxIndex C)))))) /\ (cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),((width (Gauge (C,(ApproxIndex C)))) -' 1))) = LSeg (((Gauge (C,(ApproxIndex C))) * (((X-SpanStart (C,(ApproxIndex C))) -' 1),(width (Gauge (C,(ApproxIndex C)))))),((Gauge (C,(ApproxIndex C))) * ((((X-SpanStart (C,(ApproxIndex C))) -' 1) + 1),(width (Gauge (C,(ApproxIndex C))))))) by A8, A11, A12, GOBOARD5:26;
then A14: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(width (Gauge (C,(ApproxIndex C))))) meets cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),((width (Gauge (C,(ApproxIndex C)))) -' 1)) by XBOOLE_0:def_7;
 (width (Gauge (C,(ApproxIndex C)))) -' 1 < width (Gauge (C,(ApproxIndex C))) by A13, A11, NAT_1:14, XREAL_1:233;
then  cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),((width (Gauge (C,(ApproxIndex C)))) -' 1)) c= UBD C by A6, A8, A14, A9, A5, GOBOARD9:4, JORDAN1A:25;
hence  contradiction by A4, A10, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
end;
end;

definition
let C be being_simple_closed_curve Subset of (TOP-REAL 2);
let n be Element of NAT ;
assume  n is_sufficiently_large_for C ;
then A1: n >= ApproxIndex C by Def1;
set i1 = X-SpanStart (C,n);
func Y-SpanStart (C,n) ->  Element of NAT  means :Def3: :: JORDAN11:def 3
( it <= width (Gauge (C,n)) & ( for k being Element of NAT st it <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= it ) );
existence
 ex b1 being Element of NAT st
( b1 <= width (Gauge (C,n)) & ( for k being Element of NAT st b1 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b1 ) )
proof
set m = ApproxIndex C;
defpred S1[ Element of NAT ] means ( $1 <= width (Gauge (C,n)) & ( for k being Element of NAT st $1 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) );
set X =  {  i where i is Element of NAT : S1[i]  }  ;
set j0 = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2;
A2:  {  i where i is Element of NAT : S1[i]  }  is Subset of NAT from DOMAIN_1:sch_7();
A3: (Y-InitStart C) + 1 < width (Gauge (C,(ApproxIndex C))) by Th3;
then  (Y-InitStart C) + 1 < (2 |^ (ApproxIndex C)) + (2 + 1) by JORDAN1A:28;
then  (Y-InitStart C) + 1 < ((2 |^ (ApproxIndex C)) + 2) + 1 ;
then A4: Y-InitStart C < (2 |^ (ApproxIndex C)) + 2 by XREAL_1:6;
A5: 1 < Y-InitStart C by Th2;
then  1 + 1 <= Y-InitStart C by NAT_1:13;
then  (Y-InitStart C) -' 2 < 2 |^ (ApproxIndex C) by A4, NAT_D:54;
then  (2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) <= (2 |^ (n -' (ApproxIndex C))) * (2 |^ (ApproxIndex C)) by XREAL_1:64;
then  (2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) <= 2 |^ ((n -' (ApproxIndex C)) + (ApproxIndex C)) by NEWTON:8;
then A6: (2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) <= 2 |^ n by A1, XREAL_1:235;
A7: now__::_thesis:_for_j_being_Element_of_NAT_st_((2_|^_(n_-'_(ApproxIndex_C)))_*_((Y-InitStart_C)_-'_2))_+_2_<=_j_&_j_<=_((2_|^_(n_-'_(ApproxIndex_C)))_*_((Y-InitStart_C)_-'_2))_+_2_holds_
cell_((Gauge_(C,n)),((X-SpanStart_(C,n))_-'_1),j)_c=_BDD_C
 2 |^ ((ApproxIndex C) -' 1) <= 2 |^ (ApproxIndex C) by NAT_D:35, PREPOWER:93;
then A8: (2 |^ ((ApproxIndex C) -' 1)) + 2 <= (2 |^ (ApproxIndex C)) + 2 by XREAL_1:6;
len (Gauge (C,(ApproxIndex C))) = (2 |^ (ApproxIndex C)) + (2 + 1) by JORDAN8:def_1
.= ((2 |^ (ApproxIndex C)) + 2) + 1 ;
then A9: X-SpanStart (C,(ApproxIndex C)) < len (Gauge (C,(ApproxIndex C))) by A8, NAT_1:13;
A10: Y-InitStart C >= 1 + 1 by A5, NAT_1:13;
let j be Element of NAT ; ::_thesis: ( ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= j & j <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 implies cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C )
assume that
A11: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= j and
A12: j <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 ; ::_thesis: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C
A13: ApproxIndex C >= 1 by Th1;
 1 <= 2 |^ ((ApproxIndex C) -' 1) by PREPOWER:11;
then A14: 2 + 1 <= X-SpanStart (C,(ApproxIndex C)) by XREAL_1:6;
A15: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(Y-InitStart C)) c= BDD C by Def2;
 j = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A11, A12, XXREAL_0:1;
then A16: j = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 by A10, XREAL_1:233;
(n -' (ApproxIndex C)) + ((ApproxIndex C) -' 1) = (n -' (ApproxIndex C)) + ((ApproxIndex C) - 1) by Th1, XREAL_1:233
.= ((n -' (ApproxIndex C)) + (ApproxIndex C)) - 1
.= n - 1 by A1, XREAL_1:235
.= n -' 1 by A1, A13, XREAL_1:233, XXREAL_0:2 ;
then  X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 by NEWTON:8;
then  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(Y-InitStart C)) by A1, A3, A14, A9, A16, Th2, JORDAN1A:48;
hence  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C by A15, XBOOLE_1:1; ::_thesis: verum
end;
 2 |^ n <= (2 |^ n) + 1 by NAT_1:11;
then  (2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) <= (2 |^ n) + 1 by A6, XXREAL_0:2;
then  ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= ((2 |^ n) + 1) + 2 by XREAL_1:6;
then  ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= (2 |^ n) + (1 + 2) ;
then  ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= len (Gauge (C,n)) by JORDAN8:def_1;
then  ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= width (Gauge (C,n)) by JORDAN8:def_1;
then  ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 in  {  i where i is Element of NAT : S1[i]  }  by A7;
then reconsider X =  {  i where i is Element of NAT : S1[i]  }  as non empty Subset of NAT by A2;
take  min X ; ::_thesis: ( min X <= width (Gauge (C,n)) & ( for k being Element of NAT st min X <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= min X ) )
 min X in X by XXREAL_2:def_7;
then  ex j being Element of NAT st
( j = min X & S1[j] ) ;
hence  S1[ min X] ; ::_thesis: for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= min X
let j be Element of NAT ; ::_thesis: ( j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) implies j >= min X )
assume  S1[j] ; ::_thesis: j >= min X
then  j in X ;
hence  j >= min X by XXREAL_2:def_7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st b1 <= width (Gauge (C,n)) & ( for k being Element of NAT st b1 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b1 ) & b2 <= width (Gauge (C,n)) & ( for k being Element of NAT st b2 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b2 ) holds
b1 = b2
proof
let it1, it2 be Element of NAT ; ::_thesis: ( it1 <= width (Gauge (C,n)) & ( for k being Element of NAT st it1 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= it1 ) & it2 <= width (Gauge (C,n)) & ( for k being Element of NAT st it2 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= it2 ) implies it1 = it2 )
defpred S1[ Element of NAT ] means ( $1 <= width (Gauge (C,n)) & ( for i being Element of NAT st $1 <= i & i <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),i) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for i being Element of NAT st j <= i & i <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),i) c= BDD C ) holds
j >= $1 ) );
assume that
A17: S1[it1] and
A18: S1[it2] ; ::_thesis: it1 = it2
A19: it2 <= it1 by A17, A18;
 it1 <= it2 by A17, A18;
hence  it1 = it2 by A19, XXREAL_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Y-SpanStart JORDAN11:def_3_:_
 for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for n being Element of NAT st n is_sufficiently_large_for C holds
for b3 being Element of NAT holds
( b3 = Y-SpanStart (C,n) iff ( b3 <= width (Gauge (C,n)) & ( for k being Element of NAT st b3 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of NAT st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b3 ) ) );

theorem Th4: :: JORDAN11:4
for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2
proof
let n be Element of NAT ; ::_thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ( n is_sufficiently_large_for C implies X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 )
set m = ApproxIndex C;
A1: ApproxIndex C >= 1 by Th1;
assume  n is_sufficiently_large_for C ; ::_thesis: X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2
then A2: n >= ApproxIndex C by Def1;
(n -' (ApproxIndex C)) + ((ApproxIndex C) -' 1) = (n -' (ApproxIndex C)) + ((ApproxIndex C) - 1) by Th1, XREAL_1:233
.= ((n -' (ApproxIndex C)) + (ApproxIndex C)) - 1
.= n - 1 by A2, XREAL_1:235
.= n -' 1 by A2, A1, XREAL_1:233, XXREAL_0:2 ;
hence  X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 by NEWTON:8; ::_thesis: verum
end;

theorem Th5: :: JORDAN11:5
for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
Y-SpanStart (C,n) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2
proof
let n be Element of NAT ; ::_thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
Y-SpanStart (C,n) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ( n is_sufficiently_large_for C implies Y-SpanStart (C,n) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 )
set m = ApproxIndex C;
A1: X-SpanStart (C,(ApproxIndex C)) > 2 by JORDAN1H:49;
set j0 = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2;
set i1 = X-SpanStart (C,n);
assume A2: n is_sufficiently_large_for C ; ::_thesis: Y-SpanStart (C,n) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2
then A3: n >= ApproxIndex C by Def1;
A4: 1 < Y-InitStart C by Th2;
then  1 + 1 <= Y-InitStart C by NAT_1:13;
then A5: (Y-InitStart C) -' 2 = (Y-InitStart C) - 2 by XREAL_1:233;
A6: (Y-InitStart C) + 1 < width (Gauge (C,(ApproxIndex C))) by Th3;
A7: now__::_thesis:_for_j_being_Element_of_NAT_st_((2_|^_(n_-'_(ApproxIndex_C)))_*_((Y-InitStart_C)_-'_2))_+_2_<=_j_&_j_<=_((2_|^_(n_-'_(ApproxIndex_C)))_*_((Y-InitStart_C)_-'_2))_+_2_holds_
cell_((Gauge_(C,n)),((X-SpanStart_(C,n))_-'_1),j)_c=_BDD_C
 (ApproxIndex C) -' 1 <= ApproxIndex C by NAT_D:44;
then A8: 2 |^ ((ApproxIndex C) -' 1) <= 2 |^ (ApproxIndex C) by PREPOWER:93;
 len (Gauge (C,(ApproxIndex C))) = (2 |^ (ApproxIndex C)) + 3 by JORDAN8:def_1;
then A9: X-SpanStart (C,(ApproxIndex C)) < len (Gauge (C,(ApproxIndex C))) by A8, XREAL_1:8;
A10: 2 + 1 <= X-SpanStart (C,(ApproxIndex C)) by A1, NAT_1:13;
A11: X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 by A2, Th4;
let j be Element of NAT ; ::_thesis: ( ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= j & j <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 implies cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C )
assume that
A12: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= j and
A13: j <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 ; ::_thesis: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C
A14: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(Y-InitStart C)) c= BDD C by Def2;
 j = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A12, A13, XXREAL_0:1;
then  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(Y-InitStart C)) by A3, A6, A5, A10, A9, A11, Th2, JORDAN1A:48;
hence  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C by A14, XBOOLE_1:1; ::_thesis: verum
end;
 Y-InitStart C < (Y-InitStart C) + 1 by XREAL_1:29;
then  Y-InitStart C < width (Gauge (C,(ApproxIndex C))) by Th3, XXREAL_0:2;
then  ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= width (Gauge (C,n)) by A3, A4, A5, JORDAN1A:32;
hence  Y-SpanStart (C,n) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A2, A7, Def3; ::_thesis: verum
end;

theorem Th6: :: JORDAN11:6
for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) c= BDD C
proof
let n be Element of NAT ; ::_thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) c= BDD C
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ( n is_sufficiently_large_for C implies cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) c= BDD C )
assume A1: n is_sufficiently_large_for C ; ::_thesis: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) c= BDD C
then  Y-SpanStart (C,n) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by Th5;
hence  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) c= BDD C by A1, Def3; ::_thesis: verum
end;

theorem Th7: :: JORDAN11:7
for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
( 1 < Y-SpanStart (C,n) & Y-SpanStart (C,n) <= width (Gauge (C,n)) )
proof
let n be Element of NAT ; ::_thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
( 1 < Y-SpanStart (C,n) & Y-SpanStart (C,n) <= width (Gauge (C,n)) )
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ( n is_sufficiently_large_for C implies ( 1 < Y-SpanStart (C,n) & Y-SpanStart (C,n) <= width (Gauge (C,n)) ) )
assume A1: n is_sufficiently_large_for C ; ::_thesis: ( 1 < Y-SpanStart (C,n) & Y-SpanStart (C,n) <= width (Gauge (C,n)) )
thus  1 < Y-SpanStart (C,n) ::_thesis: Y-SpanStart (C,n) <= width (Gauge (C,n))
proof
A2: (X-SpanStart (C,n)) -' 1 <= len (Gauge (C,n)) by JORDAN1H:50;
assume A3: Y-SpanStart (C,n) <= 1 ; ::_thesis: contradiction
percases ( Y-SpanStart (C,n) = 0 or Y-SpanStart (C,n) = 1 ) by A3, NAT_1:25;
supposeA4: Y-SpanStart (C,n) = 0 ; ::_thesis: contradiction
A5: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A2, JORDAN1A:49;
 0 <= width (Gauge (C,n)) ;
then A6: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) is empty by A2, JORDAN1A:24;
 cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= BDD C by A1, A4, Th6;
hence  contradiction by A6, A5, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
suppose Y-SpanStart (C,n) = 1 ; ::_thesis: contradiction
then A7: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= BDD C by A1, Th6;
set i1 = X-SpanStart (C,n);
A8: (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) by NAT_D:44;
 X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49;
then A9: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by A8, XXREAL_0:2;
 BDD C c= C ` by JORDAN2C:25;
then A10: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= C ` by A7, XBOOLE_1:1;
 UBD C is_outside_component_of C by JORDAN2C:68;
then A11: UBD C is_a_component_of C ` by JORDAN2C:def_3;
A12: width (Gauge (C,n)) <> 0 by GOBOARD1:def_3;
then A13: 0 + 1 <= width (Gauge (C,n)) by NAT_1:14;
then A14: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) is empty by A2, JORDAN1A:24;
 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50;
then  (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0)) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1))) = LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(0 + 1))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(0 + 1)))) by A12, A9, GOBOARD5:26;
then A15: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) meets cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1)) by XBOOLE_0:def_7;
 cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A2, JORDAN1A:49;
then  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= UBD C by A13, A9, A15, A11, A10, GOBOARD9:4, JORDAN1A:25;
hence  contradiction by A7, A14, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
end;
end;
thus  Y-SpanStart (C,n) <= width (Gauge (C,n)) by A1, Def3; ::_thesis: verum
end;

theorem :: JORDAN11:8
for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
[(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n))
proof
let n be Element of NAT ; ::_thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
[(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n))
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ( n is_sufficiently_large_for C implies [(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) )
A1: X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49;
 1 + 1 < X-SpanStart (C,n) by JORDAN1H:49;
then A2: 1 < X-SpanStart (C,n) by NAT_1:13;
assume A3: n is_sufficiently_large_for C ; ::_thesis: [(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n))
then A4: Y-SpanStart (C,n) <= width (Gauge (C,n)) by Th7;
 1 < Y-SpanStart (C,n) by A3, Th7;
hence  [(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A2, A1, A4, MATRIX_1:36; ::_thesis: verum
end;

theorem :: JORDAN11:9
for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
[((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n))
proof
let n be Element of NAT ; ::_thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
[((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n))
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ( n is_sufficiently_large_for C implies [((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) )
A1: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50;
A2: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by JORDAN1H:50;
assume A3: n is_sufficiently_large_for C ; ::_thesis: [((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n))
then A4: Y-SpanStart (C,n) <= width (Gauge (C,n)) by Th7;
 1 < Y-SpanStart (C,n) by A3, Th7;
hence  [((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A1, A2, A4, MATRIX_1:36; ::_thesis: verum
end;

theorem :: JORDAN11:10
for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) -' 1)) meets C
proof
let n be Element of NAT ; ::_thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) -' 1)) meets C
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ( n is_sufficiently_large_for C implies cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) -' 1)) meets C )
set i1 = X-SpanStart (C,n);
A1: (Y-SpanStart (C,n)) - 1 < Y-SpanStart (C,n) by XREAL_1:146;
assume A2: n is_sufficiently_large_for C ; ::_thesis: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) -' 1)) meets C
then A3: 1 < Y-SpanStart (C,n) by Th7;
assume A4: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) -' 1)) misses C ; ::_thesis: contradiction
A5: for k being Element of NAT st (Y-SpanStart (C,n)) -' 1 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C
proof
let k be Element of NAT ; ::_thesis: ( (Y-SpanStart (C,n)) -' 1 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 implies cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C )
assume that
A6: (Y-SpanStart (C,n)) -' 1 <= k and
A7: k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 ; ::_thesis: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C
percases ( (Y-SpanStart (C,n)) -' 1 = k or (Y-SpanStart (C,n)) -' 1 < k ) by A6, XXREAL_0:1;
supposeA8: (Y-SpanStart (C,n)) -' 1 = k ; ::_thesis: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C
 1 < Y-SpanStart (C,n) by A2, Th7;
then A9: k + 1 = Y-SpanStart (C,n) by A8, XREAL_1:235;
A10: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= C ` by A4, A8, SUBSET_1:23;
A11: k < k + 1 by XREAL_1:29;
 Y-SpanStart (C,n) <= width (Gauge (C,n)) by A2, Th7;
then A12: k < width (Gauge (C,n)) by A9, A11, XXREAL_0:2;
set W =  {  B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C  }  ;
A13: (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) by NAT_D:44;
 X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49;
then A14: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by A13, XXREAL_0:2;
A15: BDD C = union  {  B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C  }  by JORDAN2C:def_4;
 1 + 1 < X-SpanStart (C,n) by JORDAN1H:49;
then  1 <= (X-SpanStart (C,n)) - 1 by XREAL_1:19;
then  1 <= (X-SpanStart (C,n)) -' 1 by NAT_D:39;
then  (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(k + 1))) = LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(k + 1))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(k + 1)))) by A14, A12, GOBOARD5:26;
then  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) meets cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(k + 1)) by XBOOLE_0:def_7;
then  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) meets BDD C by A2, A9, Th6, XBOOLE_1:63;
then consider e being set  such that
A16: e in  {  B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C  }  and
A17: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) meets e by A15, ZFMISC_1:80;
consider B being Subset of (TOP-REAL 2) such that
A18: e = B and
A19: B is_inside_component_of C by A16;
A20: B c= BDD C by A15, A16, A18, ZFMISC_1:74;
 B is_a_component_of C ` by A19, JORDAN2C:def_2;
then  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= B by A10, A14, A12, A17, A18, GOBOARD9:4, JORDAN1A:25;
hence  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C by A20, XBOOLE_1:1; ::_thesis: verum
end;
suppose (Y-SpanStart (C,n)) -' 1 < k ; ::_thesis: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C
then  Y-SpanStart (C,n) < k + 1 by NAT_D:55;
then  Y-SpanStart (C,n) <= k by NAT_1:13;
hence  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C by A2, A7, Def3; ::_thesis: verum
end;
end;
end;
 Y-SpanStart (C,n) <= width (Gauge (C,n)) by A2, Def3;
then  (Y-SpanStart (C,n)) -' 1 <= width (Gauge (C,n)) by NAT_D:44;
then  (Y-SpanStart (C,n)) -' 1 >= Y-SpanStart (C,n) by A2, A5, Def3;
hence  contradiction by A3, A1, XREAL_1:233; ::_thesis: verum
end;

theorem :: JORDAN11:11
for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) misses C
proof
let n be Element of NAT ; ::_thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) misses C
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ( n is_sufficiently_large_for C implies cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) misses C )
assume  n is_sufficiently_large_for C ; ::_thesis: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) misses C
then  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) c= BDD C by Th6;
hence  cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) misses C by JORDAN1A:7, XBOOLE_1:63; ::_thesis: verum
end;

begin


theorem Th12: :: JORDAN11:12
for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for D being Simple_closed_curve holds UBD C meets UBD D
proof
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: for D being Simple_closed_curve holds UBD C meets UBD D
let D be Simple_closed_curve; ::_thesis: UBD C meets UBD D
reconsider A = C as bounded Subset of (Euclid 2) by JORDAN2C:11;
consider r1 being Real, x1 being Point of (Euclid 2) such that
 0 < r1 and
A1: A c= Ball (x1,r1) by METRIC_6:def_3;
reconsider B = D as bounded Subset of (Euclid 2) by JORDAN2C:11;
consider r2 being Real, x2 being Point of (Euclid 2) such that
 0 < r2 and
A2: B c= Ball (x2,r2) by METRIC_6:def_3;
reconsider C9 = (Ball (x1,r1)) ` , D9 = (Ball (x2,r2)) ` as connected Subset of (TOP-REAL 2) by JORDAN1K:37;
consider x3 being Point of (Euclid 2), r3 being Real such that
A3: (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x3,r3) by WEIERSTR:1;
A4: now__::_thesis:_not_D9_is_bounded
assume  D9 is bounded ; ::_thesis: contradiction
then  D9 is bounded Subset of (Euclid 2) by JORDAN2C:11;
hence  contradiction by JORDAN1K:8; ::_thesis: verum
end;
A5: now__::_thesis:_not_C9_is_bounded
assume  C9 is bounded ; ::_thesis: contradiction
then  C9 is bounded Subset of (Euclid 2) by JORDAN2C:11;
hence  contradiction by JORDAN1K:8; ::_thesis: verum
end;
 (Ball (x3,r3)) ` c= ((Ball (x1,r1)) \/ (Ball (x2,r2))) ` by A3, SUBSET_1:12;
then A6: (Ball (x3,r3)) ` c= ((Ball (x1,r1)) `) /\ ((Ball (x2,r2)) `) by XBOOLE_1:53;
then A7: (Ball (x3,r3)) ` c= (Ball (x1,r1)) ` by XBOOLE_1:18;
A8: (Ball (x3,r3)) ` c= (Ball (x2,r2)) ` by A6, XBOOLE_1:18;
 (Ball (x2,r2)) ` c= B ` by A2, SUBSET_1:12;
then  (Ball (x2,r2)) ` misses B by SUBSET_1:23;
then  D9 c= UBD D by A4, JORDAN2C:125;
then A9: (Ball (x3,r3)) ` c= UBD D by A8, XBOOLE_1:1;
 (Ball (x1,r1)) ` c= A ` by A1, SUBSET_1:12;
then  (Ball (x1,r1)) ` misses A by SUBSET_1:23;
then  C9 c= UBD C by A5, JORDAN2C:125;
then A10: (Ball (x3,r3)) ` c= UBD C by A7, XBOOLE_1:1;
 (Ball (x3,r3)) ` <> {} (Euclid 2) by JORDAN1K:8;
hence  UBD C meets UBD D by A10, A9, XBOOLE_1:68; ::_thesis: verum
end;

theorem Th13: :: JORDAN11:13
for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for q, p being Point of (TOP-REAL 2) st q in UBD C & p in BDD C holds
dist (q,C) < dist (q,p)
proof
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: for q, p being Point of (TOP-REAL 2) st q in UBD C & p in BDD C holds
dist (q,C) < dist (q,p)
let q, p be Point of (TOP-REAL 2); ::_thesis: ( q in UBD C & p in BDD C implies dist (q,C) < dist (q,p) )
assume that
A1: q in UBD C and
A2: p in BDD C and
A3: dist (q,C) >= dist (q,p) ; ::_thesis: contradiction
A4: UBD C is_a_component_of C ` by JORDAN2C:124;
now__::_thesis:_not_LSeg_(p,q)_meets_C
assume  LSeg (p,q) meets C ; ::_thesis: contradiction
then consider x being set  such that
A5: x in LSeg (p,q) and
A6: x in C by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A5;
A7: dist (q,C) <= dist (q,x) by A6, JORDAN1K:50;
 C misses BDD C by JORDAN1A:7;
then  x <> p by A2, A6, XBOOLE_0:3;
hence  contradiction by A3, A5, A7, JORDAN1K:30, XXREAL_0:2; ::_thesis: verum
end;
then A8: LSeg (p,q) c= C ` by SUBSET_1:23;
 q in LSeg (p,q) by RLTOPSP1:68;
then A9: LSeg (p,q) meets UBD C by A1, XBOOLE_0:3;
A10: BDD C = union  {  B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C  }  by JORDAN2C:def_4;
then consider X being set  such that
A11: p in X and
A12: X in  {  B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C  }  by A2, TARSKI:def_4;
consider B being Subset of (TOP-REAL 2) such that
A13: X = B and
A14: B is_inside_component_of C by A12;
 B c= BDD C by A10, A12, A13, ZFMISC_1:74;
then A15: B misses UBD C by JORDAN2C:24, XBOOLE_1:63;
 p in LSeg (p,q) by RLTOPSP1:68;
then A16: LSeg (p,q) meets B by A11, A13, XBOOLE_0:3;
 B is_a_component_of C ` by A14, JORDAN2C:def_2;
then  UBD C = B by A8, A4, A9, A16, JORDAN9:1;
hence  contradiction by A15, XBOOLE_1:66; ::_thesis: verum
end;

theorem Th14: :: JORDAN11:14
for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st not p in BDD C holds
dist (p,C) <= dist (p,(BDD C))
proof
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st not p in BDD C holds
dist (p,C) <= dist (p,(BDD C))
let p be Point of (TOP-REAL 2); ::_thesis: ( not p in BDD C implies dist (p,C) <= dist (p,(BDD C)) )
percases ( p in C or not p in C ) ;
suppose p in C ; ::_thesis: ( not p in BDD C implies dist (p,C) <= dist (p,(BDD C)) )
then  dist (p,C) = 0 by JORDAN1K:45;
hence  ( not p in BDD C implies dist (p,C) <= dist (p,(BDD C)) ) by JORDAN1K:44; ::_thesis: verum
end;
supposeA1: not p in C ; ::_thesis: ( not p in BDD C implies dist (p,C) <= dist (p,(BDD C)) )
assume that
A2: not p in BDD C and
A3: dist (p,C) > dist (p,(BDD C)) ; ::_thesis: contradiction
A4: ex q being Point of (TOP-REAL 2) st
( q in BDD C & dist (p,q) < dist (p,C) ) by A3, JORDAN1K:48;
 p in C ` by A1, SUBSET_1:29;
then  p in (BDD C) \/ (UBD C) by JORDAN2C:27;
then  p in UBD C by A2, XBOOLE_0:def_3;
hence  contradiction by A4, Th13; ::_thesis: verum
end;
end;
end;

theorem Th15: :: JORDAN11:15
for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for D being Simple_closed_curve holds
( not C c= BDD D or not D c= BDD C )
proof
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: for D being Simple_closed_curve holds
( not C c= BDD D or not D c= BDD C )
let D be Simple_closed_curve; ::_thesis: ( not C c= BDD D or not D c= BDD C )
assume that
A1: C c= BDD D and
A2: D c= BDD C ; ::_thesis: contradiction
 UBD C meets UBD D by Th12;
then consider e being set  such that
A3: e in UBD C and
A4: e in UBD D by XBOOLE_0:3;
reconsider p = e as Point of (TOP-REAL 2) by A3;
 UBD D misses BDD D by JORDAN2C:24;
then A5: not p in BDD D by A4, XBOOLE_0:3;
 UBD C misses BDD C by JORDAN2C:24;
then A6: not p in BDD C by A3, XBOOLE_0:3;
then  dist (p,C) <= dist (p,(BDD C)) by Th14;
then  dist (p,(BDD D)) < dist (p,(BDD C)) by A1, A5, JORDAN1K:51, XXREAL_0:2;
then  dist (p,(BDD D)) < dist (p,D) by A2, A6, JORDAN1K:51, XXREAL_0:2;
hence  contradiction by A5, Th14; ::_thesis: verum
end;

theorem Th16: :: JORDAN11:16
for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for D being Simple_closed_curve st C c= BDD D holds
D c= UBD C
proof
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: for D being Simple_closed_curve st C c= BDD D holds
D c= UBD C
let D be Simple_closed_curve; ::_thesis: ( C c= BDD D implies D c= UBD C )
assume A1: C c= BDD D ; ::_thesis: D c= UBD C
assume A2: not D c= UBD C ; ::_thesis: contradiction
 C misses D by A1, JORDAN1A:7, XBOOLE_1:63;
then  D c= BDD C by A2, JORDAN1K:19;
hence  contradiction by A1, Th15; ::_thesis: verum
end;

theorem :: JORDAN11:17
for n being Element of NAT
for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds L~ (Cage (C,n)) c= UBD C
proof
let n be Element of NAT ; ::_thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds L~ (Cage (C,n)) c= UBD C
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: L~ (Cage (C,n)) c= UBD C
 C c= BDD (L~ (Cage (C,n))) by JORDAN10:12;
hence  L~ (Cage (C,n)) c= UBD C by Th16; ::_thesis: verum
end;