let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: ex n being Element of NAT st n is_sufficiently_large_for C
set s = ((W-bound C) + (E-bound C)) / 2;
set e = (Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))));
set f = (Gauge (C,1)) * ((X-SpanStart (C,1)),1);
A1: len (Gauge (C,1)) = width (Gauge (C,1)) by JORDAN8:def 1;
A2: X-SpanStart (C,1) = Center (Gauge (C,1)) by JORDAN1B:16;
then X-SpanStart (C,1) = ((len (Gauge (C,1))) div 2) + 1 by JORDAN1A:def 1;
then A3: 1 <= X-SpanStart (C,1) by NAT_1:11;
len (Gauge (C,1)) >= 4 by JORDAN8:10;
then A4: 1 < len (Gauge (C,1)) by XXREAL_0:2;
then A5: ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `1 = ((W-bound C) + (E-bound C)) / 2 by A2, JORDAN1A:38;
then A6: (Gauge (C,1)) * ((X-SpanStart (C,1)),1) in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN1A:8;
0 < len (Gauge (C,1)) by JORDAN8:10;
then (len (Gauge (C,1))) div 2 < len (Gauge (C,1)) by INT_1:56;
then ((len (Gauge (C,1))) div 2) + 1 <= len (Gauge (C,1)) by NAT_1:13;
then X-SpanStart (C,1) <= len (Gauge (C,1)) by A2, JORDAN1A:def 1;
then A7: ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `2 < ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))) `2 by A3, A4, A1, GOBOARD5:4;
set e1 = proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))));
set f1 = proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1));
A8: proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))) = ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))) `2 by PSCOMP_1:def 6;
4 <= len (Gauge (C,1)) by JORDAN8:10;
then A9: 1 <= len (Gauge (C,1)) by XXREAL_0:2;
set AA = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc C);
set BB = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Lower_Arc C);
deffunc 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();
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 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: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 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:13;
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:65;
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:65;
A23: p `2 = proj2 . q by A19, A22, PSCOMP_1:def 6
.= q `2 by PSCOMP_1:def 6 ;
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:31
.= q `1 by A14, A25, JORDAN6:31 ;
then p = q by A23, TOPREAL3:6;
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:50;

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:52;
(W-min C) `1 = ((W-bound C) + (E-bound C)) / 2 by A14, A26, A28, JORDAN6:31;
hence contradiction by A29, SPRECT_1:31; :: thesis: verum

end;

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

A31: (E-max C) `1 = E-bound C by EUCLID:52;
(E-max C) `1 = ((W-bound C) + (E-bound C)) / 2 by A14, A26, A30, JORDAN6:31;
hence contradiction by A31, SPRECT_1:31; :: 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) ;
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 A37: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A38: 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, A38, A36, JORDAN1A:44, 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:118;
Es . i = lower_bound 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: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 A12;
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 A14, 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 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: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 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:52;
then E . i in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN1A:8;
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:13;
(E . i) `2 = Es . i by A50, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) by A10 ;
then ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & E . i = (Gauge (C,(i + 1))) * ((X-SpanStart (C,(i + 1))),j) ) by A2, A1, 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:118;
Fs . i = upper_bound 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:65, RCOMP_1:14;
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:52;
then A58: dd `2 = (F . i) `2 by A55, PSCOMP_1:def 6;
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:52;
then dd `1 = (F . i) `1 by A59, A52, JORDAN6:31;
hence F . i in Lower_Arc (L~ (Cage (C,(i + 1)))) by A56, A58, TOPREAL3:6; :: thesis: verum

end;

A60: for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B )

proof

let i be Element of NAT ; :: thesis: ( S . i is interval & S . i meets A & S . i meets B )
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
A61: 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 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: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, A63, JORDAN1A:44, 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:118;
Es . i = lower_bound 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:65, RCOMP_1:14;
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) ;
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 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:52;
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:52;
A73: (F . i) `2 = Fs . i by A71, EUCLID:52
.= upper_bound (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:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) by A10 ;
then consider j being Element of NAT such that
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:28;
(E . i) `2 = Es . i by A69, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) by A10 ;
then ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & E . i = (Gauge (C,(i + 1))) * ((X-SpanStart (C,(i + 1))),j) ) by A2, A1, 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:118;
A82: (E . i) `2 = Es . i by A69, EUCLID:52
.= dd `2 by A66, PSCOMP_1:def 6 ;
for p being real number st p in D holds
p <= (E . i) `2

proof

let p be real number ; :: thesis: ( p in D implies p <= (E . i) `2 )
assume p in D ; :: thesis: p <= (E . i) `2
then consider x being set such that
x in dom proj2 and
A83: x in DD and
A84: p = proj2 . x by FUNCT_1:def 6;
A85: ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `2 <= (E . i) `2 by A7, A67, A82, TOPREAL1:4;
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:4;
hence p <= (E . i) `2 by A84, PSCOMP_1:def 6; :: thesis: verum

end;

then A86: upper_bound D <= (E . i) `2 by A81, SEQ_4:45;
dd `1 = (E . i) `1 by A14, A70, A67, JORDAN6:31;
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:6;
Fs . i = upper_bound 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:65, RCOMP_1:14;
A90: (F . i) `2 = Fs . i by A71, EUCLID:52
.= dd `2 by A89, PSCOMP_1:def 6 ;
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: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 A72, A91, JORDAN6:31;
then A92: F . i in LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A91, A90, 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 A87, TOPREAL1:6;
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:6;
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) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
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:35;
then A97: p `2 in D by PSCOMP_1:def 6;
E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A12;
then A98: (E . i) `2 = Es . i by EUCLID:52
.= lower_bound D by A10 ;
D is bounded by RCOMP_1:10;
then A99: (E . i) `2 <= p `2 by A98, A97, SEQ_4:def 2;
p `2 <= (E . i) `2 by A73, A86, A96, TOPREAL1:4;
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:6; :: 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:68;
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:68;
then A103: LSeg ((E . i),(F . i)) c= LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A92, TOPREAL1:6;
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) ;
reconsider E0 = proj2 .: EE as compact Subset of REAL by JCT_MISC:15;
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:35;
then A107: p `2 in E0 by PSCOMP_1:def 6;
F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A33;
then A108: (F . i) `2 = Fs . i by EUCLID:52
.= upper_bound E0 by A32 ;
E0 is bounded by RCOMP_1:10;
then A109: (F . i) `2 >= p `2 by A108, A107, SEQ_4:def 1;
p `2 >= (F . i) `2 by A73, A86, A106, TOPREAL1:4;
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:6; :: 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 interval by JCT_MISC:6; :: thesis: ( S . i meets A & S . i meets B )
A113: Center (Gauge (C,(i + 1))) <= len (Gauge (C,(i + 1))) by JORDAN1B:13;
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:68;
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:11;
then A116: k <= j by A61, A74, A76, A73, A79, A80, A113, A86, 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 A61, A93, A75, A76, A78, A80, A102, A115, JORDAN1J:64, XBOOLE_1:77;
hence S . i meets A by A112, 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 A61, A93, A75, A76, A78, A80, A116, A102, A115, JORDAN1J:63, XBOOLE_1:77;
hence S . i meets B by A112, 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 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:53;
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: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 A117, RELAT_1:123, 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:12;
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: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 )
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 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;
A128: 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 A129: (dom proj2) /\ CC = CC by XBOOLE_1:28;
A130: 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 A125, JORDAN1H:48;
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:19;
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: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) ;
A136: proj2 . (E . k0) = (E . k0) `2 by PSCOMP_1:def 6;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
A137: Fs . k0 = upper_bound 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:52;
(E . k0) `2 = Es . k0 by A139, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))))) by A10 ;
then ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(k0 + 1))) & E . k0 = (Gauge (C,(k0 + 1))) * ((X-SpanStart (C,(k0 + 1))),j) ) by A2, A1, 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:118;
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:65, RCOMP_1:14;
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) ;
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 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: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, A133, JORDAN1A:44, 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:118;
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:52;
A149: (F . k0) `2 = Fs . k0 by A147, EUCLID:52
.= dd `2 by A143, PSCOMP_1:def 6 ;
E . k0 in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A140, 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 A148, A144, JORDAN6:31;
then A150: F . k0 in LSeg ((E . k0),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A144, A149, TOPREAL3:6;
Es . k0 = lower_bound 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:65, RCOMP_1:14;
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:52
.= dd `2 by A152, PSCOMP_1:def 6 ;
then A155: ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `2 <= (E . k0) `2 by A7, A153, TOPREAL1:4;
then A156: (F . k0) `2 <= (E . k0) `2 by A144, A149, TOPREAL1:4;
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:53;
then A157: |[(((W-bound C) + (E-bound C)) / 2),r]| in LSeg ((E . k0),(F . k0)) by A140, A148, JORDAN1A:11;
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:68;
A160: E . k0 in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) by RLTOPSP1:68;
then A161: LSeg ((E . k0),(F . k0)) c= LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) by A150, TOPREAL1:6;
for x being set holds
( x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) iff x = F . k0 )

proof

let x be set ; :: thesis: ( x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) iff x = F . k0 )
thus ( x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) implies x = F . k0 ) :: thesis: ( x = F . k0 implies x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) )

proof

F . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Fs . k0)]| by A33;
then A162: (F . k0) `2 = Fs . k0 by EUCLID:52
.= upper_bound 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:4;
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:35;
then A166: p `2 in E0 by PSCOMP_1:def 6;
E0 is bounded by RCOMP_1:10;
then (F . k0) `2 >= p `2 by A162, A166, SEQ_4:def 1;
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:6; :: 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:68;
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 6;
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:4;
hence p <= (E . k0) `2 by A172, PSCOMP_1:def 6; :: 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:118;
then A173: upper_bound W <= (E . k0) `2 by A170, SEQ_4:45;
dd `1 = (E . k0) `1 by A14, A140, A153, 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 A153, A154, 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 A159, TOPREAL1:6;
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:6;
for x being set holds
( x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) iff x = E . k0 )

proof

let x be set ; :: thesis: ( x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) iff x = E . k0 )
thus ( x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) implies x = E . k0 ) :: thesis: ( x = E . k0 implies x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) )

proof

E . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Es . k0)]| by A12;
then A175: (E . k0) `2 = Es . k0 by EUCLID:52
.= lower_bound 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:4;
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:35;
then A179: p `2 in D by PSCOMP_1:def 6;
D is bounded by RCOMP_1:10;
then (E . k0) `2 <= p `2 by A175, A179, SEQ_4:def 2;
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:6; :: 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:68;
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:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))))) by A10 ;
then consider j being Element of NAT such that
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:52
.= upper_bound (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:28;
1 <= Center (Gauge (C,(k0 + 1))) by JORDAN1B:11;
then k <= j by A135, A183, A185, A186, A188, A189, A128, A173, GOBOARD5:4;
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:37; :: 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:11;

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: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 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: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 A120, 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 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: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 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:16;
A201: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A202: X-SpanStart (C,n) <= len (Gauge (C,n)) by JORDAN1H:49;
A203: 1 <= X-SpanStart (C,n) by JORDAN1H:49, XXREAL_0:2;
n > 0 by A194, A196, A199, JORDAN1B:41;
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:36;
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:22; :: thesis: verum