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

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

proof

let i be Element of NAT ; :: thesis: E . i in Upper_Arc (L~ (Cage (C,(i + 1))))
set p = E . i;
A35: i + 1 >= 1 by NAT_1:11;
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A36: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A37: X-SpanStart (C,(i + 1)) = Center (Gauge (C,(i + 1))) by JORDAN1B:16;
then LSeg (((Gauge (C,(i + 1))) * ((X-SpanStart (C,(i + 1))),1)),((Gauge (C,(i + 1))) * ((X-SpanStart (C,(i + 1))),(len (Gauge (C,(i + 1))))))) meets Upper_Arc (L~ (Cage (C,(i + 1)))) by JORDAN1B:31;
then LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) meets Upper_Arc (L~ (Cage (C,(i + 1)))) by A2, A37, A35, JORDAN1A:44, XBOOLE_1:63;
then DD <> {} by XBOOLE_0:def 7;
then dom proj2 meets DD by A36, XBOOLE_0:def 7;
then A38: D <> {} by RELAT_1:118;
Es . i = lower_bound D by A10;
then consider dd being Point of (TOP-REAL 2) such that
A39: dd in DD and
A40: Es . i = proj2 . dd by A38, FUNCT_2:65, RCOMP_1:14;
A41: dd in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A39, XBOOLE_0:def 4;
A42: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A11;
then (E . i) `2 = Es . i by EUCLID:52;
then A43: dd `2 = (E . i) `2 by A40, PSCOMP_1:def 6;
(E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by A42, EUCLID:52;
then A44: dd `1 = (E . i) `1 by A13, A41, JORDAN6:31;
dd in Upper_Arc (L~ (Cage (C,(i + 1)))) by A39, XBOOLE_0:def 4;
hence E . i in Upper_Arc (L~ (Cage (C,(i + 1)))) by A44, A43, TOPREAL3:6; :: thesis: verum

end;

A45: for i being Element of NAT holds F . i in Lower_Arc (L~ (Cage (C,(i + 1))))

proof

let i be Element of NAT ; :: thesis: F . i in Lower_Arc (L~ (Cage (C,(i + 1))))
set p = F . i;
A46: X-SpanStart (C,(i + 1)) = Center (Gauge (C,(i + 1))) by JORDAN1B:16;
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
A47: E . i in Upper_Arc (L~ (Cage (C,(i + 1)))) by A34;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A48: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A49: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A11;
then A50: (E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
then E . i in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN1A:8;
then A51: LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) c= Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A6, JORDAN1A:13;
(E . i) `2 = Es . i by A49, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) by A10 ;
then ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & E . i = (Gauge (C,(i + 1))) * ((X-SpanStart (C,(i + 1))),j) ) by A2, A1, A46, A50, JORDAN1F:13;
then LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i)) meets Lower_Arc (L~ (Cage (C,(i + 1)))) by A2, A46, A47, JORDAN1J:62;
then DD <> {} by XBOOLE_0:def 7;
then dom proj2 meets DD by A48, XBOOLE_0:def 7;
then A52: D <> {} by RELAT_1:118;
Fs . i = upper_bound D by A31;
then consider dd being Point of (TOP-REAL 2) such that
A53: dd in DD and
A54: Fs . i = proj2 . dd by A52, FUNCT_2:65, RCOMP_1:14;
A55: dd in Lower_Arc (L~ (Cage (C,(i + 1)))) by A53, XBOOLE_0:def 4;
A56: F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A32;
then (F . i) `2 = Fs . i by EUCLID:52;
then A57: dd `2 = (F . i) `2 by A54, PSCOMP_1:def 6;
A58: dd in LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A53, XBOOLE_0:def 4;
(F . i) `1 = ((W-bound C) + (E-bound C)) / 2 by A56, EUCLID:52;
then dd `1 = (F . i) `1 by A58, A51, JORDAN6:31;
hence F . i in Lower_Arc (L~ (Cage (C,(i + 1)))) by A55, A57, TOPREAL3:6; :: thesis: verum

end;

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

proof

let i be Element of NAT ; :: thesis: ( S . i is interval & S . i meets A & S . i meets B )
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
A60: X-SpanStart (C,(i + 1)) = Center (Gauge (C,(i + 1))) by JORDAN1B:16;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A61: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A62: 1 <= i + 1 by NAT_1:11;
LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),1)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(len (Gauge (C,(i + 1))))))) meets Upper_Arc (L~ (Cage (C,(i + 1)))) by JORDAN1B:31;
then LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) meets Upper_Arc (L~ (Cage (C,(i + 1)))) by A2, A62, JORDAN1A:44, XBOOLE_1:63;
then DD <> {} by XBOOLE_0:def 7;
then dom proj2 meets DD by A61, XBOOLE_0:def 7;
then A63: D <> {} by RELAT_1:118;
Es . i = lower_bound D by A10;
then consider dd being Point of (TOP-REAL 2) such that
A64: dd in DD and
A65: Es . i = proj2 . dd by A63, FUNCT_2:65, RCOMP_1:14;
A66: dd in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) by A64, XBOOLE_0:def 4;
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A67: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A68: E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A11;
then A69: (E . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A70: F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A32;
then A71: (F . i) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A72: (F . i) `2 = Fs . i by A70, EUCLID:52
.= upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))))) by A31 ;
(E . i) `2 = Es . i by A68, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) by A10 ;
then consider j being Element of NAT such that
A73: 1 <= j and
A74: j <= width (Gauge (C,(i + 1))) and
A75: E . i = (Gauge (C,(i + 1))) * ((X-SpanStart (C,(i + 1))),j) by A2, A1, A69, A60, JORDAN1F:13;
A76: E . i in Upper_Arc (L~ (Cage (C,(i + 1)))) by A34;
then consider k being Element of NAT such that
A77: 1 <= k and
A78: k <= width (Gauge (C,(i + 1))) and
A79: F . i = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k) by A2, A60, A71, A73, A74, A75, A72, JORDAN1I:28;
(E . i) `2 = Es . i by A68, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) by A10 ;
then ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & E . i = (Gauge (C,(i + 1))) * ((X-SpanStart (C,(i + 1))),j) ) by A2, A1, A69, A60, JORDAN1F:13;
then LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i)) meets Lower_Arc (L~ (Cage (C,(i + 1)))) by A2, A60, A76, JORDAN1J:62;
then DD <> {} by XBOOLE_0:def 7;
then dom proj2 meets DD by A67, XBOOLE_0:def 7;
then A80: D <> {} by RELAT_1:118;
A81: (E . i) `2 = Es . i by A68, EUCLID:52
.= dd `2 by A65, PSCOMP_1:def 6 ;
for p being real number st p in D holds
p <= (E . i) `2

proof

let p be real number ; :: thesis: ( p in D implies p <= (E . i) `2 )
assume p in D ; :: thesis: p <= (E . i) `2
then consider x being set such that
x in dom proj2 and
A82: x in DD and
A83: p = proj2 . x by FUNCT_1:def 6;
A84: ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `2 <= (E . i) `2 by A7, A66, A81, TOPREAL1:4;
reconsider x = x as Point of (TOP-REAL 2) by A82;
x in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i)) by A82, XBOOLE_0:def 4;
then x `2 <= (E . i) `2 by A84, TOPREAL1:4;
hence p <= (E . i) `2 by A83, PSCOMP_1:def 6; :: thesis: verum

end;

then A85: upper_bound D <= (E . i) `2 by A80, SEQ_4:45;
dd `1 = (E . i) `1 by A13, A69, A66, JORDAN6:31;
then A86: E . i in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A66, A81, TOPREAL3:6;
Fs . i = upper_bound D by A31;
then consider dd being Point of (TOP-REAL 2) such that
A87: dd in DD and
A88: Fs . i = proj2 . dd by A80, FUNCT_2:65, RCOMP_1:14;
A89: (F . i) `2 = Fs . i by A70, EUCLID:52
.= dd `2 by A88, PSCOMP_1:def 6 ;
A90: dd in LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A87, XBOOLE_0:def 4;
E . i in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A69, JORDAN1A:8;
then LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) c= Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A6, JORDAN1A:13;
then dd `1 = (F . i) `1 by A71, A90, JORDAN6:31;
then A91: F . i in LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A90, A89, TOPREAL3:6;
(Gauge (C,1)) * ((X-SpanStart (C,1)),1) in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by RLTOPSP1:68;
then LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i)) c= LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A86, TOPREAL1:6;
then A92: LSeg ((E . i),(F . i)) c= LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A86, A91, TOPREAL1:6;
A93: for x being set st x in (LSeg ((E . i),(F . i))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) holds
x = E . i

proof

let x be set ; :: thesis: ( x in (LSeg ((E . i),(F . i))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) implies x = E . i )
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
assume A94: x in (LSeg ((E . i),(F . i))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) ; :: thesis: x = E . i
then reconsider p = x as Point of (TOP-REAL 2) ;
A95: p in LSeg ((E . i),(F . i)) by A94, XBOOLE_0:def 4;
p in Upper_Arc (L~ (Cage (C,(i + 1)))) by A94, XBOOLE_0:def 4;
then p in DD by A92, A95, XBOOLE_0:def 4;
then proj2 . p in D by FUNCT_2:35;
then A96: p `2 in D by PSCOMP_1:def 6;
E . i = |[(((W-bound C) + (E-bound C)) / 2),(Es . i)]| by A11;
then A97: (E . i) `2 = Es . i by EUCLID:52
.= lower_bound D by A10 ;
D is real-bounded by RCOMP_1:10;
then A98: (E . i) `2 <= p `2 by A97, A96, SEQ_4:def 2;
p `2 <= (E . i) `2 by A72, A85, A95, TOPREAL1:4;
then A99: p `2 = (E . i) `2 by A98, XXREAL_0:1;
p `1 = (E . i) `1 by A69, A71, A95, GOBOARD7:5;
hence x = E . i by A99, TOPREAL3:6; :: thesis: verum

end;

A100: (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) in LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))) by RLTOPSP1:68;
A101: (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) = {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))}

proof

thus (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) c= {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} :: according to XBOOLE_0:def 10 :: thesis: {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} c= (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1)))))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) or x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} )
assume x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) ; :: thesis: x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))}
then x = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) by A60, A75, A79, A93;
hence x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} or x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) )
assume x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))} ; :: thesis: x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1)))))
then x = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) by TARSKI:def 1;
hence x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))) by A60, A76, A75, A100, XBOOLE_0:def 4; :: thesis: verum

end;

E . i in LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by RLTOPSP1:68;
then A102: LSeg ((E . i),(F . i)) c= LSeg ((E . i),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A91, TOPREAL1:6;
A103: for x being set st x in (LSeg ((E . i),(F . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) holds
x = F . i

proof

let x be set ; :: thesis: ( x in (LSeg ((E . i),(F . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) implies x = F . i )
reconsider EE = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider E0 = proj2 .: EE as compact Subset of REAL by JCT_MISC:15;
assume A104: x in (LSeg ((E . i),(F . i))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) ; :: thesis: x = F . i
then reconsider p = x as Point of (TOP-REAL 2) ;
A105: p in LSeg ((E . i),(F . i)) by A104, XBOOLE_0:def 4;
p in Lower_Arc (L~ (Cage (C,(i + 1)))) by A104, XBOOLE_0:def 4;
then p in EE by A102, A105, XBOOLE_0:def 4;
then proj2 . p in E0 by FUNCT_2:35;
then A106: p `2 in E0 by PSCOMP_1:def 6;
F . i = |[(((W-bound C) + (E-bound C)) / 2),(Fs . i)]| by A32;
then A107: (F . i) `2 = Fs . i by EUCLID:52
.= upper_bound E0 by A31 ;
E0 is real-bounded by RCOMP_1:10;
then A108: (F . i) `2 >= p `2 by A107, A106, SEQ_4:def 1;
p `2 >= (F . i) `2 by A72, A85, A105, TOPREAL1:4;
then A109: p `2 = (F . i) `2 by A108, XXREAL_0:1;
p `1 = (F . i) `1 by A69, A71, A105, GOBOARD7:5;
hence x = F . i by A109, TOPREAL3:6; :: thesis: verum

end;

A110: F . i in Lower_Arc (L~ (Cage (C,(i + 1)))) by A45;
A111: S . i = proj2 .: (LSeg ((E . i),(F . i))) by A33;
hence S . i is interval by JCT_MISC:6; :: thesis: ( S . i meets A & S . i meets B )
A112: Center (Gauge (C,(i + 1))) <= len (Gauge (C,(i + 1))) by JORDAN1B:13;
A113: (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k) in LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j))) by RLTOPSP1:68;
A114: (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) = {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))}

proof

thus (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) c= {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} :: according to XBOOLE_0:def 10 :: thesis: {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} c= (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1)))))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) or x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} )
assume x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) ; :: thesis: x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))}
then x = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k) by A60, A75, A79, A103;
hence x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} or x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) )
assume x in {((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k))} ; :: thesis: x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1)))))
then x = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k) by TARSKI:def 1;
hence x in (LSeg (((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),k)),((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j)))) /\ (Lower_Arc (L~ (Cage (C,(i + 1))))) by A79, A110, A113, XBOOLE_0:def 4; :: thesis: verum

end;

1 <= Center (Gauge (C,(i + 1))) by JORDAN1B:11;
then A115: k <= j by A60, A73, A75, A72, A78, A79, A112, A85, GOBOARD5:4;
then LSeg ((E . i),(F . i)) meets (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc C) by A60, A92, A74, A75, A77, A79, A101, A114, JORDAN1J:64, XBOOLE_1:77;
hence S . i meets A by A111, JORDAN1A:14; :: thesis: S . i meets B
LSeg ((E . i),(F . i)) meets (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Lower_Arc C) by A60, A92, A74, A75, A77, A79, A115, A101, A114, JORDAN1J:63, XBOOLE_1:77;
hence S . i meets B by A111, JORDAN1A:14; :: thesis: verum

end;

proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) = ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `2 by PSCOMP_1:def 6;
then A116: proj2 .: (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) = [.(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1))),(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))).] by A7, A8, SPRECT_1:53;
then A117: B c= [.(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1))),(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))).] by RELAT_1:123, XBOOLE_1:17;
A c= [.(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1))),(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))).] by A116, RELAT_1:123, XBOOLE_1:17;
then consider r being real number such that
A118: r in [.(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),1))),(proj2 . ((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))).] and
A119: not r in A \/ B and
A120: for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) by A14, A117, A59, JCT_MISC:12;
reconsider r = r as Real by XREAL_0:def 1;
set p = |[(((W-bound C) + (E-bound C)) / 2),r]|;
A121: |[(((W-bound C) + (E-bound C)) / 2),r]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
for Y being set st Y in BDD-Family C holds
|[(((W-bound C) + (E-bound C)) / 2),r]| in Y

proof

let Y be set ; :: thesis: ( Y in BDD-Family C implies |[(((W-bound C) + (E-bound C)) / 2),r]| in Y )
A122: BDD-Family C = { (Cl (BDD (L~ (Cage (C,k1))))) where k1 is Element of NAT : verum } by JORDAN10:def 2;
assume Y in BDD-Family C ; :: thesis: |[(((W-bound C) + (E-bound C)) / 2),r]| in Y
then consider k1 being Element of NAT such that
A123: Y = Cl (BDD (L~ (Cage (C,k1)))) by A122;
consider k0 being Element of NAT such that
A124: k1 <= k0 and
A125: r in S . k0 by A120;
A126: proj2 . (F . k0) = (F . k0) `2 by PSCOMP_1:def 6;
reconsider EE = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider CC = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider W = proj2 .: CC as compact Subset of REAL by JCT_MISC:15;
A127: Center (Gauge (C,(k0 + 1))) <= len (Gauge (C,(k0 + 1))) by JORDAN1B:13;
reconsider E0 = proj2 .: EE as compact Subset of REAL by JCT_MISC:15;
CC c= the carrier of (TOP-REAL 2) ;
then CC c= dom proj2 by FUNCT_2:def 1;
then A128: (dom proj2) /\ CC = CC by XBOOLE_1:28;
A129: RightComp (Cage (C,(k0 + 1))) c= RightComp (Cage (C,k0)) by JORDAN1H:48, NAT_1:11;
RightComp (Cage (C,k0)) c= RightComp (Cage (C,k1)) by A124, JORDAN1H:48;
then RightComp (Cage (C,(k0 + 1))) c= RightComp (Cage (C,k1)) by A129, XBOOLE_1:1;
then A130: Cl (RightComp (Cage (C,(k0 + 1)))) c= Cl (RightComp (Cage (C,k1))) by PRE_TOPC:19;
A131: E . k0 in Upper_Arc (L~ (Cage (C,(k0 + 1)))) by A34;
A132: 1 + 0 <= k0 + 1 by NAT_1:11;
A133: E . k0 in Upper_Arc (L~ (Cage (C,(k0 + 1)))) by A34;
A134: X-SpanStart (C,(k0 + 1)) = Center (Gauge (C,(k0 + 1))) by JORDAN1B:16;
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) as compact Subset of (TOP-REAL 2) ;
A135: proj2 . (E . k0) = (E . k0) `2 by PSCOMP_1:def 6;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
A136: Fs . k0 = upper_bound D by A31;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A137: (dom proj2) /\ DD = DD by XBOOLE_1:28;
A138: E . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Es . k0)]| by A11;
then A139: (E . k0) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
(E . k0) `2 = Es . k0 by A138, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))))) by A10 ;
then ex j being Element of NAT st
( 1 <= j & j <= width (Gauge (C,(k0 + 1))) & E . k0 = (Gauge (C,(k0 + 1))) * ((X-SpanStart (C,(k0 + 1))),j) ) by A2, A1, A139, A134, JORDAN1F:13;
then A140: LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) meets Lower_Arc (L~ (Cage (C,(k0 + 1)))) by A2, A134, A133, JORDAN1J:62;
then DD <> {} by XBOOLE_0:def 7;
then dom proj2 meets DD by A137, XBOOLE_0:def 7;
then D <> {} by RELAT_1:118;
then consider dd being Point of (TOP-REAL 2) such that
A141: dd in DD and
A142: Fs . k0 = proj2 . dd by A136, FUNCT_2:65, RCOMP_1:14;
A143: dd in LSeg ((E . k0),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A141, XBOOLE_0:def 4;
reconsider DD = (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) as compact Subset of (TOP-REAL 2) ;
reconsider D = proj2 .: DD as compact Subset of REAL by JCT_MISC:15;
DD c= the carrier of (TOP-REAL 2) ;
then DD c= dom proj2 by FUNCT_2:def 1;
then A144: (dom proj2) /\ DD = DD by XBOOLE_1:28;
LSeg (((Gauge (C,(k0 + 1))) * ((Center (Gauge (C,(k0 + 1)))),1)),((Gauge (C,(k0 + 1))) * ((Center (Gauge (C,(k0 + 1)))),(len (Gauge (C,(k0 + 1))))))) meets Upper_Arc (L~ (Cage (C,(k0 + 1)))) by JORDAN1B:31;
then LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) meets Upper_Arc (L~ (Cage (C,(k0 + 1)))) by A2, A132, JORDAN1A:44, XBOOLE_1:63;
then DD <> {} by XBOOLE_0:def 7;
then dom proj2 meets DD by A144, XBOOLE_0:def 7;
then A145: D <> {} by RELAT_1:118;
A146: F . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Fs . k0)]| by A32;
then A147: (F . k0) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A148: (F . k0) `2 = Fs . k0 by A146, EUCLID:52
.= dd `2 by A142, PSCOMP_1:def 6 ;
E . k0 in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A139, JORDAN1A:8;
then LSeg ((E . k0),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) c= Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A6, JORDAN1A:13;
then dd `1 = (F . k0) `1 by A147, A143, JORDAN6:31;
then A149: F . k0 in LSeg ((E . k0),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A143, A148, TOPREAL3:6;
Es . k0 = lower_bound D by A10;
then consider dd being Point of (TOP-REAL 2) such that
A150: dd in DD and
A151: Es . k0 = proj2 . dd by A145, FUNCT_2:65, RCOMP_1:14;
A152: dd in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) by A150, XBOOLE_0:def 4;
A153: (E . k0) `2 = Es . k0 by A138, EUCLID:52
.= dd `2 by A151, PSCOMP_1:def 6 ;
then A154: ((Gauge (C,1)) * ((X-SpanStart (C,1)),1)) `2 <= (E . k0) `2 by A7, A152, TOPREAL1:4;
then A155: (F . k0) `2 <= (E . k0) `2 by A143, A148, TOPREAL1:4;
r in proj2 .: (LSeg ((E . k0),(F . k0))) by A33, A125;
then r in [.(proj2 . (F . k0)),(proj2 . (E . k0)).] by A135, A126, A155, SPRECT_1:53;
then A156: |[(((W-bound C) + (E-bound C)) / 2),r]| in LSeg ((E . k0),(F . k0)) by A139, A147, JORDAN1A:11;
A157: F . k0 in Lower_Arc (L~ (Cage (C,(k0 + 1)))) by A45;
A158: (Gauge (C,1)) * ((X-SpanStart (C,1)),1) in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) by RLTOPSP1:68;
A159: E . k0 in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) by RLTOPSP1:68;
then A160: LSeg ((E . k0),(F . k0)) c= LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) by A149, TOPREAL1:6;
for x being set holds
( x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) iff x = F . k0 )

proof

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

proof

F . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Fs . k0)]| by A32;
then A161: (F . k0) `2 = Fs . k0 by EUCLID:52
.= upper_bound E0 by A31 ;
assume A162: x in (LSeg ((E . k0),(F . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))) ; :: thesis: x = F . k0
then reconsider p = x as Point of (TOP-REAL 2) ;
A163: p in LSeg ((E . k0),(F . k0)) by A162, XBOOLE_0:def 4;
then A164: p `2 >= (F . k0) `2 by A155, TOPREAL1:4;
p in Lower_Arc (L~ (Cage (C,(k0 + 1)))) by A162, XBOOLE_0:def 4;
then p in EE by A160, A163, XBOOLE_0:def 4;
then proj2 . p in E0 by FUNCT_2:35;
then A165: p `2 in E0 by PSCOMP_1:def 6;
E0 is real-bounded by RCOMP_1:10;
then (F . k0) `2 >= p `2 by A161, A165, SEQ_4:def 1;
then A166: p `2 = (F . k0) `2 by A164, XXREAL_0:1;
p `1 = (F . k0) `1 by A139, A147, A163, GOBOARD7:5;
hence x = F . k0 by A166, TOPREAL3:6; :: thesis: verum

end;

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

end;

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

proof

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

end;

CC <> {} by A140, XBOOLE_0:def 7;
then dom proj2 meets CC by A128, XBOOLE_0:def 7;
then W <> {} by RELAT_1:118;
then A172: upper_bound W <= (E . k0) `2 by A169, SEQ_4:45;
dd `1 = (E . k0) `1 by A13, A139, A152, JORDAN6:31;
then E . k0 in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1)))))) by A152, A153, TOPREAL3:6;
then LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0)) c= LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A158, TOPREAL1:6;
then A173: LSeg ((E . k0),(F . k0)) c= LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A149, A159, TOPREAL1:6;
for x being set holds
( x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) iff x = E . k0 )

proof

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

proof

E . k0 = |[(((W-bound C) + (E-bound C)) / 2),(Es . k0)]| by A11;
then A174: (E . k0) `2 = Es . k0 by EUCLID:52
.= lower_bound D by A10 ;
assume A175: x in (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) ; :: thesis: x = E . k0
then reconsider p = x as Point of (TOP-REAL 2) ;
A176: p in LSeg ((E . k0),(F . k0)) by A175, XBOOLE_0:def 4;
then A177: p `2 <= (E . k0) `2 by A155, TOPREAL1:4;
p in Upper_Arc (L~ (Cage (C,(k0 + 1)))) by A175, XBOOLE_0:def 4;
then p in DD by A173, A176, XBOOLE_0:def 4;
then proj2 . p in D by FUNCT_2:35;
then A178: p `2 in D by PSCOMP_1:def 6;
D is real-bounded by RCOMP_1:10;
then (E . k0) `2 <= p `2 by A174, A178, SEQ_4:def 2;
then A179: p `2 = (E . k0) `2 by A177, XXREAL_0:1;
p `1 = (E . k0) `1 by A139, A147, A176, GOBOARD7:5;
hence x = E . k0 by A179, TOPREAL3:6; :: thesis: verum

end;

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

end;

then A181: (LSeg ((E . k0),(F . k0))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))) = {(E . k0)} by TARSKI:def 1;
(E . k0) `2 = Es . k0 by A138, EUCLID:52
.= lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(k0 + 1))))))) by A10 ;
then consider j being Element of NAT such that
A182: 1 <= j and
A183: j <= width (Gauge (C,(k0 + 1))) and
A184: E . k0 = (Gauge (C,(k0 + 1))) * ((X-SpanStart (C,(k0 + 1))),j) by A2, A1, A139, A134, JORDAN1F:13;
A185: (F . k0) `2 = Fs . k0 by A146, EUCLID:52
.= upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),1)),(E . k0))) /\ (Lower_Arc (L~ (Cage (C,(k0 + 1))))))) by A31 ;
then consider k being Element of NAT such that
A186: 1 <= k and
A187: k <= width (Gauge (C,(k0 + 1))) and
A188: F . k0 = (Gauge (C,(k0 + 1))) * ((X-SpanStart (C,(k0 + 1))),k) by A2, A147, A134, A182, A183, A184, A131, JORDAN1I:28;
1 <= Center (Gauge (C,(k0 + 1))) by JORDAN1B:11;
then k <= j by A134, A182, A184, A185, A187, A188, A127, A172, GOBOARD5:4;
then LSeg ((E . k0),(F . k0)) c= Cl (RightComp (Cage (C,(k0 + 1)))) by A134, A182, A183, A184, A186, A187, A188, A181, A168, Lm1;
then |[(((W-bound C) + (E-bound C)) / 2),r]| in Cl (RightComp (Cage (C,(k0 + 1)))) by A156;
then |[(((W-bound C) + (E-bound C)) / 2),r]| in Cl (RightComp (Cage (C,k1))) by A130;
hence |[(((W-bound C) + (E-bound C)) / 2),r]| in Y by A123, GOBRD14:37; :: thesis: verum

end;

then A189: |[(((W-bound C) + (E-bound C)) / 2),r]| in meet (BDD-Family C) by SETFAM_1:def 1;
A190: |[(((W-bound C) + (E-bound C)) / 2),r]| in LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1))) by A5, A12, A118, JORDAN1A:11;

A191: now :: thesis: not |[(((W-bound C) + (E-bound C)) / 2),r]| in C

assume |[(((W-bound C) + (E-bound C)) / 2),r]| in C ; :: thesis: contradiction
then |[(((W-bound C) + (E-bound C)) / 2),r]| in (Lower_Arc C) \/ (Upper_Arc C) by JORDAN6:50;
then |[(((W-bound C) + (E-bound C)) / 2),r]| in ((Lower_Arc C) \/ (Upper_Arc C)) /\ (LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) by A190, XBOOLE_0:def 4;
then |[(((W-bound C) + (E-bound C)) / 2),r]| in ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc C)) \/ ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Lower_Arc C)) by XBOOLE_1:23;
then proj2 . |[(((W-bound C) + (E-bound C)) / 2),r]| in proj2 .: (((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc C)) \/ ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Lower_Arc C))) by FUNCT_2:35;
then r in proj2 .: (((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Upper_Arc C)) \/ ((LSeg (((Gauge (C,1)) * ((X-SpanStart (C,1)),(len (Gauge (C,1))))),((Gauge (C,1)) * ((X-SpanStart (C,1)),1)))) /\ (Lower_Arc C))) by PSCOMP_1:65;
hence contradiction by A119, RELAT_1:120; :: thesis: verum

end;

meet (BDD-Family C) = C \/ (BDD C) by JORDAN10:21;
then |[(((W-bound C) + (E-bound C)) / 2),r]| in BDD C by A191, A189, XBOOLE_0:def 3;
then consider n, i, j being Element of NAT such that
A192: 1 < i and
A193: i < len (Gauge (C,n)) and
A194: 1 < j and
A195: j < width (Gauge (C,n)) and
A196: |[(((W-bound C) + (E-bound C)) / 2),r]| `1 <> ((Gauge (C,n)) * (i,j)) `1 and
A197: |[(((W-bound C) + (E-bound C)) / 2),r]| in cell ((Gauge (C,n)),i,j) and
A198: cell ((Gauge (C,n)),i,j) c= BDD C by JORDAN1C:23;
take n ; :: thesis: n is_sufficiently_large_for C
take j ; :: according to JORDAN1H:def 3 :: thesis: ( not width (Gauge (C,n)) <= j & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C )
thus j < width (Gauge (C,n)) by A195; :: thesis: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C
A199: X-SpanStart (C,n) = Center (Gauge (C,n)) by JORDAN1B:16;
A200: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A201: X-SpanStart (C,n) <= len (Gauge (C,n)) by JORDAN1H:49;
A202: 1 <= X-SpanStart (C,n) by JORDAN1H:49, XXREAL_0:2;
n > 0 by A193, A195, A198, JORDAN1B:41;
then ((Gauge (C,n)) * ((X-SpanStart (C,n)),j)) `1 = ((W-bound C) + (E-bound C)) / 2 by A2, A5, A194, A195, A199, A9, A200, JORDAN1A:36;
hence cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C by A121, A192, A193, A194, A195, A196, A197, A198, A202, A201, JORDAN1B:22; :: thesis: verum