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:17;
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:13;
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:59;
then A6: (Gauge C,1) * (X-SpanStart C,1),1 in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN1A:17;
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 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:5;
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 29;
4 <= len (Gauge C,1) by JORDAN8:13;
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 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
A10: for i being Element of NAT holds Es . i = H₁(i) from FUNCT_2:sch 4();
A11: (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;
(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 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 A11, JCT_MISC:24;
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();
A13: ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))) `1 = ((W-bound C) + (E-bound C)) / 2 by A2, A4, 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 A14: 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:23;
A15: A misses B

proof

assume A meets B ; :: thesis: contradiction
then consider z being set such that
A16: z in A and
A17: z in B by XBOOLE_0:3;
reconsider z = z as Real by A16;
consider p being Point of (TOP-REAL 2) such that
A18: 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
A19: z = proj2 . p by A16, FUNCT_2:116;
A20: p in Upper_Arc C by A18, XBOOLE_0:def 4;
consider q being Point of (TOP-REAL 2) such that
A21: 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
A22: z = proj2 . q by A17, FUNCT_2:116;
A23: p `2 = proj2 . q by A19, A22, PSCOMP_1:def 29
.= q `2 by PSCOMP_1:def 29 ;
A24: q in Lower_Arc C by A21, XBOOLE_0:def 4;
A25: q in LSeg ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))),((Gauge C,1) * (X-SpanStart C,1),1) by A21, XBOOLE_0:def 4;
A26: p in LSeg ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))),((Gauge C,1) * (X-SpanStart C,1),1) by A18, XBOOLE_0:def 4;
then p `1 = ((W-bound C) + (E-bound C)) / 2 by A14, JORDAN6:34
.= q `1 by A14, A25, JORDAN6:34 ;
then p = q by A23, TOPREAL3:11;
then p in (Upper_Arc C) /\ (Lower_Arc C) by A20, A24, XBOOLE_0:def 4;
then A27: p in {(W-min C),(E-max C)} by JORDAN6:65;

per cases ( p = W-min C or p = E-max C ) by A27, TARSKI:def 2;

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

A29: (W-min C) `1 = W-bound C by EUCLID:56;
(W-min C) `1 = ((W-bound C) + (E-bound C)) / 2 by A14, A26, A28, JORDAN6:34;
hence contradiction by A29, SPRECT_1:33; :: thesis: verum

end;

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

A31: (E-max C) `1 = E-bound C by EUCLID:56;
(E-max C) `1 = ((W-bound C) + (E-bound C)) / 2 by A14, A26, A30, JORDAN6:34;
hence contradiction by A31, SPRECT_1:33; :: thesis: verum

end;

end;

end;

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
A32: 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
A33: for i being Element of NAT holds F . i = H₄(i) from FUNCT_2:sch 4();
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
A34: for i being Element of NAT holds S . i = H₅(i) from FUNCT_2:sch 4();
A35: 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;
A36: 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) 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 A37: (dom proj2 ) /\ DD = DD by XBOOLE_1:28;
A38: X-SpanStart C,(i + 1) = Center (Gauge C,(i + 1)) by JORDAN1B:17;
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:34;
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, A38, A36, JORDAN1A:65, XBOOLE_1:63;
then DD <> {} by XBOOLE_0:def 7;
then dom proj2 meets DD by A37, XBOOLE_0:def 7;
then A39: D <> {} by RELAT_1:151;
Es . i = inf D by A10;
then consider dd being Point of (TOP-REAL 2) such that
A40: dd in DD and
A41: Es . i = proj2 . dd by A39, FUNCT_2:116, RCOMP_1:32;
A42: dd in LSeg ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))),((Gauge C,1) * (X-SpanStart C,1),1) by A40, XBOOLE_0:def 4;
A43: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A12;
then (E . i) `2 = Es . i by EUCLID:56;
then A44: dd `2 = (E . i) `2 by A41, PSCOMP_1:def 29;
(E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by A43, EUCLID:56;
then A45: dd `1 = (E . i) `1 by A14, A42, JORDAN6:34;
dd in Upper_Arc (L~ (Cage C,(i + 1))) by A40, XBOOLE_0:def 4;
hence E . i in Upper_Arc (L~ (Cage C,(i + 1))) by A45, A44, TOPREAL3:11; :: thesis: verum

end;

A46: 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;
A47: X-SpanStart C,(i + 1) = Center (Gauge C,(i + 1)) by JORDAN1B:17;
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;
A48: E . i in Upper_Arc (L~ (Cage C,(i + 1))) by A35;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A49: (dom proj2 ) /\ DD = DD by XBOOLE_1:28;
A50: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A12;
then A51: (E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
then E . i in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN1A:17;
then A52: LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) c= Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A6, JORDAN1A:23;
(E . i) `2 = Es . i by A50, 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 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, A47, A51, JORDAN1F:13;
then LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . i) meets Lower_Arc (L~ (Cage C,(i + 1))) by A2, A47, A48, JORDAN1J:62;
then DD <> {} by XBOOLE_0:def 7;
then dom proj2 meets DD by A49, XBOOLE_0:def 7;
then A53: D <> {} by RELAT_1:151;
Fs . i = sup D by A32;
then consider dd being Point of (TOP-REAL 2) such that
A54: dd in DD and
A55: Fs . i = proj2 . dd by A53, FUNCT_2:116, RCOMP_1:32;
A56: dd in Lower_Arc (L~ (Cage C,(i + 1))) by A54, XBOOLE_0:def 4;
A57: F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A33;
then (F . i) `2 = Fs . i by EUCLID:56;
then A58: dd `2 = (F . i) `2 by A55, PSCOMP_1:def 29;
A59: dd in LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) by A54, XBOOLE_0:def 4;
(F . i) `1 = ((W-bound C) + (E-bound C)) / 2 by A57, EUCLID:56;
then dd `1 = (F . i) `1 by A59, A52, JORDAN6:34;
hence F . i in Lower_Arc (L~ (Cage C,(i + 1))) by A56, A58, TOPREAL3:11; :: thesis: verum

end;

A60: 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: ( S . i is connected & 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) by PSCOMP_1:64;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:24;
A61: X-SpanStart C,(i + 1) = Center (Gauge C,(i + 1)) by JORDAN1B:17;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A62: (dom proj2 ) /\ DD = DD by XBOOLE_1:28;
A63: 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:34;
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, A63, JORDAN1A:65, XBOOLE_1:63;
then DD <> {} by XBOOLE_0:def 7;
then dom proj2 meets DD by A62, XBOOLE_0:def 7;
then A64: D <> {} by RELAT_1:151;
Es . i = inf D by A10;
then consider dd being Point of (TOP-REAL 2) such that
A65: dd in DD and
A66: Es . i = proj2 . dd by A64, FUNCT_2:116, RCOMP_1:32;
A67: dd in LSeg ((Gauge C,1) * (X-SpanStart C,1),1),((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))) by A65, 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) 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 A68: (dom proj2 ) /\ DD = DD by XBOOLE_1:28;
A69: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A12;
then A70: (E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A71: F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A33;
then A72: (F . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A73: (F . i) `2 = Fs . i by A71, EUCLID:56
.= sup (proj2 .: ((LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . i)) /\ (Lower_Arc (L~ (Cage C,(i + 1)))))) by A32 ;
(E . i) `2 = Es . i by A69, 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 A10 ;
then consider j being Element of NAT such that
A74: 1 <= j and
A75: j <= width (Gauge C,(i + 1)) and
A76: E . i = (Gauge C,(i + 1)) * (X-SpanStart C,(i + 1)),j by A2, A1, A70, A61, JORDAN1F:13;
A77: E . i in Upper_Arc (L~ (Cage C,(i + 1))) by A35;
then consider k being Element of NAT such that
A78: 1 <= k and
A79: k <= width (Gauge C,(i + 1)) and
A80: F . i = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),k by A2, A61, A72, A74, A75, A76, A73, JORDAN1I:30;
(E . i) `2 = Es . i by A69, 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 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, A70, A61, JORDAN1F:13;
then LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . i) meets Lower_Arc (L~ (Cage C,(i + 1))) by A2, A61, A77, JORDAN1J:62;
then DD <> {} by XBOOLE_0:def 7;
then dom proj2 meets DD by A68, XBOOLE_0:def 7;
then A81: D <> {} by RELAT_1:151;
A82: (E . i) `2 = Es . i by A69, EUCLID:56
.= dd `2 by A66, PSCOMP_1:def 29 ;
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
A83: x in DD and
A84: p = proj2 . x by FUNCT_1:def 12;
A85: ((Gauge C,1) * (X-SpanStart C,1),1) `2 <= (E . i) `2 by A7, A67, A82, TOPREAL1:10;
reconsider x = x as Point of (TOP-REAL 2) by A83;
x in LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . i) by A83, XBOOLE_0:def 4;
then x `2 <= (E . i) `2 by A85, TOPREAL1:10;
hence p <= (E . i) `2 by A84, PSCOMP_1:def 29; :: thesis: verum

end;

then A86: sup D <= (E . i) `2 by A81, SEQ_4:62;
dd `1 = (E . i) `1 by A14, A70, A67, JORDAN6:34;
then A87: E . i in LSeg ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))),((Gauge C,1) * (X-SpanStart C,1),1) by A67, A82, TOPREAL3:11;
Fs . i = sup D by A32;
then consider dd being Point of (TOP-REAL 2) such that
A88: dd in DD and
A89: Fs . i = proj2 . dd by A81, FUNCT_2:116, RCOMP_1:32;
A90: (F . i) `2 = Fs . i by A71, EUCLID:56
.= dd `2 by A89, PSCOMP_1:def 29 ;
A91: dd in LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) by A88, XBOOLE_0:def 4;
E . i in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A70, 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 A6, JORDAN1A:23;
then dd `1 = (F . i) `1 by A72, A91, JORDAN6:34;
then A92: F . i in LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) by A91, A90, 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 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 A87, TOPREAL1:12;
then A93: 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 A87, A92, TOPREAL1:12;
A94: 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) by PSCOMP_1:64;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:24;
assume A95: 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) ;
A96: p in LSeg (E . i),(F . i) by A95, XBOOLE_0:def 4;
p in Upper_Arc (L~ (Cage C,(i + 1))) by A95, XBOOLE_0:def 4;
then p in DD by A93, A96, XBOOLE_0:def 4;
then proj2 . p in D by FUNCT_2:43;
then A97: p `2 in D by PSCOMP_1:def 29;
E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A12;
then A98: (E . i) `2 = Es . i by EUCLID:56
.= inf D by A10 ;
D is bounded by RCOMP_1:28;
then A99: (E . i) `2 <= p `2 by A98, A97, SEQ_4:def 5;
p `2 <= (E . i) `2 by A73, A86, A96, TOPREAL1:10;
then A100: p `2 = (E . i) `2 by A99, XXREAL_0:1;
p `1 = (E . i) `1 by A70, A72, A96, GOBOARD7:5;
hence x = E . i by A100, TOPREAL3:11; :: thesis: verum

end;

A101: (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:69;
A102: (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 A61, A76, A80, A94;
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 A61, A77, A76, A101, XBOOLE_0:def 4; :: thesis: verum

end;

E . i in LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) by RLTOPSP1:69;
then A103: LSeg (E . i),(F . i) c= LSeg (E . i),((Gauge C,1) * (X-SpanStart C,1),1) by A92, TOPREAL1:12;
A104: 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) by PSCOMP_1:64;
reconsider E0 = proj2 .: EE as compact Subset of REAL by JCT_MISC:24;
assume A105: 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) ;
A106: p in LSeg (E . i),(F . i) by A105, XBOOLE_0:def 4;
p in Lower_Arc (L~ (Cage C,(i + 1))) by A105, XBOOLE_0:def 4;
then p in EE by A103, A106, XBOOLE_0:def 4;
then proj2 . p in E0 by FUNCT_2:43;
then A107: p `2 in E0 by PSCOMP_1:def 29;
F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A33;
then A108: (F . i) `2 = Fs . i by EUCLID:56
.= sup E0 by A32 ;
E0 is bounded by RCOMP_1:28;
then A109: (F . i) `2 >= p `2 by A108, A107, SEQ_4:def 4;
p `2 >= (F . i) `2 by A73, A86, A106, TOPREAL1:10;
then A110: p `2 = (F . i) `2 by A109, XXREAL_0:1;
p `1 = (F . i) `1 by A70, A72, A106, GOBOARD7:5;
hence x = F . i by A110, TOPREAL3:11; :: thesis: verum

end;

A111: F . i in Lower_Arc (L~ (Cage C,(i + 1))) by A46;
A112: S . i = proj2 .: (LSeg (E . i),(F . i)) by A34;
hence S . i is connected by JCT_MISC:15; :: thesis: ( S . i meets A & S . i meets B )
A113: Center (Gauge C,(i + 1)) <= len (Gauge C,(i + 1)) by JORDAN1B:14;
A114: (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;
A115: (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 A61, A76, A80, A104;
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 A80, A111, A114, XBOOLE_0:def 4; :: thesis: verum

end;

1 <= Center (Gauge C,(i + 1)) by JORDAN1B:12;
then A116: k <= j by A61, A74, A76, A73, A79, A80, A113, A86, GOBOARD5:5;
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 A61, A93, A75, A76, A78, A80, A102, A115, JORDAN1J:64, XBOOLE_1:77;
hence S . i meets A by A112, JORDAN1A:24; :: 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 A61, A93, A75, A76, A78, A80, A116, A102, A115, JORDAN1J:63, XBOOLE_1:77;
hence S . i meets B by A112, JORDAN1A:24; :: 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 29;
then A117: 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:61;
then A118: 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:156, 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 A117, RELAT_1:156, XBOOLE_1:17;
then consider r being real number such that
A119: r in [.(proj2 . ((Gauge C,1) * (X-SpanStart C,1),1)),(proj2 . ((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1)))).] and
A120: not r in A \/ B and
A121: for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) by A15, A118, A60, JCT_MISC:21;
reconsider r = r as Real by XREAL_0:def 1;
set p = |[(((W-bound C) + (E-bound C)) / 2),r]|;
A122: |[(((W-bound C) + (E-bound C)) / 2),r]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
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 )
A123: 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
A124: Y = Cl (BDD (L~ (Cage C,k1))) by A123;
consider k0 being Element of NAT such that
A125: k1 <= k0 and
A126: r in S . k0 by A121;
A127: proj2 . (F . k0) = (F . k0) `2 by PSCOMP_1:def 29;
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 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;
A128: Center (Gauge C,(k0 + 1)) <= len (Gauge C,(k0 + 1)) by JORDAN1B:14;
reconsider E0 = proj2 .: EE 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 A129: (dom proj2 ) /\ CC = CC by XBOOLE_1:28;
A130: 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 A125, JORDAN1H:56;
then RightComp (Cage C,(k0 + 1)) c= RightComp (Cage C,k1) by A130, XBOOLE_1:1;
then A131: Cl (RightComp (Cage C,(k0 + 1))) c= Cl (RightComp (Cage C,k1)) by PRE_TOPC:49;
A132: E . k0 in Upper_Arc (L~ (Cage C,(k0 + 1))) by A35;
A133: 1 + 0 <= k0 + 1 by NAT_1:11;
A134: E . k0 in Upper_Arc (L~ (Cage C,(k0 + 1))) by A35;
A135: X-SpanStart C,(k0 + 1) = Center (Gauge C,(k0 + 1)) by JORDAN1B:17;
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;
A136: proj2 . (E . k0) = (E . k0) `2 by PSCOMP_1:def 29;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:24;
A137: Fs . k0 = sup D by A32;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A138: (dom proj2 ) /\ DD = DD by XBOOLE_1:28;
A139: E . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Es . k0)]| by A12;
then A140: (E . k0) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
(E . k0) `2 = Es . k0 by A139, 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 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, A140, A135, JORDAN1F:13;
then A141: LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . k0) meets Lower_Arc (L~ (Cage C,(k0 + 1))) by A2, A135, A134, JORDAN1J:62;
then DD <> {} by XBOOLE_0:def 7;
then dom proj2 meets DD by A138, XBOOLE_0:def 7;
then D <> {} by RELAT_1:151;
then consider dd being Point of (TOP-REAL 2) such that
A142: dd in DD and
A143: Fs . k0 = proj2 . dd by A137, FUNCT_2:116, RCOMP_1:32;
A144: dd in LSeg (E . k0),((Gauge C,1) * (X-SpanStart C,1),1) by A142, 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) 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 A145: (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:34;
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, A133, JORDAN1A:65, XBOOLE_1:63;
then DD <> {} by XBOOLE_0:def 7;
then dom proj2 meets DD by A145, XBOOLE_0:def 7;
then A146: D <> {} by RELAT_1:151;
A147: F . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Fs . k0)]| by A33;
then A148: (F . k0) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A149: (F . k0) `2 = Fs . k0 by A147, EUCLID:56
.= dd `2 by A143, PSCOMP_1:def 29 ;
E . k0 in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A140, 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 A6, JORDAN1A:23;
then dd `1 = (F . k0) `1 by A148, A144, JORDAN6:34;
then A150: F . k0 in LSeg (E . k0),((Gauge C,1) * (X-SpanStart C,1),1) by A144, A149, TOPREAL3:11;
Es . k0 = inf D by A10;
then consider dd being Point of (TOP-REAL 2) such that
A151: dd in DD and
A152: Es . k0 = proj2 . dd by A146, FUNCT_2:116, RCOMP_1:32;
A153: dd in LSeg ((Gauge C,1) * (X-SpanStart C,1),1),((Gauge C,1) * (X-SpanStart C,1),(len (Gauge C,1))) by A151, XBOOLE_0:def 4;
A154: (E . k0) `2 = Es . k0 by A139, EUCLID:56
.= dd `2 by A152, PSCOMP_1:def 29 ;
then A155: ((Gauge C,1) * (X-SpanStart C,1),1) `2 <= (E . k0) `2 by A7, A153, TOPREAL1:10;
then A156: (F . k0) `2 <= (E . k0) `2 by A144, A149, TOPREAL1:10;
r in proj2 .: (LSeg (E . k0),(F . k0)) by A34, A126;
then r in [.(proj2 . (F . k0)),(proj2 . (E . k0)).] by A136, A127, A156, SPRECT_1:61;
then A157: |[(((W-bound C) + (E-bound C)) / 2),r]| in LSeg (E . k0),(F . k0) by A140, A148, JORDAN1A:21;
A158: F . k0 in Lower_Arc (L~ (Cage C,(k0 + 1))) by A46;
A159: (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;
A160: E . k0 in LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . k0) by RLTOPSP1:69;
then A161: LSeg (E . k0),(F . k0) c= LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . k0) by A150, TOPREAL1:12;
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 A33;
then A162: (F . k0) `2 = Fs . k0 by EUCLID:56
.= sup E0 by A32 ;
assume A163: 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) ;
A164: p in LSeg (E . k0),(F . k0) by A163, XBOOLE_0:def 4;
then A165: p `2 >= (F . k0) `2 by A156, TOPREAL1:10;
p in Lower_Arc (L~ (Cage C,(k0 + 1))) by A163, XBOOLE_0:def 4;
then p in EE by A161, A164, XBOOLE_0:def 4;
then proj2 . p in E0 by FUNCT_2:43;
then A166: p `2 in E0 by PSCOMP_1:def 29;
E0 is bounded by RCOMP_1:28;
then (F . k0) `2 >= p `2 by A162, A166, SEQ_4:def 4;
then A167: p `2 = (F . k0) `2 by A165, XXREAL_0:1;
p `1 = (F . k0) `1 by A140, A148, A164, GOBOARD7:5;
hence x = F . k0 by A167, TOPREAL3:11; :: thesis: verum

end;

assume A168: 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:69;
hence x in (LSeg (E . k0),(F . k0)) /\ (Lower_Arc (L~ (Cage C,(k0 + 1)))) by A158, A168, XBOOLE_0:def 4; :: thesis: verum

end;

then A169: (LSeg (E . k0),(F . k0)) /\ (Lower_Arc (L~ (Cage C,(k0 + 1)))) = {(F . k0)} by TARSKI:def 1;
A170: 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
A171: x in CC and
A172: p = proj2 . x by FUNCT_1:def 12;
reconsider x = x as Point of (TOP-REAL 2) by A171;
x in LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . k0) by A171, XBOOLE_0:def 4;
then x `2 <= (E . k0) `2 by A155, TOPREAL1:10;
hence p <= (E . k0) `2 by A172, PSCOMP_1:def 29; :: thesis: verum

end;

CC <> {} by A141, XBOOLE_0:def 7;
then dom proj2 meets CC by A129, XBOOLE_0:def 7;
then W <> {} by RELAT_1:151;
then A173: sup W <= (E . k0) `2 by A170, SEQ_4:62;
dd `1 = (E . k0) `1 by A14, A140, A153, JORDAN6:34;
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 A153, A154, TOPREAL3:11;
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 A159, TOPREAL1:12;
then A174: 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 A150, A160, 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: ( 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 A12;
then A175: (E . k0) `2 = Es . k0 by EUCLID:56
.= inf D by A10 ;
assume A176: 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) ;
A177: p in LSeg (E . k0),(F . k0) by A176, XBOOLE_0:def 4;
then A178: p `2 <= (E . k0) `2 by A156, TOPREAL1:10;
p in Upper_Arc (L~ (Cage C,(k0 + 1))) by A176, XBOOLE_0:def 4;
then p in DD by A174, A177, XBOOLE_0:def 4;
then proj2 . p in D by FUNCT_2:43;
then A179: p `2 in D by PSCOMP_1:def 29;
D is bounded by RCOMP_1:28;
then (E . k0) `2 <= p `2 by A175, A179, SEQ_4:def 5;
then A180: p `2 = (E . k0) `2 by A178, XXREAL_0:1;
p `1 = (E . k0) `1 by A140, A148, A177, GOBOARD7:5;
hence x = E . k0 by A180, TOPREAL3:11; :: thesis: verum

end;

assume A181: 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:69;
hence x in (LSeg (E . k0),(F . k0)) /\ (Upper_Arc (L~ (Cage C,(k0 + 1)))) by A132, A181, XBOOLE_0:def 4; :: thesis: verum

end;

then A182: (LSeg (E . k0),(F . k0)) /\ (Upper_Arc (L~ (Cage C,(k0 + 1)))) = {(E . k0)} by TARSKI:def 1;
(E . k0) `2 = Es . k0 by A139, 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 A10 ;
then consider j being Element of NAT such that
A183: 1 <= j and
A184: j <= width (Gauge C,(k0 + 1)) and
A185: E . k0 = (Gauge C,(k0 + 1)) * (X-SpanStart C,(k0 + 1)),j by A2, A1, A140, A135, JORDAN1F:13;
A186: (F . k0) `2 = Fs . k0 by A147, EUCLID:56
.= sup (proj2 .: ((LSeg ((Gauge C,1) * (X-SpanStart C,1),1),(E . k0)) /\ (Lower_Arc (L~ (Cage C,(k0 + 1)))))) by A32 ;
then consider k being Element of NAT such that
A187: 1 <= k and
A188: k <= width (Gauge C,(k0 + 1)) and
A189: F . k0 = (Gauge C,(k0 + 1)) * (X-SpanStart C,(k0 + 1)),k by A2, A148, A135, A183, A184, A185, A132, JORDAN1I:30;
1 <= Center (Gauge C,(k0 + 1)) by JORDAN1B:12;
then k <= j by A135, A183, A185, A186, A188, A189, A128, A173, GOBOARD5:5;
then LSeg (E . k0),(F . k0) c= Cl (RightComp (Cage C,(k0 + 1))) by A135, A183, A184, A185, A187, A188, A189, A182, A169, Lm1;
then |[(((W-bound C) + (E-bound C)) / 2),r]| in Cl (RightComp (Cage C,(k0 + 1))) by A157;
then |[(((W-bound C) + (E-bound C)) / 2),r]| in Cl (RightComp (Cage C,k1)) by A131;
hence |[(((W-bound C) + (E-bound C)) / 2),r]| in Y by A124, GOBRD14:47; :: thesis: verum

end;

then A190: |[(((W-bound C) + (E-bound C)) / 2),r]| in meet (BDD-Family C) by SETFAM_1:def 1;
A191: |[(((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, A13, A119, JORDAN1A:21;

A192: now

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: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 A191, 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 A120, RELAT_1:153; :: 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 A192, A190, XBOOLE_0:def 3;
then consider n, i, j being Element of NAT such that
A193: 1 < i and
A194: i < len (Gauge C,n) and
A195: 1 < j and
A196: j < width (Gauge C,n) and
A197: |[(((W-bound C) + (E-bound C)) / 2),r]| `1 <> ((Gauge C,n) * i,j) `1 and
A198: |[(((W-bound C) + (E-bound C)) / 2),r]| in cell (Gauge C,n),i,j and
A199: cell (Gauge C,n),i,j c= BDD C by JORDAN1C:35;
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 A196; :: thesis: cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C
A200: X-SpanStart C,n = Center (Gauge C,n) by JORDAN1B:17;
A201: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A202: X-SpanStart C,n <= len (Gauge C,n) by JORDAN1H:58;
A203: 1 <= X-SpanStart C,n by JORDAN1H:58, XXREAL_0:2;
n > 0 by A194, A196, A199, JORDAN1B:44;
then ((Gauge C,n) * (X-SpanStart C,n),j) `1 = ((W-bound C) + (E-bound C)) / 2 by A2, A5, A195, A196, A200, A9, A201, JORDAN1A:57;
hence cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C by A122, A193, A194, A195, A196, A197, A198, A199, A203, A202, JORDAN1B:23; :: thesis: verum