let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis:
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: X-SpanStart C,1 = Center (Gauge C,1) by JORDAN1B:17;
then X-SpanStart C,1 = ((len (Gauge C,1)) div 2) + 1 by JORDAN1A:def 1;
then A2: 1 <= X-SpanStart C,1 by NAT_1:11;
len (Gauge C,1) >= 4 by JORDAN8:13;
then A3: 1 < len (Gauge C,1) by XXREAL_0:2;
then A4: ((Gauge C,1) * (X-SpanStart C,1),1) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, JORDAN1A:59;
then A5: (Gauge C,1) * (X-SpanStart C,1),1 in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN1A:17;
A6: ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, A3, JORDAN1A:59;
then (Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1)) in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN1A:17;
then A7: 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 A5, JORDAN1A:23;
A8: len (Gauge C,1) = width (Gauge C,1) by JORDAN8:def 1;
0 < len (Gauge C,1) by JORDAN8:13;
then (len (Gauge C,1)) div 2 < len (Gauge C,1) by INT_1:83;
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 A1, JORDAN1A:def 1;
then A9: ((Gauge C,1) * (X-SpanStart C,1),1) `2 < ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))) `2 by A2, A3, A8, GOBOARD5:5;
A10: ( proj2 . ((Gauge C,1) * (X-SpanStart C,1),1) = ((Gauge C,1) * (X-SpanStart C,1),1) `2 & 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 29;
deffunc H₁( 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
A11: for i being Element of NAT holds Es . i = H₁(i) from FUNCT_2:sch 4();
deffunc H₂( 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
A12: for i being Element of NAT holds E . i = H₂(i) from FUNCT_2:sch 4();
deffunc H₃( 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
A13: for i being Element of NAT holds Fs . i = H₃(i) from FUNCT_2:sch 4();
deffunc H₄( 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
A14: for i being Element of NAT holds F . i = H₄(i) from FUNCT_2:sch 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);
A15: 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:
set p = E . i;
A16: X-SpanStart C,(i + 1) = Center (Gauge C,(i + 1)) by JORDAN1B:17;
then A17: 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:34;
i + 1 >= 1 by NAT_1:11;
then A18: 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 A1, A16, A17, JORDAN1A:65, XBOOLE_1:63;
E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A12;
then A19: ( (E . i) `1 = ((W-bound C) + (E-bound C)) / 2 & (E . i) `2 = Es . i ) by EUCLID:56;
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) by PSCOMP_1:64;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:24;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A20: (dom proj2 ) /\ DD = DD by XBOOLE_1:28;
DD <> {} by A18, XBOOLE_0:def 7;
then dom proj2 meets DD by A20, XBOOLE_0:def 7;
then A21: D <> {} by RELAT_1:151;
Es . i = inf D by A11;
then Es . i in D by A21, RCOMP_1:32;
then consider dd being Point of (TOP-REAL 2) such that
A22: dd in DD and
A23: Es . i = proj2 . dd by FUNCT_2:116;
A24: dd in Upper_Arc (L~ (Cage C,(i + 1))) by A22, XBOOLE_0:def 4;
dd in LSeg ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))),((Gauge C,1) * (X-SpanStart C,1),1) by A22, XBOOLE_0:def 4;
then A25: dd `1 = (E . i) `1 by A7, A19, JORDAN6:34;
dd `2 = (E . i) `2 by A19, A23, PSCOMP_1:def 29;
hence E . i in Upper_Arc (L~ (Cage C,(i + 1))) by A24, A25, TOPREAL3:11; :: thesis:

end;

A26: 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:
set p = F . i;
A27: X-SpanStart C,(i + 1) = Center (Gauge C,(i + 1)) by JORDAN1B:17;
A28: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A12;
then A29: (E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
(E . i) `2 = Es . i by A28, EUCLID:56
.= inf (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 A11 ;
then consider j being Element of NAT such that
A30: 1 <= j and
A31: j <= width (Gauge C,(i + 1)) and
A32: E . i = (Gauge C,(i + 1)) * (X-SpanStart C,(i + 1)),j by A1, A8, A27, A29, JORDAN1F:13;
E . i in Upper_Arc (L~ (Cage C,(i + 1))) by A15;
then A33: LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . i) meets Lower_Arc (L~ (Cage C,(i + 1))) by A1, A27, A30, A31, A32, JORDAN1J:62;
F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A14;
then A34: ( (F . i) `1 = ((W-bound C) + (E-bound C)) / 2 & (F . i) `2 = Fs . i ) by EUCLID:56;
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) by PSCOMP_1:64;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:24;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A35: (dom proj2 ) /\ DD = DD by XBOOLE_1:28;
DD <> {} by A33, XBOOLE_0:def 7;
then dom proj2 meets DD by A35, XBOOLE_0:def 7;
then A36: D <> {} by RELAT_1:151;
Fs . i = sup D by A13;
then Fs . i in D by A36, RCOMP_1:32;
then consider dd being Point of (TOP-REAL 2) such that
A37: dd in DD and
A38: Fs . i = proj2 . dd by FUNCT_2:116;
A39: dd in Lower_Arc (L~ (Cage C,(i + 1))) by A37, XBOOLE_0:def 4;
A40: dd in LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) by A37, XBOOLE_0:def 4;
E . i in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A29, JORDAN1A:17;
then LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) c= Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A5, JORDAN1A:23;
then A41: dd `1 = (F . i) `1 by A34, A40, JORDAN6:34;
dd `2 = (F . i) `2 by A34, A38, PSCOMP_1:def 29;
hence F . i in Lower_Arc (L~ (Cage C,(i + 1))) by A39, A41, TOPREAL3:11; :: thesis:

end;

A42: 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 A9, A10, SPRECT_1:61;
deffunc H₅( Element of NAT ) -> Element of bool REAL = proj2 .: (LSeg (E . $1),(F . $1));
consider S being Function of NAT ,(bool REAL ) such that
A43: for i being Element of NAT holds S . i = H₅(i) from FUNCT_2:sch 4();
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);
( (LSeg ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))),((Gauge C,1) * (X-SpanStart C,1),1)) /\ (Upper_Arc C) is compact & (LSeg ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))),((Gauge C,1) * (X-SpanStart C,1),1)) /\ (Lower_Arc C) is compact ) by COMPTS_1:20;
then 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:24;
A44: A misses B

proof

assume A meets B ; :: thesis:
then consider z being set such that
A45: z in A and
A46: z in B by XBOOLE_0:3;
reconsider z = z as Real by A45;
consider p being Point of (TOP-REAL 2) such that
A47: 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
A48: z = proj2 . p by A45, FUNCT_2:116;
consider q being Point of (TOP-REAL 2) such that
A49: 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
A50: z = proj2 . q by A46, FUNCT_2:116;
A51: q in LSeg ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))),((Gauge C,1) * (X-SpanStart C,1),1) by A49, XBOOLE_0:def 4;
A52: p in LSeg ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))),((Gauge C,1) * (X-SpanStart C,1),1) by A47, XBOOLE_0:def 4;
then A53: p `1 = ((W-bound C) + (E-bound C)) / 2 by A7, JORDAN6:34
.= q `1 by A7, A51, JORDAN6:34 ;
p `2 = proj2 . q by A48, A50, PSCOMP_1:def 29
.= q `2 by PSCOMP_1:def 29 ;
then A54: p = q by A53, TOPREAL3:11;
A55: p in Upper_Arc C by A47, XBOOLE_0:def 4;
q in Lower_Arc C by A49, XBOOLE_0:def 4;
then p in (Upper_Arc C) /\ (Lower_Arc C) by A54, A55, XBOOLE_0:def 4;
then A56: p in {(W-min C),(E-max C)} by JORDAN6:65;

per cases by A56, TARSKI:def 2;

suppose p = W-min C ; :: thesis:

then A57: (W-min C) `1 = ((W-bound C) + (E-bound C)) / 2 by A7, A52, JORDAN6:34;
(W-min C) `1 = W-bound C by EUCLID:56;
hence contradiction by A57, SPRECT_1:33; :: thesis:

end;

suppose p = E-max C ; :: thesis:

then A58: (E-max C) `1 = ((W-bound C) + (E-bound C)) / 2 by A7, A52, JORDAN6:34;
(E-max C) `1 = E-bound C by EUCLID:56;
hence contradiction by A58, SPRECT_1:33; :: thesis:

end;

A59: A c= [.(proj2 . ((Gauge C,1) * (X-SpanStart C,1),1)),(proj2 . ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1)))).] by A42, RELAT_1:156, XBOOLE_1:17;
A60: B c= [.(proj2 . ((Gauge C,1) * (X-SpanStart C,1),1)),(proj2 . ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1)))).] by A42, RELAT_1:156, XBOOLE_1:17;
for i being Element of NAT holds
( S . i is connected & S . i meets A & S . i meets B )

proof

let i be Element of NAT ; :: thesis:
A61: S . i = proj2 .: (LSeg (E . i),(F . i)) by A43;
hence S . i is connected by JCT_MISC:15; :: thesis:
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) by PSCOMP_1:64;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:24;
A62: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A12;
then A63: (E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A64: X-SpanStart C,(i + 1) = Center (Gauge C,(i + 1)) by JORDAN1B:17;
A65: F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A14;
then A66: (F . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A67: 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:34;
1 <= i + 1 by NAT_1:11;
then A68: 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 A1, A67, JORDAN1A:65, XBOOLE_1:63;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A69: (dom proj2 ) /\ DD = DD by XBOOLE_1:28;
DD <> {} by A68, XBOOLE_0:def 7;
then dom proj2 meets DD by A69, XBOOLE_0:def 7;
then A70: D <> {} by RELAT_1:151;
Es . i = inf D by A11;
then Es . i in D by A70, RCOMP_1:32;
then consider dd being Point of (TOP-REAL 2) such that
A71: dd in DD and
A72: Es . i = proj2 . dd by FUNCT_2:116;
A73: dd in LSeg ((Gauge C,1) * (X-SpanStart C,1),1),((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))) by A71, XBOOLE_0:def 4;
then A74: dd `1 = (E . i) `1 by A7, A63, JORDAN6:34;
A75: (E . i) `2 = Es . i by A62, EUCLID:56
.= dd `2 by A72, PSCOMP_1:def 29 ;
then A76: E . i in LSeg ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))),((Gauge C,1) * (X-SpanStart C,1),1) by A73, A74, TOPREAL3:11;
(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:69;
then A77: 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 A76, TOPREAL1:12;
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) by PSCOMP_1:64;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:24;
(E . i) `2 = Es . i by A62, EUCLID:56
.= inf (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 A11 ;
then consider j being Element of NAT such that
A78: 1 <= j and
A79: j <= width (Gauge C,(i + 1)) and
A80: E . i = (Gauge C,(i + 1)) * (X-SpanStart C,(i + 1)),j by A1, A8, A63, A64, JORDAN1F:13;
A81: E . i in Upper_Arc (L~ (Cage C,(i + 1))) by A15;
then A82: LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . i) meets Lower_Arc (L~ (Cage C,(i + 1))) by A1, A64, A78, A79, A80, JORDAN1J:62;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A83: (dom proj2 ) /\ DD = DD by XBOOLE_1:28;
DD <> {} by A82, XBOOLE_0:def 7;
then dom proj2 meets DD by A83, XBOOLE_0:def 7;
then A84: D <> {} by RELAT_1:151;
Fs . i = sup D by A13;
then Fs . i in D by A84, RCOMP_1:32;
then consider dd being Point of (TOP-REAL 2) such that
A85: dd in DD and
A86: Fs . i = proj2 . dd by FUNCT_2:116;
A87: dd in LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) by A85, XBOOLE_0:def 4;
E . i in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A63, JORDAN1A:17;
then LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) c= Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A5, JORDAN1A:23;
then A88: dd `1 = (F . i) `1 by A66, A87, JORDAN6:34;
(F . i) `2 = Fs . i by A65, EUCLID:56
.= dd `2 by A86, PSCOMP_1:def 29 ;
then A89: F . i in LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) by A87, A88, TOPREAL3:11;
then A90: 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 A76, A77, TOPREAL1:12;
E . i in LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) by RLTOPSP1:69;
then A91: LSeg (E . i),(F . i) c= LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) by A89, TOPREAL1:12;
(E . i) `2 = Es . i by A62, EUCLID:56
.= inf (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 A11 ;
then consider j being Element of NAT such that
A92: 1 <= j and
A93: j <= width (Gauge C,(i + 1)) and
A94: E . i = (Gauge C,(i + 1)) * (X-SpanStart C,(i + 1)),j by A1, A8, A63, A64, JORDAN1F:13;
A95: (F . i) `2 = Fs . i by A65, EUCLID:56
.= sup (proj2 .: ((LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . i)) /\ (Lower_Arc (L~ (Cage C,(i + 1)))))) by A13 ;
then consider k being Element of NAT such that
A96: 1 <= k and
A97: k <= width (Gauge C,(i + 1)) and
A98: F . i = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),k by A1, A64, A66, A81, A92, A93, A94, JORDAN1I:30;
A99: F . i in Lower_Arc (L~ (Cage C,(i + 1))) by A26;
A100: 1 <= Center (Gauge C,(i + 1)) by JORDAN1B:12;
A101: Center (Gauge C,(i + 1)) <= len (Gauge C,(i + 1)) by JORDAN1B:14;
for p being real number st p in D holds
p <= (E . i) `2

proof

let p be real number ; :: thesis:
assume p in D ; :: thesis:
then consider x being set such that
x in dom proj2 and
A102: x in DD and
A103: p = proj2 . x by FUNCT_1:def 12;
reconsider x = x as Point of (TOP-REAL 2) by A102;
A104: ((Gauge C,1) * (X-SpanStart C,1),1) `2 <= (E . i) `2 by A9, A73, A75, TOPREAL1:10;
x in LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . i) by A102, XBOOLE_0:def 4;
then x `2 <= (E . i) `2 by A104, TOPREAL1:10;
hence p <= (E . i) `2 by A103, PSCOMP_1:def 29; :: thesis:

end;

then A105: sup D <= (E . i) `2 by A84, SEQ_4:62;
then A106: k <= j by A64, A92, A94, A95, A97, A98, A100, A101, GOBOARD5:5;
A107: for x being set st x in (LSeg (E . i),(F . i)) /\ (Upper_Arc (L~ (Cage C,(i + 1)))) holds
x = E . i

proof

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) by PSCOMP_1:64;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:24;
let x be set ; :: thesis:
assume A108: x in (LSeg (E . i),(F . i)) /\ (Upper_Arc (L~ (Cage C,(i + 1)))) ; :: thesis:
then reconsider p = x as Point of (TOP-REAL 2) ;
A109: p in LSeg (E . i),(F . i) by A108, XBOOLE_0:def 4;
then A110: p `1 = (E . i) `1 by A63, A66, GOBOARD7:5;
A111: p `2 <= (E . i) `2 by A95, A105, A109, TOPREAL1:10;
E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A12;
then A112: (E . i) `2 = Es . i by EUCLID:56
.= inf D by A11 ;
D is bounded by RCOMP_1:28;
then A113: D is bounded_below ;
p in Upper_Arc (L~ (Cage C,(i + 1))) by A108, XBOOLE_0:def 4;
then p in DD by A90, A109, XBOOLE_0:def 4;
then proj2 . p in D by FUNCT_2:43;
then p `2 in D by PSCOMP_1:def 29;
then (E . i) `2 <= p `2 by A112, A113, SEQ_4:def 5;
then p `2 = (E . i) `2 by A111, XXREAL_0:1;
hence x = E . i by A110, TOPREAL3:11; :: thesis:

end;

A114: for x being set st x in (LSeg (E . i),(F . i)) /\ (Lower_Arc (L~ (Cage C,(i + 1)))) holds
x = F . i

proof

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) by PSCOMP_1:64;
reconsider E0 = proj2 .: EE as compact Subset of REAL by JCT_MISC:24;
let x be set ; :: thesis:
assume A115: x in (LSeg (E . i),(F . i)) /\ (Lower_Arc (L~ (Cage C,(i + 1)))) ; :: thesis:
then reconsider p = x as Point of (TOP-REAL 2) ;
A116: p in LSeg (E . i),(F . i) by A115, XBOOLE_0:def 4;
then A117: p `1 = (F . i) `1 by A63, A66, GOBOARD7:5;
A118: p `2 >= (F . i) `2 by A95, A105, A116, TOPREAL1:10;
F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A14;
then A119: (F . i) `2 = Fs . i by EUCLID:56
.= sup E0 by A13 ;
E0 is bounded by RCOMP_1:28;
then A120: E0 is bounded_above ;
p in Lower_Arc (L~ (Cage C,(i + 1))) by A115, XBOOLE_0:def 4;
then p in EE by A91, A116, XBOOLE_0:def 4;
then proj2 . p in E0 by FUNCT_2:43;
then p `2 in E0 by PSCOMP_1:def 29;
then (F . i) `2 >= p `2 by A119, A120, SEQ_4:def 4;
then p `2 = (F . i) `2 by A118, XXREAL_0:1;
hence x = F . i by A117, TOPREAL3:11; :: thesis:

end;

A121: ( (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) & (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:69;
A122: (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:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
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:
then x = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j by A64, A94, A98, A107;
hence x in {((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j)} by TARSKI:def 1; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j)} ; :: thesis:
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 A64, A81, A94, A121, XBOOLE_0:def 4; :: thesis:

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
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:
then x = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),k by A64, A94, A98, A114;
hence x in {((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),k)} by TARSKI:def 1; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),k)} ; :: thesis:
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 A98, A99, A121, XBOOLE_0:def 4; :: thesis:

end;

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 A64, A90, A93, A94, A96, A98, A106, A122, JORDAN1J:64, XBOOLE_1:77;
hence S . i meets A by A61, JORDAN1A:24; :: thesis:
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 A64, A90, A93, A94, A96, A98, A106, A122, A123, JORDAN1J:63, XBOOLE_1:77;
hence S . i meets B by A61, JORDAN1A:24; :: thesis:

end;

then consider r being real number such that
A124: r in [.(proj2 . ((Gauge C,1) * (X-SpanStart C,1),1)),(proj2 . ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1)))).] and
A125: not r in A \/ B and
A126: for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) by A44, A59, A60, JCT_MISC:21;
reconsider r = r as Real by XREAL_0:def 1;
set p = |[(((W-bound C) + (E-bound C)) / 2),r]|;
A127: |[(((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 A4, A6, A124, JORDAN1A:21;
A128: |[(((W-bound C) + (E-bound C)) / 2),r]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;

A129: now

assume |[(((W-bound C) + (E-bound C)) / 2),r]| in C ; :: thesis:
then |[(((W-bound C) + (E-bound C)) / 2),r]| in (Lower_Arc C) \/ (Upper_Arc C) by JORDAN6:65;
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 A127, 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:43;
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:128;
hence contradiction by A125, RELAT_1:153; :: thesis:

end;

A130: meet (BDD-Family C) = C \/ (BDD C) by JORDAN10:21;
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:
A131: 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:
then consider k1 being Element of NAT such that
A132: Y = Cl (BDD (L~ (Cage C,k1))) by A131;
consider k0 being Element of NAT such that
A133: k1 <= k0 and
A134: r in S . k0 by A126;
A135: E . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Es . k0)]| by A12;
then A136: (E . k0) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A137: F . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Fs . k0)]| by A14;
then A138: (F . k0) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A139: ( proj2 . (E . k0) = (E . k0) `2 & proj2 . (F . k0) = (F . k0) `2 ) by PSCOMP_1:def 29;
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) by PSCOMP_1:64;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:24;
A140: X-SpanStart C,(k0 + 1) = Center (Gauge C,(k0 + 1)) by JORDAN1B:17;
(E . k0) `2 = Es . k0 by A135, EUCLID:56
.= inf (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 A11 ;
then consider j being Element of NAT such that
A141: 1 <= j and
A142: j <= width (Gauge C,(k0 + 1)) and
A143: E . k0 = (Gauge C,(k0 + 1)) * (X-SpanStart C,(k0 + 1)),j by A1, A8, A136, A140, JORDAN1F:13;
E . k0 in Upper_Arc (L~ (Cage C,(k0 + 1))) by A15;
then A144: LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . k0) meets Lower_Arc (L~ (Cage C,(k0 + 1))) by A1, A140, A141, A142, A143, JORDAN1J:62;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A145: (dom proj2 ) /\ DD = DD by XBOOLE_1:28;
DD <> {} by A144, XBOOLE_0:def 7;
then dom proj2 meets DD by A145, XBOOLE_0:def 7;
then A146: D <> {} by RELAT_1:151;
Fs . k0 = sup D by A13;
then Fs . k0 in D by A146, RCOMP_1:32;
then consider dd being Point of (TOP-REAL 2) such that
A147: dd in DD and
A148: Fs . k0 = proj2 . dd by FUNCT_2:116;
A149: dd in LSeg (E . k0),((Gauge C,1) * (X-SpanStart C,1),1) by A147, XBOOLE_0:def 4;
E . k0 in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A136, JORDAN1A:17;
then LSeg (E . k0),((Gauge C,1) * (X-SpanStart C,1),1) c= Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A5, JORDAN1A:23;
then A150: dd `1 = (F . k0) `1 by A138, A149, JORDAN6:34;
A151: (F . k0) `2 = Fs . k0 by A137, EUCLID:56
.= dd `2 by A148, PSCOMP_1:def 29 ;
then A152: F . k0 in LSeg (E . k0),((Gauge C,1) * (X-SpanStart C,1),1) by A149, A150, TOPREAL3: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,(k0 + 1)))) as compact Subset of (TOP-REAL 2) by PSCOMP_1:64;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:24;
A153: 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:34;
1 + 0 <= k0 + 1 by NAT_1:11;
then A154: 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 A1, A153, JORDAN1A:65, XBOOLE_1:63;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A155: (dom proj2 ) /\ DD = DD by XBOOLE_1:28;
DD <> {} by A154, XBOOLE_0:def 7;
then dom proj2 meets DD by A155, XBOOLE_0:def 7;
then A156: D <> {} by RELAT_1:151;
Es . k0 = inf D by A11;
then Es . k0 in D by A156, RCOMP_1:32;
then consider dd being Point of (TOP-REAL 2) such that
A157: dd in DD and
A158: Es . k0 = proj2 . dd by FUNCT_2:116;
A159: dd in LSeg ((Gauge C,1) * (X-SpanStart C,1),1),((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))) by A157, XBOOLE_0:def 4;
then A160: dd `1 = (E . k0) `1 by A7, A136, JORDAN6:34;
A161: (E . k0) `2 = Es . k0 by A135, EUCLID:56
.= dd `2 by A158, PSCOMP_1:def 29 ;
then A162: E . k0 in LSeg ((Gauge C,1) * (X-SpanStart C,1),1),((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))) by A159, A160, TOPREAL3:11;
A163: ((Gauge C,1) * (X-SpanStart C,1),1) `2 <= (E . k0) `2 by A9, A159, A161, TOPREAL1:10;
then A164: (F . k0) `2 <= (E . k0) `2 by A149, A151, TOPREAL1:10;
r in proj2 .: (LSeg (E . k0),(F . k0)) by A43, A134;
then r in [.(proj2 . (F . k0)),(proj2 . (E . k0)).] by A139, A164, SPRECT_1:61;
then A165: |[(((W-bound C) + (E-bound C)) / 2),r]| in LSeg (E . k0),(F . k0) by A136, A138, JORDAN1A:21;
(E . k0) `2 = Es . k0 by A135, EUCLID:56
.= inf (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 A11 ;
then consider j being Element of NAT such that
A166: 1 <= j and
A167: j <= width (Gauge C,(k0 + 1)) and
A168: E . k0 = (Gauge C,(k0 + 1)) * (X-SpanStart C,(k0 + 1)),j by A1, A8, A136, A140, JORDAN1F:13;
A169: E . k0 in Upper_Arc (L~ (Cage C,(k0 + 1))) by A15;
A170: F . k0 in Lower_Arc (L~ (Cage C,(k0 + 1))) by A26;
A171: (F . k0) `2 = Fs . k0 by A137, EUCLID:56
.= sup (proj2 .: ((LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . k0)) /\ (Lower_Arc (L~ (Cage C,(k0 + 1)))))) by A13 ;
then consider k being Element of NAT such that
A172: 1 <= k and
A173: k <= width (Gauge C,(k0 + 1)) and
A174: F . k0 = (Gauge C,(k0 + 1)) * (X-SpanStart C,(k0 + 1)),k by A1, A138, A140, A166, A167, A168, A169, JORDAN1I:30;
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) by PSCOMP_1:64;
reconsider W = proj2 .: CC as compact Subset of REAL by JCT_MISC:24;
CC c= the carrier of (TOP-REAL 2) ;
then CC c= dom proj2 by FUNCT_2:def 1;
then A175: (dom proj2 ) /\ CC = CC by XBOOLE_1:28;
CC <> {} by A144, XBOOLE_0:def 7;
then dom proj2 meets CC by A175, XBOOLE_0:def 7;
then A176: W <> {} by RELAT_1:151;
A177: 1 <= Center (Gauge C,(k0 + 1)) by JORDAN1B:12;
A178: Center (Gauge C,(k0 + 1)) <= len (Gauge C,(k0 + 1)) by JORDAN1B:14;
for p being real number st p in W holds
p <= (E . k0) `2

proof

let p be real number ; :: thesis:
assume p in W ; :: thesis:
then consider x being set such that
x in dom proj2 and
A179: x in CC and
A180: p = proj2 . x by FUNCT_1:def 12;
reconsider x = x as Point of (TOP-REAL 2) by A179;
x in LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . k0) by A179, XBOOLE_0:def 4;
then x `2 <= (E . k0) `2 by A163, TOPREAL1:10;
hence p <= (E . k0) `2 by A180, PSCOMP_1:def 29; :: thesis:

end;

then sup W <= (E . k0) `2 by A176, SEQ_4:62;
then A181: k <= j by A140, A166, A168, A171, A173, A174, A177, A178, GOBOARD5:5;
A182: E . k0 in LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . k0) by RLTOPSP1:69;
then A183: LSeg (E . k0),(F . k0) c= LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . k0) by A152, TOPREAL1:12;
(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:69;
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 A162, TOPREAL1:12;
then A184: 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 A152, A182, TOPREAL1:12;
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:
thus ( x in (LSeg (E . k0),(F . k0)) /\ (Upper_Arc (L~ (Cage C,(k0 + 1)))) implies x = E . k0 ) :: thesis:

proof

assume A185: x in (LSeg (E . k0),(F . k0)) /\ (Upper_Arc (L~ (Cage C,(k0 + 1)))) ; :: thesis:
then reconsider p = x as Point of (TOP-REAL 2) ;
A186: p in LSeg (E . k0),(F . k0) by A185, XBOOLE_0:def 4;
then A187: p `1 = (E . k0) `1 by A136, A138, GOBOARD7:5;
A188: p `2 <= (E . k0) `2 by A164, A186, TOPREAL1:10;
E . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Es . k0)]| by A12;
then A189: (E . k0) `2 = Es . k0 by EUCLID:56
.= inf D by A11 ;
D is bounded by RCOMP_1:28;
then A190: D is bounded_below ;
p in Upper_Arc (L~ (Cage C,(k0 + 1))) by A185, XBOOLE_0:def 4;
then p in DD by A184, A186, XBOOLE_0:def 4;
then proj2 . p in D by FUNCT_2:43;
then p `2 in D by PSCOMP_1:def 29;
then (E . k0) `2 <= p `2 by A189, A190, SEQ_4:def 5;
then p `2 = (E . k0) `2 by A188, XXREAL_0:1;
hence x = E . k0 by A187, TOPREAL3:11; :: thesis:

end;

assume A191: x = E . k0 ; :: thesis:
then x in LSeg (E . k0),(F . k0) by RLTOPSP1:69;
hence x in (LSeg (E . k0),(F . k0)) /\ (Upper_Arc (L~ (Cage C,(k0 + 1)))) by A169, A191, XBOOLE_0:def 4; :: thesis:

end;

then A192: (LSeg (E . k0),(F . k0)) /\ (Upper_Arc (L~ (Cage C,(k0 + 1)))) = {(E . k0)} by TARSKI:def 1;
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) by PSCOMP_1:64;
reconsider E0 = proj2 .: EE as compact Subset of REAL by JCT_MISC:24;
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:
thus ( x in (LSeg (E . k0),(F . k0)) /\ (Lower_Arc (L~ (Cage C,(k0 + 1)))) implies x = F . k0 ) :: thesis:

proof

assume A193: x in (LSeg (E . k0),(F . k0)) /\ (Lower_Arc (L~ (Cage C,(k0 + 1)))) ; :: thesis:
then reconsider p = x as Point of (TOP-REAL 2) ;
A194: p in LSeg (E . k0),(F . k0) by A193, XBOOLE_0:def 4;
then A195: p `1 = (F . k0) `1 by A136, A138, GOBOARD7:5;
A196: p `2 >= (F . k0) `2 by A164, A194, TOPREAL1:10;
F . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Fs . k0)]| by A14;
then A197: (F . k0) `2 = Fs . k0 by EUCLID:56
.= sup E0 by A13 ;
E0 is bounded by RCOMP_1:28;
then A198: E0 is bounded_above ;
p in Lower_Arc (L~ (Cage C,(k0 + 1))) by A193, XBOOLE_0:def 4;
then p in EE by A183, A194, XBOOLE_0:def 4;
then proj2 . p in E0 by FUNCT_2:43;
then p `2 in E0 by PSCOMP_1:def 29;
then (F . k0) `2 >= p `2 by A197, A198, SEQ_4:def 4;
then p `2 = (F . k0) `2 by A196, XXREAL_0:1;
hence x = F . k0 by A195, TOPREAL3:11; :: thesis:

end;

assume A199: x = F . k0 ; :: thesis:
then x in LSeg (E . k0),(F . k0) by RLTOPSP1:69;
hence x in (LSeg (E . k0),(F . k0)) /\ (Lower_Arc (L~ (Cage C,(k0 + 1)))) by A170, A199, XBOOLE_0:def 4; :: thesis:

end;

then (LSeg (E . k0),(F . k0)) /\ (Lower_Arc (L~ (Cage C,(k0 + 1)))) = {(F . k0)} by TARSKI:def 1;
then LSeg (E . k0),(F . k0) c= Cl (RightComp (Cage C,(k0 + 1))) by A140, A166, A167, A168, A172, A173, A174, A181, A192, Lm1;
then A200: |[(((W-bound C) + (E-bound C)) / 2),r]| in Cl (RightComp (Cage C,(k0 + 1))) by A165;
A201: RightComp (Cage C,(k0 + 1)) c= RightComp (Cage C,k0) by JORDAN1H:56, NAT_1:11;
RightComp (Cage C,k0) c= RightComp (Cage C,k1) by A133, JORDAN1H:56;
then RightComp (Cage C,(k0 + 1)) c= RightComp (Cage C,k1) by A201, XBOOLE_1:1;
then Cl (RightComp (Cage C,(k0 + 1))) c= Cl (RightComp (Cage C,k1)) by PRE_TOPC:49;
then |[(((W-bound C) + (E-bound C)) / 2),r]| in Cl (RightComp (Cage C,k1)) by A200;
hence |[(((W-bound C) + (E-bound C)) / 2),r]| in Y by A132, GOBRD14:47; :: thesis:

end;

then |[(((W-bound C) + (E-bound C)) / 2),r]| in meet (BDD-Family C) by SETFAM_1:def 1;
then |[(((W-bound C) + (E-bound C)) / 2),r]| in BDD C by A129, A130, XBOOLE_0:def 3;
then consider n, i, j being Element of NAT such that
A202: 1 < i and
A203: i < len (Gauge C,n) and
A204: 1 < j and
A205: j < width (Gauge C,n) and
A206: |[(((W-bound C) + (E-bound C)) / 2),r]| `1 <> ((Gauge C,n) * i,j) `1 and
A207: |[(((W-bound C) + (E-bound C)) / 2),r]| in cell (Gauge C,n),i,j and
A208: cell (Gauge C,n),i,j c= BDD C by JORDAN1C:35;
take n ; :: thesis:
take j ; :: according to JORDAN1H:def 3 :: thesis:
thus j < width (Gauge C,n) by A205; :: thesis:
A209: n > 0 by A203, A205, A208, JORDAN1B:44;
A210: X-SpanStart C,n = Center (Gauge C,n) by JORDAN1B:17;
A211: ( 1 <= X-SpanStart C,n & X-SpanStart C,n <= len (Gauge C,n) ) by JORDAN1H:58, XXREAL_0:2;
4 <= len (Gauge C,1) by JORDAN8:13;
then A212: 1 <= len (Gauge C,1) by XXREAL_0:2;
len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then ((Gauge C,n) * (X-SpanStart C,n),j) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, A4, A204, A205, A209, A210, A212, JORDAN1A:57;
hence cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C by A128, A202, A203, A204, A205, A206, A207, A208, A211, JORDAN1B:23; :: thesis: