let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: ex n being 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 H₁( Nat) -> Element of REAL = In ((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)))))))),REAL);
consider Es being Real_Sequence such that
A10: for i being Element of NAT holds Es . i = H₁(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 H₂( Element of NAT ) -> Element of the carrier of (TOP-REAL 2) = |[(((W-bound C) + (E-bound C)) / 2),(Es . $1)]|;
consider E being sequence of the carrier of (TOP-REAL 2) such that
A11: for i being Element of NAT holds E . i = H₂(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 object 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;

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

suppose A27: 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;

suppose A29: 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 H₃( Nat) -> Element of REAL = In ((upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . $1))) /\ (Lower_Arc (L~ (Cage (C,($1 + 1)))))))),REAL);
consider Fs being Real_Sequence such that
A31: 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 sequence of the carrier of (TOP-REAL 2) such that
A32: for i being Element of NAT holds F . i = H₄(i) from FUNCT_2:sch 4();
deffunc H₅( Nat) -> Element of K16(REAL) = proj2 .: (LSeg ((E . $1),(F . $1)));
consider S being sequence of (bool REAL) such that
A33: for i being Element of NAT holds S . i = H₅(i) from FUNCT_2:sch 4();
A34: for i being Nat holds E . i in Upper_Arc (L~ (Cage (C,(i + 1))))

proof

let i be 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 <> {} ;
then dom proj2 meets DD by A36;
then A38: D <> {} by RELAT_1:118;
A39: i in NAT by ORDINAL1:def 12;
then Es . i = H₁(i) by A10;
then consider dd being Point of (TOP-REAL 2) such that
A40: dd in DD and
A41: Es . i = proj2 . dd by A38, FUNCT_2:65, RCOMP_1:14;
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 A11, A39;
then (E . i) `2 = Es . i by EUCLID:52;
then A44: dd `2 = (E . i) `2 by A41, PSCOMP_1:def 6;
(E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by A43, EUCLID:52;
then A45: dd `1 = (E . i) `1 by A13, A42, JORDAN6:31;
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:6; :: thesis: verum

end;

A46: for i being Nat holds F . i in Lower_Arc (L~ (Cage (C,(i + 1))))

proof

let i be 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: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;
A48: E . i in Upper_Arc (L~ (Cage (C,(i + 1)))) by A34;
A49: i in NAT by ORDINAL1:def 12;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A50: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A51: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A11, A49;
then A52: (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 A53: 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 A51, EUCLID:52
.= H₁(i) by A10, A49
.= 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))))))) ;
then ex j being 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, A52, 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 <> {} ;
then dom proj2 meets DD by A50;
then A54: D <> {} by RELAT_1:118;
A55: i in NAT by ORDINAL1:def 12;
Fs . i = H₃(i) by A31, A55;
then consider dd being Point of (TOP-REAL 2) such that
A56: dd in DD and
A57: Fs . i = proj2 . dd by A54, FUNCT_2:65, RCOMP_1:14;
A58: dd in Lower_Arc (L~ (Cage (C,(i + 1)))) by A56, XBOOLE_0:def 4;
A59: F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A32, A55;
then (F . i) `2 = Fs . i by EUCLID:52;
then A60: dd `2 = (F . i) `2 by A57, PSCOMP_1:def 6;
A61: dd in LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A56, XBOOLE_0:def 4;
(F . i) `1 = ((W-bound C) + (E-bound C)) / 2 by A59, EUCLID:52;
then dd `1 = (F . i) `1 by A61, A53, JORDAN6:31;
hence F . i in Lower_Arc (L~ (Cage (C,(i + 1)))) by A58, A60, TOPREAL3:6; :: thesis: verum

end;

A62: for i being Nat holds
( S . i is interval & S . i meets A & S . i meets B )

proof

let i be 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;
A63: 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 A64: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A65: 1 <= i + 1 by NAT_1:11;
A66: i in NAT by ORDINAL1:def 12;
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, A65, JORDAN1A:44, XBOOLE_1:63;
then DD <> {} ;
then dom proj2 meets DD by A64;
then A67: D <> {} by RELAT_1:118;
Es . i = H₁(i) by A10, A66;
then consider dd being Point of (TOP-REAL 2) such that
A68: dd in DD and
A69: Es . i = proj2 . dd by A67, FUNCT_2:65, RCOMP_1:14;
A70: dd in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) by A68, 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 A71: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A72: i in NAT by ORDINAL1:def 12;
A73: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A11, A72;
then A74: (E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A75: F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A32, A72;
then A76: (F . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A77: (F . i) `2 = Fs . i by A75, EUCLID:52
.= H<sub>3</sub>(i) by A31, A72
.= upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))))) ;
(E . i) `2 = Es . i by A73, EUCLID:52
.= H₁(i) by A10, A72
.= 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))))))) ;
then consider j being 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 A2, A1, A74, A63, JORDAN1F:13;
A81: E . i in Upper_Arc (L~ (Cage (C,(i + 1)))) by A34;
then consider k being Nat such that
A82: 1 <= k and
A83: k <= width (Gauge (C,(i + 1))) and
A84: F . i = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k) by A2, A63, A76, A78, A79, A80, A77, JORDAN1I:28;
A85: i in NAT by ORDINAL1:def 12;
(E . i) `2 = Es . i by A73, EUCLID:52
.= H<sub>1</sub>(i) by A10, A85
.= 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))))))) ;
then ex j being 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, A74, A63, JORDAN1F:13;
then LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i)) meets Lower_Arc (L~ (Cage (C,(i + 1)))) by A2, A63, A81, JORDAN1J:62;
then DD <> {} ;
then dom proj2 meets DD by A71;
then A86: D <> {} by RELAT_1:118;
A87: (E . i) `2 = Es . i by A73, EUCLID:52
.= dd `2 by A69, PSCOMP_1:def 6 ;
for p being Real st p in D holds
p <= (E . i) `2

proof

let p be Real; :: thesis: ( p in D implies p <= (E . i) `2 )
assume p in D ; :: thesis: p <= (E . i) `2
then consider x being object such that
x in dom proj2 and
A88: x in DD and
A89: p = proj2 . x by FUNCT_1:def 6;
A90: ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `2 <= (E . i) `2 by A7, A70, A87, TOPREAL1:4;
reconsider x = x as Point of (TOP-REAL 2) by A88;
x in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i)) by A88, XBOOLE_0:def 4;
then x `2 <= (E . i) `2 by A90, TOPREAL1:4;
hence p <= (E . i) `2 by A89, PSCOMP_1:def 6; :: thesis: verum

end;

then A91: upper_bound D <= (E . i) `2 by A86, SEQ_4:45;
dd `1 = (E . i) `1 by A13, A74, A70, JORDAN6:31;
then A92: E . i in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A70, A87, TOPREAL3:6;
Fs . i = H<sub>3</sub>(i) by A31, A85;
then consider dd being Point of (TOP-REAL 2) such that
A93: dd in DD and
A94: Fs . i = proj2 . dd by A86, FUNCT_2:65, RCOMP_1:14;
A95: (F . i) `2 = Fs . i by A75, EUCLID:52
.= dd `2 by A94, PSCOMP_1:def 6 ;
A96: dd in LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A93, XBOOLE_0:def 4;
E . i in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A74, 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 A76, A96, JORDAN6:31;
then A97: F . i in LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A96, A95, 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 A92, TOPREAL1:6;
then A98: 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 A92, A97, TOPREAL1:6;
A99: 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 A100: 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) ;
A101: p in LSeg ((E . i),(F . i)) by A100, XBOOLE_0:def 4;
A102: i in NAT by ORDINAL1:def 12;
p in Upper_Arc (L~ (Cage (C,(i + 1)))) by A100, XBOOLE_0:def 4;
then p in DD by A98, A101, XBOOLE_0:def 4;
then proj2 . p in D by FUNCT_2:35;
then A103: p `2 in D by PSCOMP_1:def 6;
E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A11, A102;
then A104: (E . i) `2 = Es . i by EUCLID:52
.= H₁(i) by A10, A102
.= lower_bound D ;
D is real-bounded by RCOMP_1:10;
then A105: (E . i) `2 <= p `2 by A104, A103, SEQ_4:def 2;
p `2 <= (E . i) `2 by A77, A91, A101, TOPREAL1:4;
then A106: p `2 = (E . i) `2 by A105, XXREAL_0:1;
p `1 = (E . i) `1 by A74, A76, A101, GOBOARD7:5;
hence x = E . i by A106, TOPREAL3:6; :: thesis: verum

end;

A107: (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;
A108: (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 object ; :: 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 A63, A80, A84, A99;
hence x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: 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 A63, A81, A80, A107, 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 A109: LSeg ((E . i),(F . i)) c= LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A97, TOPREAL1:6;
A110: 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 A111: 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) ;
A112: p in LSeg ((E . i),(F . i)) by A111, XBOOLE_0:def 4;
A113: i in NAT by ORDINAL1:def 12;
p in Lower_Arc (L~ (Cage (C,(i + 1)))) by A111, XBOOLE_0:def 4;
then p in EE by A109, A112, XBOOLE_0:def 4;
then proj2 . p in E0 by FUNCT_2:35;
then A114: p `2 in E0 by PSCOMP_1:def 6;
F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A32, A113;
then A115: (F . i) `2 = Fs . i by EUCLID:52
.= H₃(i) by A31, A113
.= upper_bound E0 ;
E0 is real-bounded by RCOMP_1:10;
then A116: (F . i) `2 >= p `2 by A115, A114, SEQ_4:def 1;
p `2 >= (F . i) `2 by A77, A91, A112, TOPREAL1:4;
then A117: p `2 = (F . i) `2 by A116, XXREAL_0:1;
p `1 = (F . i) `1 by A74, A76, A112, GOBOARD7:5;
hence x = F . i by A117, TOPREAL3:6; :: thesis: verum

end;

A118: F . i in Lower_Arc (L~ (Cage (C,(i + 1)))) by A46;
A119: S . i = proj2 .: (LSeg ((E . i),(F . i))) by A33, A85;
hence S . i is interval by JCT_MISC:6; :: thesis: ( S . i meets A & S . i meets B )
A120: Center (Gauge (C,(i + 1))) <= len (Gauge (C,(i + 1))) by JORDAN1B:13;
A121: (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;
A122: (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 object ; :: 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 A63, A80, A84, A110;
hence x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: 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 A84, A118, A121, XBOOLE_0:def 4; :: thesis: verum

end;

1 <= Center (Gauge (C,(i + 1))) by JORDAN1B:11;
then A123: k <= j by A63, A78, A80, A77, A83, A84, A120, A91, 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 A63, A98, A79, A80, A82, A84, A108, A122, JORDAN1J:64, XBOOLE_1:77;
hence S . i meets A by A119, 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 A63, A98, A79, A80, A82, A84, A123, A108, A122, JORDAN1J:63, XBOOLE_1:77;
hence S . i meets B by A119, 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 A124: 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 A125: 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 A124, RELAT_1:123, XBOOLE_1:17;
then consider r being Real such that
A126: r in [.(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1))),(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))).] and
A127: not r in A \/ B and
A128: for i being Nat ex k being Nat st
( i <= k & r in S . k ) by A14, A125, A62, JCT_MISC:12;
reconsider r = r as Real ;
set p = |[(((W-bound C) + (E-bound C)) / 2),r]|;
A129: |[(((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 )
A130: BDD-Family C = { (Cl (BDD (L~ (Cage (C,k1))))) where k1 is 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 Nat such that
A131: Y = Cl (BDD (L~ (Cage (C,k1)))) by A130;
consider k0 being Nat such that
A132: k1 <= k0 and
A133: r in S . k0 by A128;
A134: 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;
A135: 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 A136: (dom proj2) /\ CC = CC by XBOOLE_1:28;
A137: 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 A132, JORDAN1H:48;
then RightComp (Cage (C,(k0 + 1))) c= RightComp (Cage (C,k1)) by A137;
then A138: Cl (RightComp (Cage (C,(k0 + 1)))) c= Cl (RightComp (Cage (C,k1))) by PRE_TOPC:19;
A139: E . k0 in Upper_Arc (L~ (Cage (C,(k0 + 1)))) by A34;
A140: 1 + 0 <= k0 + 1 by NAT_1:11;
A141: E . k0 in Upper_Arc (L~ (Cage (C,(k0 + 1)))) by A34;
A142: 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) ;
A143: proj2 . (E . k0) = (E . k0) `2 by PSCOMP_1:def 6;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
A144: k0 in NAT by ORDINAL1:def 12;
A145: Fs . k0 = H₃(k0) by A31, A144
.= upper_bound D ;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A146: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A147: E . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Es . k0)]| by A11, A144;
then A148: (E . k0) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
(E . k0) `2 = Es . k0 by A147, EUCLID:52
.= H₁(k0) by A10, A144
.= 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))))))) ;
then ex j being 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, A148, A142, JORDAN1F:13;
then A149: LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) meets Lower_Arc (L~ (Cage (C,(k0 + 1)))) by A2, A142, A141, JORDAN1J:62;
then DD <> {} ;
then dom proj2 meets DD by A146;
then D <> {} by RELAT_1:118;
then consider dd being Point of (TOP-REAL 2) such that
A150: dd in DD and
A151: Fs . k0 = proj2 . dd by A145, FUNCT_2:65, RCOMP_1:14;
A152: dd in LSeg ((E . k0),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A150, 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 A153: (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, A140, JORDAN1A:44, XBOOLE_1:63;
then DD <> {} ;
then dom proj2 meets DD by A153;
then A154: D <> {} by RELAT_1:118;
A155: F . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Fs . k0)]| by A32, A144;
then A156: (F . k0) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A157: (F . k0) `2 = Fs . k0 by A155, EUCLID:52
.= dd `2 by A151, PSCOMP_1:def 6 ;
E . k0 in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A148, 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 A156, A152, JORDAN6:31;
then A158: F . k0 in LSeg ((E . k0),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A152, A157, TOPREAL3:6;
Es . k0 = H<sub>1</sub>(k0) by A10, A144;
then consider dd being Point of (TOP-REAL 2) such that
A159: dd in DD and
A160: Es . k0 = proj2 . dd by A154, FUNCT_2:65, RCOMP_1:14;
A161: dd in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) by A159, XBOOLE_0:def 4;
A162: (E . k0) `2 = Es . k0 by A147, EUCLID:52
.= dd `2 by A160, PSCOMP_1:def 6 ;
then A163: ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `2 <= (E . k0) `2 by A7, A161, TOPREAL1:4;
then A164: (F . k0) `2 <= (E . k0) `2 by A152, A157, TOPREAL1:4;
r in proj2 .: (LSeg ((E . k0),(F . k0))) by A33, A133, A144;
then r in [.(proj2 . (F . k0)),(proj2 . (E . k0)).] by A143, A134, A164, SPRECT_1:53;
then A165: |[(((W-bound C) + (E-bound C)) / 2),r]| in LSeg ((E . k0),(F . k0)) by A148, A156, JORDAN1A:11;
A166: F . k0 in Lower_Arc (L~ (Cage (C,(k0 + 1)))) by A46;
A167: (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;
A168: E . k0 in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) by RLTOPSP1:68;
then A169: LSeg ((E . k0),(F . k0)) c= LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) by A158, TOPREAL1:6;
for x being object holds
( x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) iff x = F . k0 )

proof

let x be object ; :: 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, A144;
then A170: (F . k0) `2 = Fs . k0 by EUCLID:52
.= H<sub>3</sub>(k0) by A31, A144 ;
assume A171: 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) ;
A172: p in LSeg ((E . k0),(F . k0)) by A171, XBOOLE_0:def 4;
then A173: p `2 >= (F . k0) `2 by A164, TOPREAL1:4;
p in Lower_Arc (L~ (Cage (C,(k0 + 1)))) by A171, XBOOLE_0:def 4;
then p in EE by A169, A172, XBOOLE_0:def 4;
then proj2 . p in E0 by FUNCT_2:35;
then A174: p `2 in E0 by PSCOMP_1:def 6;
E0 is real-bounded by RCOMP_1:10;
then (F . k0) `2 >= p `2 by A170, A174, SEQ_4:def 1;
then A175: p `2 = (F . k0) `2 by A173, XXREAL_0:1;
p `1 = (F . k0) `1 by A148, A156, A172, GOBOARD7:5;
hence x = F . k0 by A175, TOPREAL3:6; :: thesis: verum

end;

assume A176: 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 A166, A176, XBOOLE_0:def 4; :: thesis: verum

end;

then A177: (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) = {(F . k0)} by TARSKI:def 1;
A178: for p being Real st p in W holds
p <= (E . k0) `2

proof

let p be Real; :: thesis: ( p in W implies p <= (E . k0) `2 )
assume p in W ; :: thesis: p <= (E . k0) `2
then consider x being object such that
x in dom proj2 and
A179: x in CC and
A180: p = proj2 . x by FUNCT_1:def 6;
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:4;
hence p <= (E . k0) `2 by A180, PSCOMP_1:def 6; :: thesis: verum

end;

CC <> {} by A149;
then dom proj2 meets CC by A136;
then W <> {} by RELAT_1:118;
then A181: upper_bound W <= (E . k0) `2 by A178, SEQ_4:45;
dd `1 = (E . k0) `1 by A13, A148, A161, 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 A161, A162, 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 A167, TOPREAL1:6;
then A182: 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 A158, A168, TOPREAL1:6;
for x being object holds
( x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) iff x = E . k0 )

proof

let x be object ; :: 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, A144;
then A183: (E . k0) `2 = Es . k0 by EUCLID:52
.= H<sub>1</sub>(k0) by A10, A144 ;
assume A184: 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) ;
A185: p in LSeg ((E . k0),(F . k0)) by A184, XBOOLE_0:def 4;
then A186: p `2 <= (E . k0) `2 by A164, TOPREAL1:4;
p in Upper_Arc (L~ (Cage (C,(k0 + 1)))) by A184, XBOOLE_0:def 4;
then p in DD by A182, A185, XBOOLE_0:def 4;
then proj2 . p in D by FUNCT_2:35;
then A187: p `2 in D by PSCOMP_1:def 6;
D is real-bounded by RCOMP_1:10;
then (E . k0) `2 <= p `2 by A183, A187, SEQ_4:def 2;
then A188: p `2 = (E . k0) `2 by A186, XXREAL_0:1;
p `1 = (E . k0) `1 by A148, A156, A185, GOBOARD7:5;
hence x = E . k0 by A188, TOPREAL3:6; :: thesis: verum

end;

assume A189: 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 A139, A189, XBOOLE_0:def 4; :: thesis: verum

end;

then A190: (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) = {(E . k0)} by TARSKI:def 1;
(E . k0) `2 = Es . k0 by A147, EUCLID:52
.= H<sub>1</sub>(k0) by A10, A144
.= 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))))))) ;
then consider j being Nat such that
A191: 1 <= j and
A192: j <= width (Gauge (C,(k0 + 1))) and
A193: E . k0 = (Gauge (C,(k0 + 1))) * ((X-SpanStart (C,(k0 + 1))),j) by A2, A1, A148, A142, JORDAN1F:13;
A194: (F . k0) `2 = Fs . k0 by A155, EUCLID:52
.= H₃(k0) by A31, A144
.= upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))))) ;
then consider k being Nat such that
A195: 1 <= k and
A196: k <= width (Gauge (C,(k0 + 1))) and
A197: F . k0 = (Gauge (C,(k0 + 1))) * ((X-SpanStart (C,(k0 + 1))),k) by A2, A156, A142, A191, A192, A193, A139, JORDAN1I:28;
1 <= Center (Gauge (C,(k0 + 1))) by JORDAN1B:11;
then k <= j by A142, A191, A193, A194, A196, A197, A135, A181, GOBOARD5:4;
then LSeg ((E . k0),(F . k0)) c= Cl (RightComp (Cage (C,(k0 + 1)))) by A142, A191, A192, A193, A195, A196, A197, A190, A177, Lm1;
then |[(((W-bound C) + (E-bound C)) / 2),r]| in Cl (RightComp (Cage (C,(k0 + 1)))) by A165;
then |[(((W-bound C) + (E-bound C)) / 2),r]| in Cl (RightComp (Cage (C,k1))) by A138;
hence |[(((W-bound C) + (E-bound C)) / 2),r]| in Y by A131, GOBRD14:37; :: thesis: verum

end;

then A198: |[(((W-bound C) + (E-bound C)) / 2),r]| in meet (BDD-Family C) by SETFAM_1:def 1;
A199: |[(((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, A126, JORDAN1A:11;

A200: 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 A199, 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 A127, 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 A200, A198, XBOOLE_0:def 3;
then consider n, i, j being Nat such that
A201: 1 < i and
A202: i < len (Gauge (C,n)) and
A203: 1 < j and
A204: j < width (Gauge (C,n)) and
A205: |[(((W-bound C) + (E-bound C)) / 2),r]| `1 <> ((Gauge (C,n)) * (i,j)) `1 and
A206: |[(((W-bound C) + (E-bound C)) / 2),r]| in cell ((Gauge (C,n)),i,j) and
A207: 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 A204; :: thesis: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C
A208: X-SpanStart (C,n) = Center (Gauge (C,n)) by JORDAN1B:16;
A209: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A210: X-SpanStart (C,n) <= len (Gauge (C,n)) by JORDAN1H:49;
A211: 1 <= X-SpanStart (C,n) by JORDAN1H:49, XXREAL_0:2;
n > 0 by A202, A204, A207, JORDAN1B:41;
then ((Gauge (C,n)) * ((X-SpanStart (C,n)),j)) `1 = ((W-bound C) + (E-bound C)) / 2 by A2, A5, A203, A204, A208, A9, A209, JORDAN1A:36;
hence cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C by A129, A201, A202, A203, A204, A205, A206, A207, A211, A210, JORDAN1B:22; :: thesis: verum