let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
let e be Real; :: thesis:
assume that
A1: P is being_simple_closed_curve and
A2: e > 0 ; :: thesis:
A3: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, JORDAN6:def 8;
then consider g1 being Function of I[01],(TOP-REAL 2) such that
A4: ( g1 is continuous & g1 is one-to-one ) and
A5: rng g1 = Upper_Arc P and
A6: g1 . 0 = W-min P and
A7: g1 . 1 = E-max P by Th17;
consider h1 being FinSequence of REAL such that
A8: h1 . 1 = 0 and
A9: h1 . (len h1) = 1 and
A10: 5 <= len h1 and
A11: rng h1 c= the carrier of I[01] and
A12: h1 is increasing and
A13: for i being Nat
for Q being Subset of I[01]
for W being Subset of (Euclid 2) st 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g1 .: Q holds
diameter W < e by A2, A4, UNIFORM1:13;
h1 is FinSequence of the carrier of I[01] by A11, FINSEQ_1:def 4;
then reconsider h11 = g1 * h1 as FinSequence of the carrier of (TOP-REAL 2) by FINSEQ_2:32;
A14: 2 < len h1 by A10, XXREAL_0:2;
then A15: 2 in dom h1 by FINSEQ_3:25;
A16: 1 <= len h1 by A10, XXREAL_0:2;
then A17: 1 in dom h1 by FINSEQ_3:25;
A18: 1 + 1 in dom h1 by A14, FINSEQ_3:25;
then A19: h1 . (1 + 1) in rng h1 by FUNCT_1:def 3;
A20: h11 is one-to-one by A4, A12;
A21: Lower_Arc P is_an_arc_of E-max P, W-min P by A1, JORDAN6:def 9;
then consider g2 being Function of I[01],(TOP-REAL 2) such that
A22: ( g2 is continuous & g2 is one-to-one ) and
A23: rng g2 = Lower_Arc P and
A24: g2 . 0 = E-max P and
A25: g2 . 1 = W-min P by Th17;
consider h2 being FinSequence of REAL such that
A26: h2 . 1 = 0 and
A27: h2 . (len h2) = 1 and
A28: 5 <= len h2 and
A29: rng h2 c= the carrier of I[01] and
A30: h2 is increasing and
A31: for i being Nat
for Q being Subset of I[01]
for W being Subset of (Euclid 2) st 1 <= i & i < len h2 & Q = [.(h2 /. i),(h2 /. (i + 1)).] & W = g2 .: Q holds
diameter W < e by A2, A22, UNIFORM1:13;
h2 is FinSequence of the carrier of I[01] by A29, FINSEQ_1:def 4;
then reconsider h21 = g2 * h2 as FinSequence of the carrier of (TOP-REAL 2) by FINSEQ_2:32;
A32: h21 is one-to-one by A22, A30;
A33: 1 <= len h2 by A28, XXREAL_0:2;
then A34: len h2 in dom h2 by FINSEQ_3:25;
then A35: h21 . (len h2) = W-min P by A25, A27, FUNCT_1:13;
reconsider h0 = h11 ^ (mid (h21,2,((len h21) -' 1))) as FinSequence of the carrier of (TOP-REAL 2) ;
A36: len h0 = (len h11) + (len (mid (h21,2,((len h21) -' 1)))) by FINSEQ_1:22;
set i = (len h0) -' 1;
take h0 ; :: thesis:
A37: rng h1 c= dom g1 by A11, FUNCT_2:def 1;
then A38: dom h1 = dom h11 by RELAT_1:27;
then A39: len h1 = len h11 by FINSEQ_3:29;
then A40: h0 . 2 = h11 . 2 by A14, FINSEQ_1:64;
A41: h0 . (1 + 1) = h11 . (1 + 1) by A39, A14, FINSEQ_1:64;
then A42: h0 . (1 + 1) = g1 . (h1 . (1 + 1)) by A18, FUNCT_1:13;
set k = (((len h0) -' (len h11)) + 2) -' 1;
0 + 2 <= ((len h0) -' (len h11)) + 2 by XREAL_1:6;
then A43: 2 -' 1 <= (((len h0) -' (len h11)) + 2) -' 1 by NAT_D:42;
A44: 0 in dom g1 by Lm5, BORSUK_1:40, FUNCT_2:def 1;
A45: len h1 in dom h1 by A16, FINSEQ_3:25;
dom g2 = the carrier of I[01] by FUNCT_2:def 1;
then A46: dom h2 = dom h21 by A29, RELAT_1:27;
then A47: len h2 = len h21 by FINSEQ_3:29;
then A48: 2 <= len h21 by A28, XXREAL_0:2;
len h21 <= (len h21) + 1 by NAT_1:12;
then A49: (len h21) - 1 <= ((len h21) + 1) - 1 by XREAL_1:9;
then A50: (len h21) -' 1 <= len h21 by A28, A47, XREAL_0:def 2;
2 <= len h21 by A28, A47, XXREAL_0:2;
then A51: (1 + 1) - 1 <= (len h21) - 1 by XREAL_1:9;
then A52: (len h21) -' 1 = (len h21) - 1 by XREAL_0:def 2;
3 < len h21 by A28, A47, XXREAL_0:2;
then A53: (2 + 1) - 1 < (len h21) - 1 by XREAL_1:9;
then A54: 2 < (len h21) -' 1 by A51, NAT_D:39;
then A55: ((len h21) -' 1) -' 2 = ((len h21) -' 1) - 2 by XREAL_1:233;
A56: 1 <= (len h21) -' 1 by A51, XREAL_0:def 2;
then A57: len (mid (h21,2,((len h21) -' 1))) = (((len h21) -' 1) -' 2) + 1 by A48, A50, A54, FINSEQ_6:118;
(3 + 2) - 2 <= (len h2) - 2 by A28, XREAL_1:9;
then A58: 5 + 3 <= (len h1) + ((len h2) - 2) by A10, XREAL_1:7;
then A59: len h0 > (1 + 1) + 1 by A39, A47, A36, A52, A55, A57, XXREAL_0:2;
then A60: (len h0) -' 1 > 1 + 1 by Lm2;
then A61: 1 < (len h0) -' 1 by XXREAL_0:2;
A62: (3 + 2) - 2 <= (len h2) - 2 by A28, XREAL_1:9;
then A63: 1 <= (len h2) - 2 by XXREAL_0:2;
then A64: (len h1) + 1 <= len h0 by A39, A47, A36, A52, A55, A57, XREAL_1:7;
then A65: len h0 > len h1 by NAT_1:13;
then A66: 1 < len h0 by A16, XXREAL_0:2;
then A67: 1 in dom h0 by FINSEQ_3:25;
then A68: h0 /. 1 = h0 . 1 by PARTFUN1:def 6;
A69: dom g1 = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then A70: 1 in dom (g1 * h1) by A8, A17, Lm5, FUNCT_1:11;
then A71: h11 . 1 = W-min P by A6, A8, FUNCT_1:12;
hence A72: h0 . 1 = W-min P by A70, FINSEQ_1:def 7; :: thesis:
then A73: h0 /. 1 = W-min P by A67, PARTFUN1:def 6;
A74: len h0 in dom h0 by A66, FINSEQ_3:25;
then A75: h0 /. (len h0) = h0 . (len h0) by PARTFUN1:def 6;
A76: 1 in dom h2 by A33, FINSEQ_3:25;
then A77: h21 . 1 = E-max P by A24, A26, FUNCT_1:13;
thus A78: h0 is one-to-one :: thesis:

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A79: x in dom h0 and
A80: y in dom h0 and
A81: h0 . x = h0 . y ; :: thesis:
reconsider nx = x, ny = y as Nat by A79, A80;
A82: 1 <= nx by A79, FINSEQ_3:25;
A83: nx <= len h0 by A79, FINSEQ_3:25;
A84: 1 <= ny by A80, FINSEQ_3:25;
A85: ny <= len h0 by A80, FINSEQ_3:25;

per cases ;

suppose nx <= len h1 ; :: thesis:

then A86: nx in dom h1 by A82, FINSEQ_3:25;
then A87: h1 . nx in rng h1 by FUNCT_1:def 3;
A88: h0 . nx = h11 . nx by A38, A86, FINSEQ_1:def 7
.= g1 . (h1 . nx) by A38, A86, FUNCT_1:12 ;
then A89: h0 . nx in Upper_Arc P by A5, A37, A87, FUNCT_1:def 3;

per cases ;

suppose ny <= len h1 ; :: thesis:

then A90: ny in dom h1 by A84, FINSEQ_3:25;
then A91: h1 . ny in rng h1 by FUNCT_1:def 3;
h0 . ny = h11 . ny by A38, A90, FINSEQ_1:def 7
.= g1 . (h1 . ny) by A90, FUNCT_1:13 ;
then h1 . nx = h1 . ny by A4, A37, A81, A87, A88, A91;
hence x = y by A12, A86, A90, FUNCT_1:def 4; :: thesis:

end;

suppose A92: ny > len h1 ; :: thesis:

A93: 0 + 2 <= (ny -' (len h11)) + 2 by XREAL_1:6;
then A94: 1 <= ((ny -' (len h11)) + 2) -' 1 by Lm1, NAT_D:42;
(len h1) + 1 <= ny by A92, NAT_1:13;
then A95: ((len h1) + 1) - (len h1) <= ny - (len h1) by XREAL_1:9;
then 1 <= ny -' (len h11) by A39, A92, XREAL_1:233;
then 1 + 1 <= (((ny -' (len h11)) + 1) + 1) - 1 by XREAL_1:6;
then A96: 2 <= ((ny -' (len h11)) + 2) -' 1 by A93, Lm1, NAT_D:39, NAT_D:42;
A97: ny - (len h11) = ny -' (len h11) by A39, A92, XREAL_1:233;
ny - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A39, A47, A36, A52, A55, A57, A85, XREAL_1:9;
then A98: (ny -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A97, XREAL_1:6;
then ((ny -' (len h11)) + 2) -' 1 <= len h21 by A47, NAT_D:44;
then A99: ((ny -' (len h11)) + 2) -' 1 in dom h21 by A94, FINSEQ_3:25;
((ny -' (len h11)) + 2) - 1 <= (len h2) - 1 by A98, XREAL_1:9;
then A100: ((ny -' (len h11)) + 2) -' 1 <= (len h2) - 1 by A93, Lm1, NAT_D:39, NAT_D:42;
A101: ny <= (len h11) + (len (mid (h21,2,((len h21) -' 1)))) by A85, FINSEQ_1:22;
then A102: ny - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by XREAL_1:9;
(len h11) + 1 <= ny by A39, A92, NAT_1:13;
then A103: h0 . ny = (mid (h21,2,((len h21) -' 1))) . (ny - (len h11)) by A101, FINSEQ_1:23;
then A104: h0 . ny = h21 . (((ny -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A97, A102, A95, FINSEQ_6:118;
then h0 . ny in rng h21 by A99, FUNCT_1:def 3;
then h0 . ny in rng g2 by FUNCT_1:14;
then h0 . nx in (Upper_Arc P) /\ (Lower_Arc P) by A23, A81, A89, XBOOLE_0:def 4;
then A105: h0 . nx in {(W-min P),(E-max P)} by A1, JORDAN6:50;

per cases by A105, TARSKI:def 2;

suppose h0 . nx = W-min P ; :: thesis:

then h21 . (((ny -' (len h11)) + 2) -' 1) = W-min P by A39, A48, A56, A50, A54, A81, A103, A97, A102, A95, FINSEQ_6:118;
then len h21 = ((ny -' (len h11)) + 2) -' 1 by A46, A47, A34, A35, A32, A99;
then (len h21) + 1 <= ((len h21) - 1) + 1 by A47, A100, XREAL_1:6;
then ((len h21) + 1) - (len h21) <= (len h21) - (len h21) by XREAL_1:9;
then ((len h21) + 1) - (len h21) <= 0 ;
hence x = y ; :: thesis:

end;

suppose h0 . nx = E-max P ; :: thesis:

then 1 = ((ny -' (len h11)) + 2) -' 1 by A46, A76, A77, A32, A81, A104, A99;
hence x = y by A96; :: thesis:

end;

suppose A106: nx > len h1 ; :: thesis:

then (len h1) + 1 <= nx by NAT_1:13;
then A107: ((len h1) + 1) - (len h1) <= nx - (len h1) by XREAL_1:9;
then 1 <= nx -' (len h11) by A39, A106, XREAL_1:233;
then A108: 1 + 1 <= (((nx -' (len h11)) + 1) + 1) - 1 by XREAL_1:6;
A109: nx <= (len h11) + (len (mid (h21,2,((len h21) -' 1)))) by A83, FINSEQ_1:22;
then A110: nx - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by XREAL_1:9;
A111: nx - (len h11) = nx -' (len h11) by A39, A106, XREAL_1:233;
nx - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A39, A47, A36, A52, A55, A57, A83, XREAL_1:9;
then A112: (nx -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A111, XREAL_1:6;
then A113: ((nx -' (len h11)) + 2) - 1 <= (len h2) - 1 by XREAL_1:9;
A114: ((nx -' (len h11)) + 2) -' 1 <= len h21 by A47, A112, NAT_D:44;
A115: 0 + 2 <= (nx -' (len h11)) + 2 by XREAL_1:6;
then 1 <= ((nx -' (len h11)) + 2) -' 1 by Lm1, NAT_D:42;
then A116: ((nx -' (len h11)) + 2) -' 1 in dom h21 by A114, FINSEQ_3:25;
(len h11) + 1 <= nx by A39, A106, NAT_1:13;
then A117: h0 . nx = (mid (h21,2,((len h21) -' 1))) . (nx - (len h11)) by A109, FINSEQ_1:23;
then A118: h0 . nx = h21 . (((nx -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A111, A110, A107, FINSEQ_6:118;
then h0 . nx in rng h21 by A116, FUNCT_1:def 3;
then A119: h0 . nx in Lower_Arc P by A23, FUNCT_1:14;

per cases ;

suppose ny <= len h1 ; :: thesis:

then A120: ny in dom h1 by A84, FINSEQ_3:25;
then A121: h1 . ny in rng h1 by FUNCT_1:def 3;
h0 . ny = h11 . ny by A38, A120, FINSEQ_1:def 7
.= g1 . (h1 . ny) by A38, A120, FUNCT_1:12 ;
then h0 . ny in rng g1 by A37, A121, FUNCT_1:def 3;
then h0 . ny in (Upper_Arc P) /\ (Lower_Arc P) by A5, A81, A119, XBOOLE_0:def 4;
then A122: h0 . ny in {(W-min P),(E-max P)} by A1, JORDAN6:50;
A123: ((nx -' (len h11)) + 2) -' 1 <= (len h2) - 1 by A115, A113, Lm1, NAT_D:39, NAT_D:42;
A124: 2 <= ((nx -' (len h11)) + 2) -' 1 by A108, A115, Lm1, NAT_D:39, NAT_D:42;

per cases by A122, TARSKI:def 2;

suppose h0 . ny = W-min P ; :: thesis:

then len h21 = ((nx -' (len h11)) + 2) -' 1 by A46, A47, A34, A35, A32, A81, A118, A116;
then (len h21) + 1 <= ((len h21) - 1) + 1 by A47, A123, XREAL_1:6;
then ((len h21) + 1) - (len h21) <= (len h21) - (len h21) by XREAL_1:9;
then ((len h21) + 1) - (len h21) <= 0 ;
hence x = y ; :: thesis:

end;

suppose h0 . ny = E-max P ; :: thesis:

then h21 . (((nx -' (len h11)) + 2) -' 1) = E-max P by A39, A48, A56, A50, A54, A81, A117, A111, A110, A107, FINSEQ_6:118;
then 1 = ((nx -' (len h11)) + 2) -' 1 by A46, A76, A77, A32, A116;
hence x = y by A124; :: thesis:

end;

suppose A125: ny > len h1 ; :: thesis:

then A126: ny - (len h11) = ny -' (len h11) by A39, XREAL_1:233;
(len h1) + 1 <= ny by A125, NAT_1:13;
then A127: ( h0 . ny = (mid (h21,2,((len h21) -' 1))) . (ny - (len h11)) & ((len h1) + 1) - (len h1) <= ny - (len h1) ) by A39, A36, A85, FINSEQ_1:23, XREAL_1:9;
0 + 2 <= (ny -' (len h11)) + 2 by XREAL_1:6;
then A128: 1 <= ((ny -' (len h11)) + 2) -' 1 by Lm1, NAT_D:42;
ny - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by A36, A85, XREAL_1:9;
then A129: h0 . ny = h21 . (((ny -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A126, A127, FINSEQ_6:118;
ny - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A39, A47, A36, A52, A55, A57, A85, XREAL_1:9;
then (ny -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A126, XREAL_1:6;
then ((ny -' (len h11)) + 2) -' 1 <= len h21 by A47, NAT_D:44;
then ((ny -' (len h11)) + 2) -' 1 in dom h21 by A128, FINSEQ_3:25;
then ((nx -' (len h1)) + 2) -' 1 = ((ny -' (len h1)) + 2) -' 1 by A39, A32, A81, A118, A116, A129;
then ((nx -' (len h1)) + 2) - 1 = ((ny -' (len h1)) + 2) -' 1 by A39, A115, Lm1, NAT_D:39, NAT_D:42;
then (nx -' (len h1)) + (2 - 1) = ((ny -' (len h1)) + 2) - 1 by A39, A128, NAT_D:39;
then ((len h1) + nx) - (len h1) = (len h1) + (ny - (len h1)) by A39, A111, A126, XCMPLX_1:29;
hence x = y ; :: thesis:

end;

then A130: h0 /. (len h0) <> W-min P by A16, A72, A65, A74, A75, A67;
A131: dom g2 = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
thus 8 <= len h0 by A38, A47, A36, A52, A55, A57, A58, FINSEQ_3:29; :: thesis:
( rng (mid (h21,2,((len h21) -' 1))) c= rng h21 & rng (g2 * h2) c= rng g2 ) by FINSEQ_6:119, RELAT_1:26;
then ( rng (g1 * h1) c= rng g1 & rng (mid (h21,2,((len h21) -' 1))) c= rng g2 ) by RELAT_1:26;
then (rng h11) \/ (rng (mid (h21,2,((len h21) -' 1)))) c= (Upper_Arc P) \/ (Lower_Arc P) by A5, A23, XBOOLE_1:13;
then rng h0 c= (Upper_Arc P) \/ (Lower_Arc P) by FINSEQ_1:31;
hence rng h0 c= P by A1, JORDAN6:def 9; :: thesis:
A132: dom g1 = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
thus for i being Nat st 1 <= i & i < len h0 holds
LE h0 /. i,h0 /. (i + 1),P :: thesis:

proof

let i be Nat; :: thesis:
assume that
A133: 1 <= i and
A134: i < len h0 ; :: thesis:
A135: i + 1 <= len h0 by A134, NAT_1:13;
A136: i < i + 1 by NAT_1:13;
A137: 1 < i + 1 by A133, NAT_1:13;

per cases ;

suppose A138: i < len h1 ; :: thesis:

then A139: i + 1 <= len h1 by NAT_1:13;
then A140: i + 1 in dom h1 by A137, FINSEQ_3:25;
then A141: h1 . (i + 1) in rng h1 by FUNCT_1:def 3;
then A142: h1 . (i + 1) <= 1 by A11, BORSUK_1:40, XXREAL_1:1;
h0 . (i + 1) = h11 . (i + 1) by A39, A137, A139, FINSEQ_1:64;
then A143: h0 . (i + 1) = g1 . (h1 . (i + 1)) by A140, FUNCT_1:13;
then A144: h0 . (i + 1) in Upper_Arc P by A5, A132, A11, A141, BORSUK_1:40, FUNCT_1:def 3;
i in dom h0 by A133, A134, FINSEQ_3:25;
then A145: h0 /. i = h0 . i by PARTFUN1:def 6;
A146: i in dom h1 by A133, A138, FINSEQ_3:25;
then A147: h1 . i in rng h1 by FUNCT_1:def 3;
then A148: ( 0 <= h1 . i & h1 . i <= 1 ) by A11, BORSUK_1:40, XXREAL_1:1;
A149: g1 . (h1 . i) in rng g1 by A132, A11, A147, BORSUK_1:40, FUNCT_1:def 3;
h0 . i = h11 . i by A39, A133, A138, FINSEQ_1:64;
then A150: h0 . i = g1 . (h1 . i) by A146, FUNCT_1:13;
i + 1 in dom h0 by A135, A137, FINSEQ_3:25;
then A151: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 6;
h1 . i < h1 . (i + 1) by A12, A136, A146, A140, SEQM_3:def 1;
then LE h0 /. i,h0 /. (i + 1), Upper_Arc P, W-min P, E-max P by A3, A4, A5, A6, A7, A150, A148, A143, A142, A145, A151, Th18;
hence LE h0 /. i,h0 /. (i + 1),P by A5, A150, A145, A151, A149, A144, JORDAN6:def 10; :: thesis:

end;

suppose A152: i >= len h1 ; :: thesis:

per cases by A152, XXREAL_0:1;

suppose A153: i > len h1 ; :: thesis:

A184: now :: thesis:

assume h0 /. (i + 1) = W-min P ; :: thesis:
then len h21 = (((i + 1) -' (len h11)) + 2) -' 1 by A46, A47, A34, A35, A32, A164, A174, A183;
then ((len h21) + 1) - (len h21) <= (len h21) - (len h21) by A47, A181, A182, XREAL_1:9;
then ((len h21) + 1) - (len h21) <= 0 ;
hence contradiction ; :: thesis:

end;

((i -' (len h11)) + 2) -' 1 < (((i -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
then A185: h2 . (((i -' (len h11)) + 2) -' 1) < h2 . ((((i -' (len h11)) + 2) -' 1) + 1) by A30, A170, A175, SEQM_3:def 1;
i in dom h0 by A133, A134, FINSEQ_3:25;
then A186: h0 /. i = h0 . i by PARTFUN1:def 6;
( 0 <= h2 . (((i -' (len h11)) + 2) -' 1) & h2 . (((i -' (len h11)) + 2) -' 1) <= 1 ) by A29, A172, BORSUK_1:40, XXREAL_1:1;
then LE h0 /. i,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P by A21, A22, A23, A24, A25, A171, A179, A177, A185, A186, A174, Th18;
hence LE h0 /. i,h0 /. (i + 1),P by A186, A174, A173, A180, A184, JORDAN6:def 10; :: thesis:

end;

suppose A187: i = len h1 ; :: thesis:

end;

A199: (len h0) -' 1 < len h0 by A66, JORDAN5B:1;
then A200: ((len h0) -' 1) + 1 <= len h0 by NAT_1:13;
A201: 1 + 1 <= len h0 by A65, A14, XXREAL_0:2;
then A202: 1 <= (len h0) -' 1 by Lm3;
then A203: (len h0) -' 1 in dom h0 by A199, FINSEQ_3:25;
then A204: h0 /. ((len h0) -' 1) = h0 . ((len h0) -' 1) by PARTFUN1:def 6;
A205: 1 + 1 <= len h0 by A66, NAT_1:13;
then 1 + 1 in dom h0 by FINSEQ_3:25;
then A206: h0 /. (1 + 1) = h0 . (1 + 1) by PARTFUN1:def 6;

A207: now :: thesis:

A208: 1 + 1 in dom h1 by A14, FINSEQ_3:25;
then A209: h1 . (1 + 1) in rng h1 by FUNCT_1:def 3;
A210: h0 . (1 + 1) = h11 . (1 + 1) by A39, A14, FINSEQ_1:64;
then h0 . (1 + 1) = g1 . (h1 . (1 + 1)) by A208, FUNCT_1:13;
then A211: h0 . (1 + 1) in Upper_Arc P by A5, A132, A11, A209, BORSUK_1:40, FUNCT_1:def 3;
assume A212: h0 /. (1 + 1) = h0 /. ((len h0) -' 1) ; :: thesis:

per cases ) -' 1 <= len h1 or (len h0) -' 1 > len h1 ) ;

suppose (len h0) -' 1 <= len h1 ; :: thesis:

then ( h0 . ((len h0) -' 1) = h11 . ((len h0) -' 1) & (len h0) -' 1 in dom h1 ) by A39, A202, FINSEQ_1:64, FINSEQ_3:25;
hence contradiction by A38, A20, A60, A204, A206, A212, A208, A210; :: thesis:

end;

suppose A213: (len h0) -' 1 > len h1 ; :: thesis:

(len h0) -' 1 in dom h0 by A202, A199, FINSEQ_3:25;
then A214: h0 /. ((len h0) -' 1) = h0 . ((len h0) -' 1) by PARTFUN1:def 6;
A215: ((len h0) -' 1) - (len h11) = ((len h0) -' 1) -' (len h11) by A39, A213, XREAL_1:233;
((len h0) -' 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A39, A47, A36, A52, A55, A57, A199, XREAL_1:9;
then (((len h0) -' 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A215, XREAL_1:6;
then A216: ((((len h0) -' 1) -' (len h11)) + 2) -' 1 <= len h21 by A47, NAT_D:44;
((len h0) -' 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A39, A47, A36, A52, A55, A57, A199, XREAL_1:9;
then A217: (((len h0) -' 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A215, XREAL_1:6;
set k = ((((len h0) -' 1) -' (len h11)) + 2) -' 1;
A218: ((len h0) -' 1) - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by A36, A199, XREAL_1:9;
A219: 0 + 2 <= (((len h0) -' 1) -' (len h11)) + 2 by XREAL_1:6;
then A220: ((((len h0) -' 1) -' (len h11)) + 2) -' 1 = ((((len h0) -' 1) -' (len h11)) + 2) - 1 by Lm1, NAT_D:39, NAT_D:42;
1 <= ((((len h0) -' 1) -' (len h11)) + 2) -' 1 by A219, Lm1, NAT_D:42;
then A221: ((((len h0) -' 1) -' (len h11)) + 2) -' 1 in dom h2 by A46, A216, FINSEQ_3:25;
then h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) in rng h2 by FUNCT_1:def 3;
then A222: g2 . (h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1)) in rng g2 by A131, A29, BORSUK_1:40, FUNCT_1:def 3;
A223: (len h1) + 1 <= (len h0) -' 1 by A213, NAT_1:13;
then ( h0 . ((len h0) -' 1) = (mid (h21,2,((len h21) -' 1))) . (((len h0) -' 1) - (len h11)) & ((len h1) + 1) - (len h1) <= ((len h0) -' 1) - (len h1) ) by A39, A36, A199, FINSEQ_1:23, XREAL_1:9;
then A224: h0 . ((len h0) -' 1) = h21 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A215, A218, FINSEQ_6:118;
then h0 . ((len h0) -' 1) = g2 . (h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1)) by A221, FUNCT_1:13;
then h0 . ((len h0) -' 1) in (Upper_Arc P) /\ (Lower_Arc P) by A23, A206, A212, A211, A214, A222, XBOOLE_0:def 4;
then h0 . ((len h0) -' 1) in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
then A225: ( h0 . ((len h0) -' 1) = W-min P or h0 . ((len h0) -' 1) = E-max P ) by TARSKI:def 2;
((len h11) + 1) - (len h11) <= ((len h0) -' 1) - (len h11) by A39, A223, XREAL_1:9;
then 1 <= ((len h0) -' 1) -' (len h11) by NAT_D:39;
then 1 + 2 <= (((len h0) -' 1) -' (len h11)) + 2 by XREAL_1:6;
then (1 + 2) - 1 <= ((((len h0) -' 1) -' (len h11)) + 2) - 1 by XREAL_1:9;
then A226: 1 < ((((len h0) -' 1) -' (len h11)) + 2) -' 1 by A220, XXREAL_0:2;
((((len h0) -' 1) -' (len h11)) + 2) -' 1 < (((((len h0) -' 1) -' (len h11)) + 2) - 1) + 1 by A220, NAT_1:13;
hence contradiction by A46, A76, A34, A77, A35, A32, A224, A217, A226, A221, A225; :: thesis:

end;

A227: 1 in dom g2 by Lm6, BORSUK_1:40, FUNCT_2:def 1;
A228: ((len h2) - 1) - 1 < len h2 by Lm4;

A229: now :: thesis:

per cases ) -' 1 <= len h1 or (len h0) -' 1 > len h1 ) ;

case A230: (len h0) -' 1 <= len h1 ; :: thesis:

A231: h0 /. (1 + 1) in Upper_Arc P by A5, A132, A11, A206, A42, A19, BORSUK_1:40, FUNCT_1:def 3;
A232: ( 0 <= h1 . (1 + 1) & h1 . (1 + 1) <= 1 ) by A11, A19, BORSUK_1:40, XXREAL_1:1;
A233: (len h0) -' 1 in dom h1 by A61, A230, FINSEQ_3:25;
then A234: h1 . ((len h0) -' 1) in rng h1 by FUNCT_1:def 3;
then A235: h1 . ((len h0) -' 1) <= 1 by A11, BORSUK_1:40, XXREAL_1:1;
h0 . ((len h0) -' 1) = h11 . ((len h0) -' 1) by A39, A61, A230, FINSEQ_1:64;
then A236: h0 . ((len h0) -' 1) = g1 . (h1 . ((len h0) -' 1)) by A233, FUNCT_1:13;
then A237: h0 /. ((len h0) -' 1) in Upper_Arc P by A5, A132, A11, A204, A234, BORSUK_1:40, FUNCT_1:def 3;
h1 . (1 + 1) < h1 . ((len h0) -' 1) by A12, A60, A18, A233, SEQM_3:def 1;
then LE h0 /. (1 + 1),h0 /. ((len h0) -' 1), Upper_Arc P, W-min P, E-max P by A3, A4, A5, A6, A7, A204, A206, A42, A236, A235, A232, Th18;
hence LE h0 /. (1 + 1),h0 /. ((len h0) -' 1),P by A231, A237, JORDAN6:def 10; :: thesis:

end;

case A238: (len h0) -' 1 > len h1 ; :: thesis:

1 + 1 in dom h1 by A14, FINSEQ_3:25;
then A239: h11 . (1 + 1) = g1 . (h1 . (1 + 1)) by FUNCT_1:13;
A240: ((len h0) -' 1) - (len h11) = ((len h0) -' 1) -' (len h11) by A39, A238, XREAL_1:233;
(((len h0) -' 1) + 1) - 1 <= ((len h1) + ((len h2) - 2)) - 1 by A39, A47, A36, A52, A55, A57, A200, XREAL_1:9;
then ((len h0) -' 1) - (len h11) <= ((len h1) + (((len h2) - 2) - 1)) - (len h11) by XREAL_1:9;
then (((len h0) -' 1) -' (len h11)) + 2 <= (((len h2) - 2) - 1) + 2 by A39, A240, XREAL_1:6;
then A241: ((((len h0) -' 1) -' (len h11)) + 2) - 1 <= ((len h2) - 1) - 1 by XREAL_1:9;
A242: (len h1) + 1 <= (len h0) -' 1 by A238, NAT_1:13;
then A243: ((len h1) + 1) - (len h1) <= ((len h0) -' 1) - (len h1) by XREAL_1:9;
h1 . (1 + 1) in rng h1 by A15, FUNCT_1:def 3;
then A244: g1 . (h1 . (1 + 1)) in rng g1 by A132, A11, BORSUK_1:40, FUNCT_1:def 3;
0 + 2 <= (((len h0) -' 1) -' (len h11)) + 2 by XREAL_1:6;
then A245: 2 -' 1 <= ((((len h0) -' 1) -' (len h11)) + 2) -' 1 by NAT_D:42;
set k = ((((len h0) -' 1) -' (len h11)) + 2) -' 1;
0 + 1 <= (((((len h0) -' 1) -' (len h11)) + 1) + 1) - 1 by XREAL_1:6;
then A246: ((((len h0) -' 1) -' (len h11)) + 2) -' 1 = ((((len h0) -' 1) -' (len h11)) + 2) - 1 by NAT_D:39;
A247: ((len h0) -' 1) - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by A36, A199, XREAL_1:9;
((len h0) -' 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A39, A47, A36, A52, A55, A57, A199, XREAL_1:9;
then (((len h0) -' 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A240, XREAL_1:6;
then ((((len h0) -' 1) -' (len h11)) + 2) -' 1 <= len h21 by A47, NAT_D:44;
then A248: ((((len h0) -' 1) -' (len h11)) + 2) -' 1 in dom h21 by A245, Lm1, FINSEQ_3:25;
A249: h0 . ((len h0) -' 1) = (mid (h21,2,((len h21) -' 1))) . (((len h0) -' 1) - (len h11)) by A39, A36, A199, A242, FINSEQ_1:23;
then h0 . ((len h0) -' 1) = h21 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A240, A247, A243, FINSEQ_6:118;
then A250: h0 . ((len h0) -' 1) = g2 . (h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1)) by A46, A248, FUNCT_1:13;
h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) in rng h2 by A46, A248, FUNCT_1:def 3;
then A251: h0 . ((len h0) -' 1) in Lower_Arc P by A23, A131, A29, A250, BORSUK_1:40, FUNCT_1:def 3;
1 <= ((len h0) -' 1) - (len h11) by A38, A243, FINSEQ_3:29;
then h0 . ((len h0) -' 1) = h21 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) by A48, A56, A50, A54, A240, A247, A249, FINSEQ_6:118;
then h0 /. ((len h0) -' 1) <> W-min P by A228, A46, A34, A35, A32, A204, A246, A248, A241;
hence LE h0 /. (1 + 1),h0 /. ((len h0) -' 1),P by A5, A204, A206, A41, A239, A244, A251, JORDAN6:def 10; :: thesis:

end;

A252: (len h0) - (len h11) = (len h0) -' (len h11) by A39, A65, XREAL_1:233;
then (((len h0) -' (len h11)) + 2) -' 1 <= len h21 by A36, A52, A55, A57, NAT_D:44;
then (((len h0) -' (len h11)) + 2) -' 1 in dom h21 by A43, Lm1, FINSEQ_3:25;
then A253: ( h21 . ((((len h0) -' (len h11)) + 2) -' 1) = g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) & h2 . ((((len h0) -' (len h11)) + 2) -' 1) in rng h2 ) by A46, FUNCT_1:13, FUNCT_1:def 3;
h1 . (len h1) in dom g1 by A9, A69, XXREAL_1:1;
then A254: len h1 in dom (g1 * h1) by A45, FUNCT_1:11;
then A255: h11 . (len h1) = E-max P by A7, A9, FUNCT_1:12;
A256: for i being Nat st 1 <= i & i + 1 <= len h0 holds
( LE h0 /. i,h0 /. (i + 1),P & h0 /. (i + 1) <> W-min P & h0 /. i <> h0 /. (i + 1) )

proof

let i be Nat; :: thesis:
assume that
A257: 1 <= i and
A258: i + 1 <= len h0 ; :: thesis:
A259: i < i + 1 by NAT_1:13;
A260: 1 < i + 1 by A257, NAT_1:13;
then i + 1 in dom h0 by A258, FINSEQ_3:25;
then A261: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 6;
A262: i < len h0 by A258, NAT_1:13;
then i in dom h0 by A257, FINSEQ_3:25;
then A263: h0 /. i = h0 . i by PARTFUN1:def 6;

per cases ;

suppose A264: i < len h1 ; :: thesis:

then A265: i + 1 <= len h1 by NAT_1:13;
then A266: i + 1 in dom h1 by A260, FINSEQ_3:25;
then A267: h1 . (i + 1) in rng h1 by FUNCT_1:def 3;
then A268: h1 . (i + 1) <= 1 by A11, BORSUK_1:40, XXREAL_1:1;
A269: ( i + 1 <> 1 & i + 1 <> i ) by A257, NAT_1:13;
A270: i in dom h1 by A257, A264, FINSEQ_3:25;
then A271: h1 . i in rng h1 by FUNCT_1:def 3;
then A272: ( 0 <= h1 . i & h1 . i <= 1 ) by A11, BORSUK_1:40, XXREAL_1:1;
A273: h0 . (i + 1) = h11 . (i + 1) by A39, A260, A265, FINSEQ_1:64;
then A274: h0 . (i + 1) = g1 . (h1 . (i + 1)) by A266, FUNCT_1:13;
then A275: h0 . (i + 1) in Upper_Arc P by A5, A132, A11, A267, BORSUK_1:40, FUNCT_1:def 3;
A276: h0 . i = h11 . i by A39, A257, A264, FINSEQ_1:64;
then A277: g1 . (h1 . i) = h0 /. i by A263, A270, FUNCT_1:13;
g1 . (h1 . i) in rng g1 by A132, A11, A271, BORSUK_1:40, FUNCT_1:def 3;
then A278: h0 . i in Upper_Arc P by A5, A276, A270, FUNCT_1:13;
h1 . i < h1 . (i + 1) by A12, A259, A270, A266, SEQM_3:def 1;
then LE h0 /. i,h0 /. (i + 1), Upper_Arc P, W-min P, E-max P by A3, A4, A5, A6, A7, A261, A274, A277, A272, A268, Th18;
hence ( LE h0 /. i,h0 /. (i + 1),P & h0 /. (i + 1) <> W-min P & h0 /. i <> h0 /. (i + 1) ) by A38, A17, A71, A20, A263, A261, A276, A270, A273, A266, A278, A275, A269, JORDAN6:def 10; :: thesis:

end;

suppose A279: i >= len h1 ; :: thesis:

per cases by A279, XXREAL_0:1;

suppose A280: i > len h1 ; :: thesis:

i - (len h11) < ((len h11) + ((len h2) - 2)) - (len h11) by A47, A36, A52, A55, A57, A262, XREAL_1:9;
then A281: (i - (len h11)) + 2 < ((len h2) - 2) + 2 by XREAL_1:6;
i + 1 > len h11 by A39, A280, NAT_1:13;
then A282: (i + 1) - (len h11) = (i + 1) -' (len h11) by XREAL_1:233;
set j = ((i -' (len h11)) + 2) -' 1;
A283: (i + 1) - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by A36, A258, XREAL_1:9;
A284: 0 + 2 <= (i -' (len h11)) + 2 by XREAL_1:6;
then A285: (((i -' (len h11)) + 2) -' 1) + 1 = (((i -' (len h11)) + (1 + 1)) - 1) + 1 by Lm1, NAT_D:39, NAT_D:42
.= (i -' (len h11)) + (1 + 1) ;
A286: (len h1) + 1 <= i by A280, NAT_1:13;
then A287: ((len h1) + 1) - (len h1) <= i - (len h1) by XREAL_1:9;
i + 1 in dom h0 by A258, A260, FINSEQ_3:25;
then A288: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 6;
A289: (len h1) + 1 <= i + 1 by A286, NAT_1:13;
then A290: ((len h1) + 1) - (len h1) <= (i + 1) - (len h1) by XREAL_1:9;
then 1 < ((i + 1) -' (len h11)) + (2 - 1) by A39, A282, NAT_1:13;
then A291: 0 < (((i + 1) -' (len h11)) + 2) - 1 ;
h0 . (i + 1) = (mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) by A39, A36, A258, A289, FINSEQ_1:23;
then A292: h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A282, A283, A290, FINSEQ_6:118;
A293: i <= (len h11) + (len (mid (h21,2,((len h21) -' 1)))) by A262, FINSEQ_1:22;
(len h11) + 1 <= i by A39, A280, NAT_1:13;
then A294: h0 . i = (mid (h21,2,((len h21) -' 1))) . (i - (len h11)) by A293, FINSEQ_1:23;
A295: i - (len h11) = i -' (len h11) by A39, A280, XREAL_1:233;
A296: 1 <= ((i -' (len h11)) + 2) -' 1 by A284, Lm1, NAT_D:42;
then 1 < (((i -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
then A297: (((i -' (len h11)) + 2) -' 1) + 1 in dom h2 by A295, A281, A285, FINSEQ_3:25;
then A298: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by FUNCT_1:def 3;
then A299: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) <= 1 by A29, BORSUK_1:40, XXREAL_1:1;
i - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A39, A47, A36, A52, A55, A57, A262, XREAL_1:9;
then (i -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A295, XREAL_1:6;
then ((i -' (len h11)) + 2) -' 1 <= len h21 by A47, NAT_D:44;
then A300: ((i -' (len h11)) + 2) -' 1 in dom h2 by A46, A296, FINSEQ_3:25;
((i -' (len h11)) + 2) -' 1 < (((i -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
then A301: h2 . (((i -' (len h11)) + 2) -' 1) < h2 . ((((i -' (len h11)) + 2) -' 1) + 1) by A30, A300, A297, SEQM_3:def 1;
i in dom h0 by A257, A262, FINSEQ_3:25;
then A302: h0 /. i = h0 . i by PARTFUN1:def 6;
i - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by A293, XREAL_1:9;
then A303: h0 . i = h21 . (((i -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A294, A295, A287, FINSEQ_6:118;
then A304: h0 . i = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by A300, FUNCT_1:13;
A305: (((i -' (len h11)) + 2) -' 1) + 1 = (((i - (len h11)) + 2) - 1) + 1 by A295, A284, Lm1, NAT_D:39, NAT_D:42
.= (((i + 1) -' (len h11)) + 2) -' 1 by A282, A291, XREAL_0:def 2 ;
then A306: h0 /. (i + 1) <> W-min P by A46, A34, A35, A32, A295, A292, A281, A285, A297, A288;
A307: h0 . (i + 1) = g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) by A292, A305, A297, FUNCT_1:13;
then A308: h0 /. (i + 1) in Lower_Arc P by A23, A131, A29, A298, A288, BORSUK_1:40, FUNCT_1:def 3;
A309: h2 . (((i -' (len h11)) + 2) -' 1) in rng h2 by A300, FUNCT_1:def 3;
then A310: ( ((i -' (len h11)) + 2) -' 1 < (((i -' (len h11)) + 2) -' 1) + 1 & h0 /. i in Lower_Arc P ) by A23, A131, A29, A304, A302, BORSUK_1:40, FUNCT_1:def 3, NAT_1:13;
( 0 <= h2 . (((i -' (len h11)) + 2) -' 1) & h2 . (((i -' (len h11)) + 2) -' 1) <= 1 ) by A29, A309, BORSUK_1:40, XXREAL_1:1;
then LE h0 /. i,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P by A21, A22, A23, A24, A25, A304, A307, A301, A302, A288, A299, Th18;
hence ( LE h0 /. i,h0 /. (i + 1),P & h0 /. (i + 1) <> W-min P & h0 /. i <> h0 /. (i + 1) ) by A46, A32, A303, A292, A305, A300, A297, A302, A288, A306, A310, A308, JORDAN6:def 10; :: thesis:

end;

suppose A311: i = len h1 ; :: thesis:

then A312: i - (len h11) = i -' (len h11) by A39, XREAL_1:233;
i - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A39, A47, A36, A52, A55, A57, A262, XREAL_1:9;
then A313: (i -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A312, XREAL_1:6;
then A314: ((i -' (len h11)) + 2) -' 1 <= len h21 by A47, NAT_D:44;
set j = ((i -' (len h11)) + 2) -' 1;
A315: (((i -' (len h11)) + 2) -' 1) + 1 <> ((i -' (len h11)) + 2) -' 1 ;
A316: 0 + 2 <= (i -' (len h11)) + 2 by XREAL_1:6;
then A317: (((i -' (len h11)) + 2) -' 1) + 1 = (((i -' (len h11)) + (1 + 1)) - 1) + 1 by Lm1, NAT_D:39, NAT_D:42
.= (i -' (len h11)) + 2 ;
2 -' 1 <= ((i -' (len h11)) + 2) -' 1 by A316, NAT_D:42;
then 1 < (((i -' (len h11)) + 2) -' 1) + 1 by Lm1, NAT_1:13;
then A318: (((i -' (len h11)) + 2) -' 1) + 1 in dom h2 by A313, A317, FINSEQ_3:25;
then A319: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by FUNCT_1:def 3;
i + 1 <= (len h11) + (len (mid (h21,2,((len h21) -' 1)))) by A258, FINSEQ_1:22;
then A320: (i + 1) - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by XREAL_1:9;
A321: (i + 1) - (len h11) = (i + 1) -' (len h11) by A39, A259, A311, XREAL_1:233;
then A322: 0 < (((i + 1) -' (len h11)) + 2) - 1 by A39, A311;
h0 . (i + 1) = (mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) by A39, A36, A258, A311, FINSEQ_1:23;
then A323: h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A311, A321, A320, FINSEQ_6:118;
A324: h0 . i = E-max P by A39, A255, A257, A311, FINSEQ_1:64;
then A325: h0 . i in Upper_Arc P by A1, Th1;
(len h1) -' (len h11) = (len h11) - (len h11) by A39, XREAL_0:def 2;
then (0 + 2) - 1 = (((len h1) -' (len h11)) + 2) - 1 ;
then A326: h0 . i = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by A24, A26, A311, A324, NAT_D:39;
1 <= ((i -' (len h11)) + 2) -' 1 by A316, Lm1, NAT_D:42;
then A327: ((i -' (len h11)) + 2) -' 1 in dom h2 by A46, A314, FINSEQ_3:25;
then A328: h21 . (((i -' (len h11)) + 2) -' 1) = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by FUNCT_1:13;
i in dom h0 by A257, A262, FINSEQ_3:25;
then A329: h0 /. i = h0 . i by PARTFUN1:def 6;
i + 1 in dom h0 by A258, A260, FINSEQ_3:25;
then A330: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 6;
A331: (((i -' (len h11)) + 2) -' 1) + 1 = (((i - (len h11)) + 2) - 1) + 1 by A39, A311, Lm1, XREAL_0:def 2
.= (((i + 1) -' (len h11)) + 2) -' 1 by A321, A322, XREAL_0:def 2 ;
then h0 . (i + 1) = g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) by A323, A318, FUNCT_1:13;
then A332: h0 . (i + 1) in Lower_Arc P by A23, A131, A29, A319, BORSUK_1:40, FUNCT_1:def 3;
i - (len h11) < ((len h11) + ((len h2) - 2)) - (len h11) by A47, A36, A52, A55, A57, A262, XREAL_1:9;
then (i - (len h11)) + 2 < ((len h2) - 2) + 2 by XREAL_1:6;
then (((i -' (len h11)) + 2) -' 1) + 1 < len h2 by A39, A311, A317, XREAL_0:def 2;
then h0 /. (i + 1) <> W-min P by A46, A34, A35, A32, A323, A331, A318, A330;
hence ( LE h0 /. i,h0 /. (i + 1),P & h0 /. (i + 1) <> W-min P & h0 /. i <> h0 /. (i + 1) ) by A46, A32, A323, A331, A327, A328, A326, A318, A329, A330, A332, A325, A315, JORDAN6:def 10; :: thesis:

end;

then A333: ( LE h0 /. 1,h0 /. (1 + 1),P & h0 /. 1 <> h0 /. (1 + 1) ) by A205;
A334: E-max P in Upper_Arc P by A1, Th1;
thus for i being Nat
for W being Subset of (Euclid 2) st 1 <= i & i < len h0 & W = Segment ((h0 /. i),(h0 /. (i + 1)),P) holds
diameter W < e :: thesis:

proof

let i be Nat; :: thesis:
let W be Subset of (Euclid 2); :: thesis:
assume that
A335: 1 <= i and
A336: i < len h0 and
A337: W = Segment ((h0 /. i),(h0 /. (i + 1)),P) ; :: thesis:
A338: i + 1 <= len h0 by A336, NAT_1:13;
A339: i < i + 1 by NAT_1:13;
A340: 1 < i + 1 by A335, NAT_1:13;

per cases by XXREAL_0:1;

suppose A341: i < len h1 ; :: thesis:

then A342: i in dom h1 by A335, FINSEQ_3:25;
then A343: h1 . i in rng h1 by FUNCT_1:def 3;
then A344: h1 . i <= 1 by A11, BORSUK_1:40, XXREAL_1:1;
A345: 0 <= h1 . i by A11, A343, BORSUK_1:40, XXREAL_1:1;
A346: h1 /. i = h1 . i by A335, A341, FINSEQ_4:15;
A347: h11 . i = g1 . (h1 . i) by A342, FUNCT_1:13;
then A348: h0 . i = g1 . (h1 . i) by A39, A335, A341, FINSEQ_1:64;
then A349: h0 . i in Upper_Arc P by A5, A132, A11, A343, BORSUK_1:40, FUNCT_1:def 3;
i in dom h0 by A335, A336, FINSEQ_3:25;
then A350: h0 /. i = h0 . i by PARTFUN1:def 6;
i + 1 in dom h0 by A338, A340, FINSEQ_3:25;
then A351: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 6;
A352: i + 1 <= len h1 by A341, NAT_1:13;
then A353: i + 1 in dom h1 by A340, FINSEQ_3:25;
then A354: h1 . i < h1 . (i + 1) by A12, A339, A342, SEQM_3:def 1;
A355: h1 /. (i + 1) = h1 . (i + 1) by A340, A352, FINSEQ_4:15;
A356: h1 . (i + 1) in rng h1 by A353, FUNCT_1:def 3;
then reconsider Q1 = [.(h1 /. i),(h1 /. (i + 1)).] as Subset of I[01] by A11, A343, A346, A355, BORSUK_1:40, XXREAL_2:def 12;
A357: h0 . i = h11 . i by A39, A335, A341, FINSEQ_1:64;
A358: h0 . (i + 1) = h11 . (i + 1) by A39, A340, A352, FINSEQ_1:64;
then A359: h0 . (i + 1) = g1 . (h1 . (i + 1)) by A353, FUNCT_1:13;
then A360: h0 . (i + 1) in Upper_Arc P by A5, A132, A11, A356, BORSUK_1:40, FUNCT_1:def 3;
A361: Segment ((h0 /. i),(h0 /. (i + 1)),P) c= g1 .: [.(h1 /. i),(h1 /. (i + 1)).]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
A362: h0 /. (i + 1) <> W-min P by A38, A17, A71, A20, A340, A358, A353, A351;
assume x in Segment ((h0 /. i),(h0 /. (i + 1)),P) ; :: thesis:
then x in { p where p is Point of (TOP-REAL 2) : ( LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) } by A362, Def1;
then consider p being Point of (TOP-REAL 2) such that
A363: p = x and
A364: LE h0 /. i,p,P and
A365: LE p,h0 /. (i + 1),P ;
A366: ( ( h0 /. i in Upper_Arc P & p in Lower_Arc P & not p = W-min P ) or ( h0 /. i in Upper_Arc P & p in Upper_Arc P & LE h0 /. i,p, Upper_Arc P, W-min P, E-max P ) or ( h0 /. i in Lower_Arc P & p in Lower_Arc P & not p = W-min P & LE h0 /. i,p, Lower_Arc P, E-max P, W-min P ) ) by A364, JORDAN6:def 10;
A367: ( ( p in Upper_Arc P & h0 /. (i + 1) in Lower_Arc P ) or ( p in Upper_Arc P & h0 /. (i + 1) in Upper_Arc P & LE p,h0 /. (i + 1), Upper_Arc P, W-min P, E-max P ) or ( p in Lower_Arc P & h0 /. (i + 1) in Lower_Arc P & LE p,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P ) ) by A365, JORDAN6:def 10;

now :: thesis:

per cases by A352, XXREAL_0:1;

suppose i + 1 < len h1 ; :: thesis:

then A368: h0 /. (i + 1) <> E-max P by A38, A45, A255, A20, A358, A353, A351;

A369: now :: thesis:

assume h0 /. (i + 1) in Lower_Arc P ; :: thesis:
then h0 /. (i + 1) in (Upper_Arc P) /\ (Lower_Arc P) by A351, A360, XBOOLE_0:def 4;
then h0 /. (i + 1) in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
hence contradiction by A362, A368, TARSKI:def 2; :: thesis:

end;

then A370: LE p,h0 /. (i + 1), Upper_Arc P, W-min P, E-max P by A365, JORDAN6:def 10;
then A371: p <> E-max P by A3, A368, JORDAN6:55;
A372: p in Upper_Arc P by A365, A369, JORDAN6:def 10;

per cases by A335, XXREAL_0:1;

suppose i > 1 ; :: thesis:

then A373: h0 /. i <> W-min P by A38, A17, A71, A20, A342, A347, A348, A350;
A374: h11 . i <> E-max P by A38, A45, A255, A20, A341, A342;

now :: thesis:

assume h0 /. i in Lower_Arc P ; :: thesis:
then h0 /. i in (Upper_Arc P) /\ (Lower_Arc P) by A350, A349, XBOOLE_0:def 4;
then h0 /. i in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
hence contradiction by A357, A350, A373, A374, TARSKI:def 2; :: thesis:

end;

then A375: ( ( h0 /. i in Upper_Arc P & p in Lower_Arc P & not p = W-min P ) or ( h0 /. i in Upper_Arc P & p in Upper_Arc P & LE h0 /. i,p, Upper_Arc P, W-min P, E-max P ) ) by A364, JORDAN6:def 10;
then A376: p <> W-min P by A3, A373, JORDAN6:54;

A377: now :: thesis:

assume p in Lower_Arc P ; :: thesis:
then p in (Upper_Arc P) /\ (Lower_Arc P) by A372, XBOOLE_0:def 4;
then p in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
hence contradiction by A371, A376, TARSKI:def 2; :: thesis:

end;

then consider z being object such that
A378: z in dom g1 and
A379: p = g1 . z by A5, A375, FUNCT_1:def 3;
reconsider rz = z as Real by A132, A378;
A380: rz <= 1 by A378, BORSUK_1:40, XXREAL_1:1;
h1 . (i + 1) in rng h1 by A353, FUNCT_1:def 3;
then A381: ( 0 <= h1 /. (i + 1) & h1 /. (i + 1) <= 1 ) by A11, A355, BORSUK_1:40, XXREAL_1:1;
reconsider z = z as set by TARSKI:1;
take z = z; :: thesis:
thus z in dom g1 by A378; :: thesis:
A382: ( g1 . (h1 /. i) = h0 /. i & h1 /. i <= 1 ) by A335, A341, A357, A347, A344, A350, FINSEQ_4:15;
g1 . (h1 /. (i + 1)) = h0 /. (i + 1) by A340, A352, A359, A351, FINSEQ_4:15;
then A383: rz <= h1 /. (i + 1) by A4, A5, A6, A7, A370, A379, A381, A380, Th19;
0 <= rz by A378, BORSUK_1:40, XXREAL_1:1;
then h1 /. i <= rz by A4, A5, A6, A7, A375, A377, A379, A382, A380, Th19;
hence z in [.(h1 /. i),(h1 /. (i + 1)).] by A383, XXREAL_1:1; :: thesis:
thus x = g1 . z by A363, A379; :: thesis:

end;

suppose A384: i = 1 ; :: thesis:

now :: thesis:

per cases ;

case A385: p <> W-min P ; :: thesis:

now :: thesis:

end;

then consider z being object such that
A386: z in dom g1 and
A387: p = g1 . z by A5, A366, FUNCT_1:def 3;
reconsider rz = z as Real by A132, A386;
A388: h1 /. 1 <= rz by A8, A346, A384, A386, BORSUK_1:40, XXREAL_1:1;
h1 . (1 + 1) in rng h1 by A353, A384, FUNCT_1:def 3;
then A389: ( 0 <= h1 /. (1 + 1) & h1 /. (1 + 1) <= 1 ) by A11, A355, A384, BORSUK_1:40, XXREAL_1:1;
A390: g1 . (h1 /. (1 + 1)) = h0 /. (1 + 1) by A352, A359, A351, A384, FINSEQ_4:15;
take rz = rz; :: thesis:
rz <= 1 by A386, BORSUK_1:40, XXREAL_1:1;
then rz <= h1 /. (1 + 1) by A4, A5, A6, A7, A370, A384, A387, A390, A389, Th19;
hence ( rz in dom g1 & rz in [.(h1 /. 1),(h1 /. (1 + 1)).] & x = g1 . rz ) by A363, A386, A387, A388, XXREAL_1:1; :: thesis:

end;

case A391: p = W-min P ; :: thesis:

thus 0 in [.(h1 /. 1),(h1 /. (1 + 1)).] by A8, A354, A346, A355, A384, XXREAL_1:1; :: thesis:
thus x = g1 . 0 by A6, A363, A391; :: thesis:

end;

hence ex y being set st
( y in dom g1 & y in [.(h1 /. i),(h1 /. (i + 1)).] & x = g1 . y ) by A44, A384; :: thesis:

end;

suppose A392: i + 1 = len h1 ; :: thesis:

then A393: h0 /. (i + 1) = E-max P by A7, A9, A45, A358, A351, FUNCT_1:13;

A394: now :: thesis:

assume that
A395: p in Lower_Arc P and
A396: not p in Upper_Arc P ; :: thesis:
LE h0 /. (i + 1),p, Lower_Arc P, E-max P, W-min P by A21, A393, A395, JORDAN5C:10;
hence contradiction by A334, A21, A367, A393, A396, JORDAN5C:12; :: thesis:

end;

( p in Upper_Arc P or p in Lower_Arc P ) by A364, JORDAN6:def 10;
then A397: LE p,h0 /. (i + 1), Upper_Arc P, W-min P, E-max P by A3, A393, A394, JORDAN5C:10;

per cases ;

suppose A398: p <> E-max P ; :: thesis:

now :: thesis:

per cases ;

case A399: p <> W-min P ; :: thesis:

A400: now :: thesis:

assume p in Lower_Arc P ; :: thesis:
then p in (Upper_Arc P) /\ (Lower_Arc P) by A394, XBOOLE_0:def 4;
then p in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
hence contradiction by A398, A399, TARSKI:def 2; :: thesis:

end;

then consider z being object such that
A401: z in dom g1 and
A402: p = g1 . z by A5, A366, FUNCT_1:def 3;
reconsider rz = z as Real by A132, A401;
A403: rz <= 1 by A401, BORSUK_1:40, XXREAL_1:1;
h1 . (i + 1) in rng h1 by A353, FUNCT_1:def 3;
then A404: ( 0 <= h1 /. (i + 1) & h1 /. (i + 1) <= 1 ) by A11, A355, BORSUK_1:40, XXREAL_1:1;
g1 . (h1 /. (i + 1)) = h0 /. (i + 1) by A340, A352, A359, A351, FINSEQ_4:15;
then A405: rz <= h1 /. (i + 1) by A4, A5, A6, A7, A397, A402, A404, A403, Th19;
take rz = rz; :: thesis:
0 <= rz by A401, BORSUK_1:40, XXREAL_1:1;
then h1 /. i <= rz by A4, A5, A6, A7, A357, A347, A344, A350, A346, A366, A400, A402, A403, Th19;
hence ( rz in dom g1 & rz in [.(h1 /. i),(h1 /. (i + 1)).] & x = g1 . rz ) by A363, A401, A402, A405, XXREAL_1:1; :: thesis:

end;

case A406: p = W-min P ; :: thesis:

then h11 . i = W-min P by A3, A357, A350, A366, JORDAN6:54;
then i = 1 by A38, A17, A71, A20, A342;
then 0 in [.(h1 /. i),(h1 /. (i + 1)).] by A8, A354, A346, A355, XXREAL_1:1;
hence ex y being set st
( y in dom g1 & y in [.(h1 /. i),(h1 /. (i + 1)).] & x = g1 . y ) by A6, A44, A363, A406; :: thesis:

end;

hence ex y being set st
( y in dom g1 & y in [.(h1 /. i),(h1 /. (i + 1)).] & x = g1 . y ) ; :: thesis:

end;

suppose A407: p = E-max P ; :: thesis:

1 in [.(h1 /. i),(h1 /. (i + 1)).] by A9, A354, A346, A355, A392, XXREAL_1:1;
hence ex y being set st
( y in dom g1 & y in [.(h1 /. i),(h1 /. (i + 1)).] & x = g1 . y ) by A7, A69, A363, A407, Lm6; :: thesis:

end;

hence x in g1 .: [.(h1 /. i),(h1 /. (i + 1)).] by FUNCT_1:def 6; :: thesis:

end;

A408: h1 . (i + 1) <= 1 by A11, A356, BORSUK_1:40, XXREAL_1:1;
g1 .: [.(h1 /. i),(h1 /. (i + 1)).] c= Segment ((h0 /. i),(h0 /. (i + 1)),P)

proof

A409: ( g1 . (h1 /. i) = h0 /. i & 0 <= h1 /. i ) by A335, A341, A348, A345, A350, FINSEQ_4:15;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in g1 .: [.(h1 /. i),(h1 /. (i + 1)).] ; :: thesis:
then consider y being object such that
A410: y in dom g1 and
A411: y in [.(h1 /. i),(h1 /. (i + 1)).] and
A412: x = g1 . y by FUNCT_1:def 6;
reconsider sy = y as Real by A411;
A413: sy <= 1 by A410, BORSUK_1:40, XXREAL_1:1;
A414: x in Upper_Arc P by A5, A410, A412, FUNCT_1:def 3;
then reconsider p1 = x as Point of (TOP-REAL 2) ;
A415: h1 /. i <= 1 by A335, A341, A344, FINSEQ_4:15;
h1 /. i <= sy by A411, XXREAL_1:1;
then LE h0 /. i,p1, Upper_Arc P, W-min P, E-max P by A3, A4, A5, A6, A7, A412, A409, A415, A413, Th18;
then A416: LE h0 /. i,p1,P by A350, A349, A414, JORDAN6:def 10;
( sy <= h1 /. (i + 1) & 0 <= sy ) by A410, A411, BORSUK_1:40, XXREAL_1:1;
then LE p1,h0 /. (i + 1), Upper_Arc P, W-min P, E-max P by A3, A4, A5, A6, A7, A359, A408, A351, A355, A412, A413, Th18;
then LE p1,h0 /. (i + 1),P by A351, A360, A414, JORDAN6:def 10;
then A417: x in { p where p is Point of (TOP-REAL 2) : ( LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) } by A416;
not h0 /. (i + 1) = W-min P by A38, A17, A71, A20, A340, A358, A353, A351;
hence x in Segment ((h0 /. i),(h0 /. (i + 1)),P) by A417, Def1; :: thesis:

end;

then W = g1 .: Q1 by A337, A361;
hence diameter W < e by A13, A335, A341; :: thesis:

end;

suppose A418: i > len h1 ; :: thesis:

i - (len h11) < ((len h11) + ((len h2) - 2)) - (len h11) by A47, A36, A52, A55, A57, A336, XREAL_1:9;
then A419: (i - (len h11)) + 2 < ((len h2) - 2) + 2 by XREAL_1:6;
A420: (len h1) + 1 <= i by A418, NAT_1:13;
then A421: ((len h1) + 1) - (len h1) <= i - (len h1) by XREAL_1:9;
A422: i - (len h11) = i -' (len h11) by A39, A418, XREAL_1:233;
i - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A39, A47, A36, A52, A55, A57, A336, XREAL_1:9;
then A423: (i -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A422, XREAL_1:6;
i + 1 > len h11 by A39, A418, NAT_1:13;
then A424: (i + 1) - (len h11) = (i + 1) -' (len h11) by XREAL_1:233;
i + 1 in dom h0 by A338, A340, FINSEQ_3:25;
then A425: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 6;
A426: i <= (len h11) + (len (mid (h21,2,((len h21) -' 1)))) by A336, FINSEQ_1:22;
(len h11) + 1 <= i by A39, A418, NAT_1:13;
then A427: h0 . i = (mid (h21,2,((len h21) -' 1))) . (i - (len h11)) by A426, FINSEQ_1:23;
A428: (i + 1) - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by A36, A338, XREAL_1:9;
i in dom h0 by A335, A336, FINSEQ_3:25;
then A429: h0 /. i = h0 . i by PARTFUN1:def 6;
set j = ((i -' (len h11)) + 2) -' 1;
len h2 < (len h2) + 1 by NAT_1:13;
then A430: (len h2) - 1 < ((len h2) + 1) - 1 by XREAL_1:9;
A431: 0 + 2 <= (i -' (len h11)) + 2 by XREAL_1:6;
then A432: (((i -' (len h11)) + 2) -' 1) + 1 = ((((i -' (len h11)) + 1) + 1) - 1) + 1 by Lm1, NAT_D:39, NAT_D:42
.= (i -' (len h11)) + (1 + 1) ;
A433: 1 <= ((i -' (len h11)) + 2) -' 1 by A431, Lm1, NAT_D:42;
then A434: 1 < (((i -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
then A435: (((i -' (len h11)) + 2) -' 1) + 1 in dom h2 by A423, A432, FINSEQ_3:25;
then A436: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by FUNCT_1:def 3;
then A437: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) <= 1 by A29, BORSUK_1:40, XXREAL_1:1;
A438: h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) = h2 . ((((i -' (len h11)) + 2) -' 1) + 1) by A423, A432, A434, FINSEQ_4:15;
((i -' (len h11)) + 2) -' 1 <= len h21 by A47, A423, NAT_D:44;
then A439: ((i -' (len h11)) + 2) -' 1 in dom h2 by A46, A433, FINSEQ_3:25;
i - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by A36, A336, XREAL_1:9;
then A440: h0 . i = h21 . (((i -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A427, A422, A421, FINSEQ_6:118;
then A441: h0 . i = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by A439, FUNCT_1:13;
A442: h2 . (((i -' (len h11)) + 2) -' 1) in rng h2 by A439, FUNCT_1:def 3;
then g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) in rng g2 by A131, A29, BORSUK_1:40, FUNCT_1:def 3;
then A443: h0 . i in Lower_Arc P by A23, A440, A439, FUNCT_1:13;
((i -' (len h11)) + 2) - 1 <= (len h2) - 1 by A423, XREAL_1:9;
then ((i -' (len h11)) + 2) - 1 < len h2 by A430, XXREAL_0:2;
then A444: ((i -' (len h11)) + 2) -' 1 < len h2 by A431, Lm1, NAT_D:39, NAT_D:42;
then A445: h2 /. (((i -' (len h11)) + 2) -' 1) = h2 . (((i -' (len h11)) + 2) -' 1) by A431, Lm1, FINSEQ_4:15, NAT_D:42;
then reconsider Q1 = [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] as Subset of I[01] by A29, A442, A436, A438, BORSUK_1:40, XXREAL_2:def 12;
A446: ( 0 <= h2 . (((i -' (len h11)) + 2) -' 1) & h2 . (((i -' (len h11)) + 2) -' 1) <= 1 ) by A29, A442, BORSUK_1:40, XXREAL_1:1;
A447: ((i -' (len h11)) + 2) -' 1 = ((i -' (len h11)) + 2) - 1 by A431, Lm1, NAT_D:39, NAT_D:42;
A448: (len h1) + 1 <= i + 1 by A420, NAT_1:13;
then A449: ((len h1) + 1) - (len h1) <= (i + 1) - (len h1) by XREAL_1:9;
then 1 < ((i + 1) -' (len h11)) + (2 - 1) by A39, A424, NAT_1:13;
then 0 < (((i + 1) -' (len h11)) + 2) - 1 ;
then A450: (((i -' (len h11)) + 2) -' 1) + 1 = (((i + 1) -' (len h11)) + 2) -' 1 by A422, A424, A447, XREAL_0:def 2;
h0 . (i + 1) = (mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) by A39, A36, A338, A448, FINSEQ_1:23;
then A451: h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A424, A428, A449, FINSEQ_6:118;
then h0 . (i + 1) = g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) by A450, A435, FUNCT_1:13;
then A452: h0 . (i + 1) in Lower_Arc P by A23, A131, A29, A436, BORSUK_1:40, FUNCT_1:def 3;
(len h1) + 1 <= i by A418, NAT_1:13;
then ((len h11) + 1) - (len h11) <= i - (len h11) by A39, XREAL_1:9;
then 1 <= i -' (len h11) by NAT_D:39;
then 1 + 2 <= (i -' (len h11)) + 2 by XREAL_1:6;
then (1 + 2) - 1 <= ((i -' (len h11)) + 2) - 1 by XREAL_1:9;
then A453: 1 < ((i -' (len h11)) + 2) -' 1 by A447, XXREAL_0:2;
A454: Segment ((h0 /. i),(h0 /. (i + 1)),P) c= g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).]

proof

h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by A435, FUNCT_1:def 3;
then A455: ( 0 <= h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) & h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) <= 1 ) by A29, A438, BORSUK_1:40, XXREAL_1:1;
A456: g2 . (h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)) = h0 /. (i + 1) by A451, A450, A435, A425, A438, FUNCT_1:13;
((i -' (len h11)) + 2) -' 1 < len h2 by A423, A432, NAT_1:13;
then A457: h0 /. i <> W-min P by A46, A34, A35, A32, A440, A439, A429;
A458: h2 /. (((i -' (len h11)) + 2) -' 1) <= 1 by A29, A442, A445, BORSUK_1:40, XXREAL_1:1;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A459: x in Segment ((h0 /. i),(h0 /. (i + 1)),P) ; :: thesis:
h0 /. (i + 1) <> W-min P by A46, A34, A35, A32, A422, A451, A419, A432, A450, A435, A425;
then x in { p where p is Point of (TOP-REAL 2) : ( LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) } by A459, Def1;
then consider p being Point of (TOP-REAL 2) such that
A460: p = x and
A461: LE h0 /. i,p,P and
A462: LE p,h0 /. (i + 1),P ;
A463: ( ( h0 /. i in Upper_Arc P & p in Lower_Arc P & not p = W-min P ) or ( h0 /. i in Upper_Arc P & p in Upper_Arc P & LE h0 /. i,p, Upper_Arc P, W-min P, E-max P ) or ( h0 /. i in Lower_Arc P & p in Lower_Arc P & not p = W-min P & LE h0 /. i,p, Lower_Arc P, E-max P, W-min P ) ) by A461, JORDAN6:def 10;
A464: h21 . (((i -' (len h11)) + 2) -' 1) <> E-max P by A46, A76, A77, A32, A453, A439;

A465: now :: thesis:

assume h0 /. i in Upper_Arc P ; :: thesis:
then h0 /. i in (Upper_Arc P) /\ (Lower_Arc P) by A429, A443, XBOOLE_0:def 4;
then h0 /. i in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
hence contradiction by A440, A429, A457, A464, TARSKI:def 2; :: thesis:

end;

then A466: LE h0 /. i,p, Lower_Arc P, E-max P, W-min P by A461, JORDAN6:def 10;
A467: h0 /. i <> E-max P by A46, A76, A77, A32, A440, A453, A439, A429;

A468: now :: thesis:

assume p in Upper_Arc P ; :: thesis:
then p in (Upper_Arc P) /\ (Lower_Arc P) by A463, A465, XBOOLE_0:def 4;
then p in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
then ( p = W-min P or p = E-max P ) by TARSKI:def 2;
hence contradiction by A21, A463, A465, A467, JORDAN6:54; :: thesis:

end;

A469: ( h0 /. (i + 1) <> E-max P & h21 . ((((i -' (len h11)) + 2) -' 1) + 1) <> W-min P ) by A46, A76, A34, A77, A35, A32, A422, A451, A419, A432, A450, A434, A435, A425;

now :: thesis:

assume h0 /. (i + 1) in Upper_Arc P ; :: thesis:
then h0 /. (i + 1) in (Upper_Arc P) /\ (Lower_Arc P) by A425, A452, XBOOLE_0:def 4;
then h0 /. (i + 1) in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
hence contradiction by A451, A450, A425, A469, TARSKI:def 2; :: thesis:

end;

then ( ( p in Lower_Arc P & h0 /. (i + 1) in Lower_Arc P & not h0 /. (i + 1) = W-min P & LE p,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P ) or ( p in Upper_Arc P & h0 /. (i + 1) in Lower_Arc P & not h0 /. (i + 1) = W-min P ) ) by A462, JORDAN6:def 10;
then consider z being object such that
A470: z in dom g2 and
A471: p = g2 . z by A23, A468, FUNCT_1:def 3;
reconsider rz = z as Real by A131, A470;
A472: rz <= 1 by A470, BORSUK_1:40, XXREAL_1:1;
LE p,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P by A462, A468, JORDAN6:def 10;
then A473: rz <= h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) by A22, A23, A24, A25, A471, A456, A472, A455, Th19;
0 <= rz by A470, BORSUK_1:40, XXREAL_1:1;
then h2 /. (((i -' (len h11)) + 2) -' 1) <= rz by A22, A23, A24, A25, A441, A429, A445, A466, A471, A458, A472, Th19;
then rz in [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] by A473, XXREAL_1:1;
hence x in g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] by A460, A470, A471, FUNCT_1:def 6; :: thesis:

end;

A474: g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) = h0 /. (i + 1) by A451, A450, A435, A425, FUNCT_1:13;
g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] c= Segment ((h0 /. i),(h0 /. (i + 1)),P)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] ; :: thesis:
then consider y being object such that
A475: y in dom g2 and
A476: y in [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] and
A477: x = g2 . y by FUNCT_1:def 6;
reconsider sy = y as Real by A476;
A478: sy <= h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) by A476, XXREAL_1:1;
A479: x in Lower_Arc P by A23, A475, A477, FUNCT_1:def 3;
then reconsider p1 = x as Point of (TOP-REAL 2) ;
A480: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) <> 1 by A27, A30, A34, A422, A419, A432, A435, FUNCT_1:def 4;

A481: now :: thesis:

assume p1 = W-min P ; :: thesis:
then 1 = sy by A22, A25, A227, A475, A477;
hence contradiction by A437, A438, A478, A480, XXREAL_0:1; :: thesis:

end;

A482: sy <= 1 by A475, BORSUK_1:40, XXREAL_1:1;
h2 /. (((i -' (len h11)) + 2) -' 1) <= sy by A476, XXREAL_1:1;
then LE h0 /. i,p1, Lower_Arc P, E-max P, W-min P by A21, A22, A23, A24, A25, A441, A429, A446, A445, A477, A482, Th18;
then A483: LE h0 /. i,p1,P by A429, A443, A479, A481, JORDAN6:def 10;
A484: h0 /. (i + 1) <> W-min P by A46, A34, A35, A32, A422, A451, A419, A432, A450, A435, A425;
0 <= sy by A475, BORSUK_1:40, XXREAL_1:1;
then LE p1,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P by A21, A22, A23, A24, A25, A474, A437, A438, A477, A478, A482, Th18;
then LE p1,h0 /. (i + 1),P by A425, A452, A479, A484, JORDAN6:def 10;
then x in { p where p is Point of (TOP-REAL 2) : ( LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) } by A483;
hence x in Segment ((h0 /. i),(h0 /. (i + 1)),P) by A484, Def1; :: thesis:

end;

then W = g2 .: Q1 by A337, A454;
hence diameter W < e by A31, A433, A444; :: thesis:

end;

suppose A485: i = len h1 ; :: thesis:

A486: (i + 1) - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by A36, A338, XREAL_1:9;
then 1 <= (i + 1) -' (len h11) by A39, A339, A485, XREAL_1:233;
then 1 < ((i + 1) -' (len h11)) + (2 - 1) by NAT_1:13;
then A487: 0 < (((i + 1) -' (len h11)) + 2) - 1 ;
i in dom h0 by A335, A336, FINSEQ_3:25;
then A488: h0 /. i = h0 . i by PARTFUN1:def 6;
A489: h0 . i = E-max P by A39, A255, A335, A485, FINSEQ_1:64;
set j = ((i -' (len h11)) + 2) -' 1;
A490: 0 + 2 <= (i -' (len h11)) + 2 by XREAL_1:6;
then A491: (((i -' (len h11)) + 2) -' 1) + 1 = ((((i -' (len h11)) + 1) + 1) - 1) + 1 by Lm1, NAT_D:39, NAT_D:42
.= (i -' (len h11)) + (1 + 1) ;
A492: (len h1) -' (len h11) = (len h11) - (len h11) by A39, XREAL_0:def 2;
then A493: (0 + 2) - 1 = (((len h1) -' (len h11)) + 2) - 1 ;
then A494: h0 . i = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by A24, A26, A485, A489, NAT_D:39;
A495: i - (len h11) = i -' (len h11) by A39, A485, XREAL_1:233;
i - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A39, A47, A36, A52, A55, A57, A336, XREAL_1:9;
then A496: (i -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A495, XREAL_1:6;
i - (len h11) < ((len h11) + ((len h2) - 2)) - (len h11) by A47, A36, A52, A55, A57, A336, XREAL_1:9;
then A497: (i - (len h11)) + 2 < ((len h2) - 2) + 2 by XREAL_1:6;
then A498: (((i -' (len h11)) + 2) -' 1) + 1 < len h2 by A39, A485, A491, XREAL_0:def 2;
A499: h0 . (i + 1) = (mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) by A39, A36, A338, A485, FINSEQ_1:23;
len h2 < (len h2) + 1 by NAT_1:13;
then A500: (len h2) - 1 < ((len h2) + 1) - 1 by XREAL_1:9;
i + 1 in dom h0 by A338, A340, FINSEQ_3:25;
then A501: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 6;
A502: 1 <= ((i -' (len h11)) + 2) -' 1 by A490, Lm1, NAT_D:42;
then A503: 1 < (((i -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
then A504: (((i -' (len h11)) + 2) -' 1) + 1 in dom h2 by A496, A491, FINSEQ_3:25;
then A505: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by FUNCT_1:def 3;
then A506: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) <= 1 by A29, BORSUK_1:40, XXREAL_1:1;
((i -' (len h11)) + 2) -' 1 <= len h21 by A47, A496, NAT_D:44;
then A507: ((i -' (len h11)) + 2) -' 1 in dom h2 by A46, A502, FINSEQ_3:25;
then A508: h2 . (((i -' (len h11)) + 2) -' 1) in rng h2 by FUNCT_1:def 3;
then g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) in rng g2 by A131, A29, BORSUK_1:40, FUNCT_1:def 3;
then A509: h0 . i in Lower_Arc P by A23, A24, A26, A485, A489, A493, NAT_D:39;
A510: h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) = h2 . ((((i -' (len h11)) + 2) -' 1) + 1) by A496, A491, A503, FINSEQ_4:15;
((i -' (len h11)) + 2) - 1 <= (len h2) - 1 by A496, XREAL_1:9;
then A511: ((i -' (len h11)) + 2) - 1 < len h2 by A500, XXREAL_0:2;
then A512: ((i -' (len h11)) + 2) -' 1 < len h2 by A490, Lm1, NAT_D:39, NAT_D:42;
then h2 /. (((i -' (len h11)) + 2) -' 1) = h2 . (((i -' (len h11)) + 2) -' 1) by A490, Lm1, FINSEQ_4:15, NAT_D:42;
then reconsider Q1 = [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] as Subset of I[01] by A29, A508, A505, A510, BORSUK_1:40, XXREAL_2:def 12;
A513: (i + 1) - (len h11) = (i + 1) -' (len h11) by A39, A339, A485, XREAL_1:233;
(((i -' (len h11)) + 2) -' 1) + 1 = (((i - (len h11)) + 2) - 1) + 1 by A39, A485, Lm1, XREAL_0:def 2
.= (((i + 1) -' (len h11)) + 2) -' 1 by A513, A487, XREAL_0:def 2 ;
then A514: h0 . (i + 1) = h21 . ((((i -' (len h11)) + 2) -' 1) + 1) by A39, A48, A56, A50, A54, A485, A499, A513, A486, FINSEQ_6:118;
then A515: h0 . (i + 1) = g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) by A504, FUNCT_1:13;
then A516: h0 . (i + 1) in Lower_Arc P by A23, A131, A29, A505, BORSUK_1:40, FUNCT_1:def 3;
A517: h21 . (((i -' (len h11)) + 2) -' 1) = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by A507, FUNCT_1:13;
A518: Segment ((h0 /. i),(h0 /. (i + 1)),P) c= g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).]

proof

(((i -' (len h11)) + 2) -' 1) + 1 < len h2 by A39, A485, A497, A491, XREAL_0:def 2;
then ((i -' (len h11)) + 2) -' 1 < len h2 by NAT_1:13;
then A519: h0 /. i <> W-min P by A46, A34, A35, A32, A507, A517, A494, A488;
A520: g2 . (h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)) = h0 /. (i + 1) by A496, A491, A503, A515, A501, FINSEQ_4:15;
h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by A504, FUNCT_1:def 3;
then A521: ( 0 <= h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) & h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) <= 1 ) by A29, A510, BORSUK_1:40, XXREAL_1:1;
A522: h0 /. (i + 1) in Lower_Arc P by A23, A131, A29, A515, A505, A501, BORSUK_1:40, FUNCT_1:def 3;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A523: x in Segment ((h0 /. i),(h0 /. (i + 1)),P) ; :: thesis:
h0 /. (i + 1) <> W-min P by A46, A34, A35, A32, A498, A514, A504, A501;
then x in { p where p is Point of (TOP-REAL 2) : ( LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) } by A523, Def1;
then consider p being Point of (TOP-REAL 2) such that
A524: p = x and
A525: LE h0 /. i,p,P and
A526: LE p,h0 /. (i + 1),P ;
A527: ( ( h0 /. i in Upper_Arc P & p in Lower_Arc P & not p = W-min P ) or ( h0 /. i in Upper_Arc P & p in Upper_Arc P & LE h0 /. i,p, Upper_Arc P, W-min P, E-max P ) or ( h0 /. i in Lower_Arc P & p in Lower_Arc P & not p = W-min P & LE h0 /. i,p, Lower_Arc P, E-max P, W-min P ) ) by A525, JORDAN6:def 10;
dom (g1 * h1) c= dom h0 by FINSEQ_1:26;
then A528: h0 /. i = E-max P by A254, A485, A489, PARTFUN1:def 6;

A529: now :: thesis:

assume A530: not p in Lower_Arc P ; :: thesis:
then p = E-max P by A3, A527, A528, JORDAN6:55;
hence contradiction by A1, A530, Th1; :: thesis:

end;

A531: now :: thesis:

assume p in Upper_Arc P ; :: thesis:
then p in (Upper_Arc P) /\ (Lower_Arc P) by A529, XBOOLE_0:def 4;
then A532: p in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
p <> W-min P by A3, A527, A519, JORDAN6:54;
hence p = E-max P by A532, TARSKI:def 2; :: thesis:

end;

then p in rng g2 by A1, A23, A525, Th1, JORDAN6:def 10;
then consider z being object such that
A533: z in dom g2 and
A534: p = g2 . z by FUNCT_1:def 3;
reconsider rz = z as Real by A131, A533;
0 <= rz by A533, BORSUK_1:40, XXREAL_1:1;
then A535: h2 /. (((i -' (len h11)) + 2) -' 1) <= rz by A26, A485, A511, A492, Lm1, FINSEQ_4:15;
A536: not h0 /. (i + 1) = E-max P by A46, A76, A77, A32, A503, A514, A504, A501;

now :: thesis:

assume h0 /. (i + 1) in Upper_Arc P ; :: thesis:
then h0 /. (i + 1) in (Upper_Arc P) /\ (Lower_Arc P) by A522, XBOOLE_0:def 4;
then h0 /. (i + 1) in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
then h21 . ((((i -' (len h11)) + 2) -' 1) + 1) = W-min P by A514, A501, A536, TARSKI:def 2;
hence contradiction by A46, A34, A35, A32, A498, A504; :: thesis:

end;

then ( ( p in Lower_Arc P & h0 /. (i + 1) in Lower_Arc P & not h0 /. (i + 1) = W-min P & LE p,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P ) or ( p in Upper_Arc P & h0 /. (i + 1) in Lower_Arc P & not h0 /. (i + 1) = W-min P ) ) by A526, JORDAN6:def 10;
then A537: LE p,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P by A21, A531, JORDAN5C:10;
rz <= 1 by A533, BORSUK_1:40, XXREAL_1:1;
then rz <= h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) by A22, A23, A24, A25, A537, A534, A520, A521, Th19;
then rz in [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] by A535, XXREAL_1:1;
hence x in g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] by A524, A533, A534, FUNCT_1:def 6; :: thesis:

end;

A538: g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) = h0 /. (i + 1) by A514, A504, A501, FUNCT_1:13;
g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] c= Segment ((h0 /. i),(h0 /. (i + 1)),P)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] ; :: thesis:
then consider y being object such that
A539: y in dom g2 and
A540: y in [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] and
A541: x = g2 . y by FUNCT_1:def 6;
reconsider sy = y as Real by A540;
A542: sy <= h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) by A540, XXREAL_1:1;
A543: x in Lower_Arc P by A23, A539, A541, FUNCT_1:def 3;
then reconsider p1 = x as Point of (TOP-REAL 2) ;
A544: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) <> 1 by A27, A30, A34, A498, A504, FUNCT_1:def 4;

A545: now :: thesis:

assume p1 = W-min P ; :: thesis:
then 1 = sy by A22, A25, A227, A539, A541;
hence contradiction by A506, A510, A542, A544, XXREAL_0:1; :: thesis:

end;

A546: ( 0 <= sy & sy <= 1 ) by A539, BORSUK_1:40, XXREAL_1:1;
then LE h0 /. i,p1, Lower_Arc P, E-max P, W-min P by A21, A22, A23, A24, A25, A489, A488, A541, Th18;
then A547: LE h0 /. i,p1,P by A488, A509, A543, A545, JORDAN6:def 10;
A548: h0 /. (i + 1) <> W-min P by A46, A34, A35, A32, A498, A514, A504, A501;
LE p1,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P by A21, A22, A23, A24, A25, A538, A506, A510, A541, A542, A546, Th18;
then LE p1,h0 /. (i + 1),P by A501, A516, A543, A548, JORDAN6:def 10;
then x in { p where p is Point of (TOP-REAL 2) : ( LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) } by A547;
hence x in Segment ((h0 /. i),(h0 /. (i + 1)),P) by A548, Def1; :: thesis:

end;

then W = g2 .: Q1 by A337, A518;
hence diameter W < e by A31, A502, A512; :: thesis:

end;

A549: len h0 = (len h1) + ((len h2) - 2) by A38, A47, A36, A52, A55, A57, FINSEQ_3:29;
thus for W being Subset of (Euclid 2) st W = Segment ((h0 /. (len h0)),(h0 /. 1),P) holds
diameter W < e :: thesis:

proof

set i = len h0;
let W be Subset of (Euclid 2); :: thesis:
set j = (((len h0) -' (len h11)) + 2) -' 1;
A550: 0 + 2 <= ((len h0) -' (len h11)) + 2 by XREAL_1:6;
then A551: 1 <= (((len h0) -' (len h11)) + 2) -' 1 by Lm1, NAT_D:42;
((len h11) + 1) - (len h11) <= (len h0) - (len h11) by A47, A36, A52, A55, A57, A62, XXREAL_0:2;
then 1 <= (len h0) -' (len h11) by NAT_D:39;
then 1 + 2 <= ((len h0) -' (len h11)) + 2 by XREAL_1:6;
then A552: (1 + 2) - 1 <= (((len h0) -' (len h11)) + 2) - 1 by XREAL_1:9;
len h0 <= (len h11) + (len (mid (h21,2,((len h21) -' 1)))) by FINSEQ_1:22;
then A553: h0 . (len h0) = (mid (h21,2,((len h21) -' 1))) . ((len h0) - (len h11)) by A39, A64, FINSEQ_1:23;
A554: (len h0) - (len h11) = (len h0) -' (len h11) by A39, A65, XREAL_1:233;
then (((len h0) -' (len h11)) + 2) -' 1 <= len h21 by A36, A52, A55, A57, NAT_D:44;
then A555: (((len h0) -' (len h11)) + 2) -' 1 in dom h2 by A46, A551, FINSEQ_3:25;
then A556: h2 . ((((len h0) -' (len h11)) + 2) -' 1) in rng h2 by FUNCT_1:def 3;
( (len h0) - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) & ((len h1) + 1) - (len h1) <= (len h0) - (len h1) ) by A549, A62, FINSEQ_1:22, XXREAL_0:2;
then A557: h0 . (len h0) = h21 . ((((len h0) -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A553, A554, FINSEQ_6:118;
then A558: h0 . (len h0) = g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) by A555, FUNCT_1:13;
then A559: h0 . (len h0) in Lower_Arc P by A23, A131, A29, A556, BORSUK_1:40, FUNCT_1:def 3;
A560: 2 -' 1 <= (((len h0) -' (len h11)) + 2) -' 1 by A550, NAT_D:42;
then A561: 1 < ((((len h0) -' (len h11)) + 2) -' 1) + 1 by Lm1, NAT_1:13;
then A562: h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1) = h2 . (((((len h0) -' (len h11)) + 2) -' 1) + 1) by A47, A36, A52, A55, A57, A554, FINSEQ_4:15;
len h2 < (len h2) + 1 by NAT_1:13;
then A563: (len h2) - 1 < ((len h2) + 1) - 1 by XREAL_1:9;
then A564: h2 /. ((((len h0) -' (len h11)) + 2) -' 1) = h2 . ((((len h0) -' (len h11)) + 2) -' 1) by A47, A36, A52, A55, A57, A554, A560, Lm1, FINSEQ_4:15;
((((len h0) -' (len h11)) + 2) -' 1) + 1 in dom h2 by A46, A36, A52, A55, A57, A554, A561, FINSEQ_3:25;
then h2 . (((((len h0) -' (len h11)) + 2) -' 1) + 1) in rng h2 by FUNCT_1:def 3;
then reconsider Q1 = [.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).] as Subset of I[01] by A29, A556, A564, A562, BORSUK_1:40, XXREAL_2:def 12;
len h0 in dom h0 by A66, FINSEQ_3:25;
then A565: h0 /. (len h0) = h0 . (len h0) by PARTFUN1:def 6;
(((len h0) -' (len h11)) + 2) -' 1 = (((len h0) -' (len h11)) + 2) - 1 by A550, Lm1, NAT_D:39, NAT_D:42;
then A566: 1 < (((len h0) -' (len h11)) + 2) -' 1 by A552, XXREAL_0:2;

A567: now :: thesis:

assume h0 . (len h0) in Upper_Arc P ; :: thesis:
then h0 . (len h0) in (Upper_Arc P) /\ (Lower_Arc P) by A559, XBOOLE_0:def 4;
then h0 . (len h0) in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
then ( h0 . (len h0) = W-min P or h0 . (len h0) = E-max P ) by TARSKI:def 2;
hence contradiction by A46, A47, A76, A34, A77, A35, A36, A52, A55, A57, A32, A554, A557, A563, A566, A555; :: thesis:

end;

A568: h2 . ((((len h0) -' (len h11)) + 2) -' 1) <= 1 by A29, A556, BORSUK_1:40, XXREAL_1:1;
A569: Segment ((h0 /. (len h0)),(h0 /. 1),P) c= g2 .: [.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A570: x in Segment ((h0 /. (len h0)),(h0 /. 1),P) ; :: thesis:
h0 /. 1 = W-min P by A72, A67, PARTFUN1:def 6;
then A571: x in { p where p is Point of (TOP-REAL 2) : ( LE h0 /. (len h0),p,P or ( h0 /. (len h0) in P & p = W-min P ) ) } by A570, Def1;
A572: ((((len h0) -' (len h11)) + 2) -' 1) + 1 in dom h2 by A46, A36, A52, A55, A57, A554, A561, FINSEQ_3:25;
( (((len h0) -' (len h11)) + 2) -' 1 < ((((len h0) -' (len h11)) + 2) -' 1) + 1 & (((len h0) -' (len h11)) + 2) -' 1 in dom h2 ) by A47, A36, A52, A55, A57, A554, A560, A563, Lm1, FINSEQ_3:25;
then h2 . ((((len h0) -' (len h11)) + 2) -' 1) < h2 . (((((len h0) -' (len h11)) + 2) -' 1) + 1) by A30, A572, SEQM_3:def 1;
then A573: h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1) in [.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).] by A564, A562, XXREAL_1:1;
consider p being Point of (TOP-REAL 2) such that
A574: p = x and
A575: ( LE h0 /. (len h0),p,P or ( h0 /. (len h0) in P & p = W-min P ) ) by A571;
A576: h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1) = 1 by A27, A47, A34, A36, A52, A55, A57, A554, PARTFUN1:def 6;

now :: thesis:

per cases by A575;

suppose A577: ( LE h0 /. (len h0),p,P & ( p <> W-min P or not h0 /. (len h0) in P ) ) ; :: thesis:

then p in Lower_Arc P by A567, A565, JORDAN6:def 10;
then consider z being object such that
A578: z in dom g2 and
A579: p = g2 . z by A23, FUNCT_1:def 3;
take z = z; :: thesis:
thus z in dom g2 by A578; :: thesis:
reconsider rz = z as Real by A131, A578;
A580: rz <= 1 by A578, BORSUK_1:40, XXREAL_1:1;
then A581: rz <= h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1) by A27, A47, A36, A52, A55, A57, A554, A561, FINSEQ_4:15;
A582: LE h0 /. (len h0),p, Lower_Arc P, E-max P, W-min P by A567, A565, A577, JORDAN6:def 10;
0 <= rz by A578, BORSUK_1:40, XXREAL_1:1;
then h2 /. ((((len h0) -' (len h11)) + 2) -' 1) <= rz by A22, A23, A24, A25, A558, A568, A565, A564, A582, A579, A580, Th19;
hence ( z in [.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).] & x = g2 . z ) by A574, A579, A581, XXREAL_1:1; :: thesis:

end;

suppose ( h0 /. (len h0) in P & p = W-min P ) ; :: thesis:

hence ex y being object st
( y in dom g2 & y in [.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).] & x = g2 . y ) by A25, A227, A574, A573, A576; :: thesis:

end;

hence x in g2 .: [.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).] by FUNCT_1:def 6; :: thesis:

end;

A583: ( 0 <= h2 . ((((len h0) -' (len h11)) + 2) -' 1) & h2 . ((((len h0) -' (len h11)) + 2) -' 1) <= 1 ) by A29, A556, BORSUK_1:40, XXREAL_1:1;
A584: g2 .: [.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).] c= Segment ((h0 /. (len h0)),(h0 /. 1),P)

proof

A585: (Upper_Arc P) \/ (Lower_Arc P) = P by A1, JORDAN6:def 9;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in g2 .: [.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).] ; :: thesis:
then consider y being object such that
A586: y in dom g2 and
A587: y in [.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).] and
A588: x = g2 . y by FUNCT_1:def 6;
reconsider sy = y as Real by A587;
A589: x in Lower_Arc P by A23, A586, A588, FUNCT_1:def 3;
then reconsider p1 = x as Point of (TOP-REAL 2) ;
( h2 /. ((((len h0) -' (len h11)) + 2) -' 1) <= sy & sy <= 1 ) by A586, A587, BORSUK_1:40, XXREAL_1:1;
then A590: LE h0 /. (len h0),p1, Lower_Arc P, E-max P, W-min P by A21, A22, A23, A24, A25, A558, A565, A583, A564, A588, Th18;

now :: thesis:

per cases ;

case p1 = W-min P ; :: thesis:

hence ( LE h0 /. (len h0),p1,P or ( h0 /. (len h0) in P & p1 = W-min P ) ) by A559, A565, A585, XBOOLE_0:def 3; :: thesis:

end;

case p1 <> W-min P ; :: thesis:

hence ( LE h0 /. (len h0),p1,P or ( h0 /. (len h0) in P & p1 = W-min P ) ) by A559, A565, A589, A590, JORDAN6:def 10; :: thesis:

end;

then A591: x in { p where p is Point of (TOP-REAL 2) : ( LE h0 /. (len h0),p,P or ( h0 /. (len h0) in P & p = W-min P ) ) } ;
h0 /. 1 = W-min P by A72, A67, PARTFUN1:def 6;
hence x in Segment ((h0 /. (len h0)),(h0 /. 1),P) by A591, Def1; :: thesis:

end;

assume W = Segment ((h0 /. (len h0)),(h0 /. 1),P) ; :: thesis:
then W = g2 .: Q1 by A569, A584;
hence diameter W < e by A31, A47, A36, A52, A55, A57, A554, A560, A563, Lm1; :: thesis:

end;

A592: for i being Nat st 1 <= i & i + 1 < len h0 holds
LE h0 /. (i + 1),h0 /. (i + 2),P

proof

let i be Nat; :: thesis:
assume that
A593: 1 <= i and
A594: i + 1 < len h0 ; :: thesis:
A595: (i + 1) + 1 <= len h0 by A594, NAT_1:13;
A596: i + 1 < (i + 1) + 1 by NAT_1:13;
A597: 1 < i + 1 by A593, NAT_1:13;
then A598: 1 < (i + 1) + 1 by NAT_1:13;

per cases ;

suppose A599: i + 1 < len h1 ; :: thesis:

then A600: i + 1 in dom h1 by A597, FINSEQ_3:25;
then A601: h1 . (i + 1) in rng h1 by FUNCT_1:def 3;
then A602: ( 0 <= h1 . (i + 1) & h1 . (i + 1) <= 1 ) by A11, BORSUK_1:40, XXREAL_1:1;
A603: 1 < (i + 1) + 1 by A597, NAT_1:13;
then (i + 1) + 1 in dom h0 by A595, FINSEQ_3:25;
then A604: h0 /. ((i + 1) + 1) = h0 . ((i + 1) + 1) by PARTFUN1:def 6;
A605: (i + 1) + 1 <= len h1 by A599, NAT_1:13;
then A606: (i + 1) + 1 in dom h1 by A603, FINSEQ_3:25;
then A607: h1 . ((i + 1) + 1) in rng h1 by FUNCT_1:def 3;
then A608: h1 . ((i + 1) + 1) <= 1 by A11, BORSUK_1:40, XXREAL_1:1;
h0 . ((i + 1) + 1) = h11 . ((i + 1) + 1) by A39, A605, A603, FINSEQ_1:64;
then A609: h0 . ((i + 1) + 1) = g1 . (h1 . ((i + 1) + 1)) by A606, FUNCT_1:13;
then A610: h0 /. ((i + 1) + 1) in Upper_Arc P by A5, A132, A11, A607, A604, BORSUK_1:40, FUNCT_1:def 3;
i + 1 in dom h0 by A594, A597, FINSEQ_3:25;
then A611: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 6;
A612: h0 . (i + 1) = h11 . (i + 1) by A39, A597, A599, FINSEQ_1:64;
then A613: h0 . (i + 1) = g1 . (h1 . (i + 1)) by A600, FUNCT_1:13;
g1 . (h1 . (i + 1)) in rng g1 by A132, A11, A601, BORSUK_1:40, FUNCT_1:def 3;
then A614: h0 /. (i + 1) in Upper_Arc P by A5, A612, A600, A611, FUNCT_1:13;
h1 . (i + 1) < h1 . ((i + 1) + 1) by A12, A596, A600, A606, SEQM_3:def 1;
then LE h0 /. (i + 1),h0 /. ((i + 1) + 1), Upper_Arc P, W-min P, E-max P by A3, A4, A5, A6, A7, A613, A602, A609, A608, A611, A604, Th18;
hence LE h0 /. (i + 1),h0 /. (i + 2),P by A614, A610, JORDAN6:def 10; :: thesis:

end;

suppose A615: i + 1 >= len h1 ; :: thesis:

per cases by A615, XXREAL_0:1;

suppose A616: i + 1 > len h1 ; :: thesis:

set j = (((i + 1) -' (len h11)) + 2) -' 1;
A617: ((i + 1) + 1) - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by A36, A595, XREAL_1:9;
A618: 0 + 2 <= ((i + 1) -' (len h11)) + 2 by XREAL_1:6;
then A619: 1 <= (((i + 1) -' (len h11)) + 2) -' 1 by Lm1, NAT_D:42;
A620: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 = ((((i + 1) -' (len h11)) + (1 + 1)) - 1) + 1 by A618, Lm1, NAT_D:39, NAT_D:42
.= ((i + 1) -' (len h11)) + 2 ;
A621: (len h1) + 1 <= i + 1 by A616, NAT_1:13;
then A622: ((len h1) + 1) - (len h1) <= (i + 1) - (len h1) by XREAL_1:9;
A623: (i + 1) - (len h11) = (i + 1) -' (len h11) by A39, A616, XREAL_1:233;
(i + 1) + 1 > len h11 by A39, A616, NAT_1:13;
then A624: ((i + 1) + 1) - (len h11) = ((i + 1) + 1) -' (len h11) by XREAL_1:233;
A625: (len h1) + 1 <= (i + 1) + 1 by A621, NAT_1:13;
then A626: ((len h1) + 1) - (len h1) <= ((i + 1) + 1) - (len h1) by XREAL_1:9;
then 1 < (((i + 1) + 1) -' (len h11)) + (2 - 1) by A39, A624, NAT_1:13;
then A627: 0 < ((((i + 1) + 1) -' (len h11)) + 2) - 1 ;
(((i + 1) -' (len h11)) + 2) -' 1 = (((i + 1) -' (len h11)) + 2) - 1 by A618, Lm1, NAT_D:39, NAT_D:42;
then A628: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 = ((((i + 1) + 1) -' (len h11)) + 2) -' 1 by A623, A624, A627, XREAL_0:def 2;
(i + 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A39, A47, A36, A52, A55, A57, A594, XREAL_1:9;
then A629: ((i + 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A623, XREAL_1:6;
then (((i + 1) -' (len h11)) + 2) -' 1 <= len h21 by A47, NAT_D:44;
then A630: (((i + 1) -' (len h11)) + 2) -' 1 in dom h2 by A46, A619, FINSEQ_3:25;
2 -' 1 <= (((i + 1) -' (len h11)) + 2) -' 1 by A618, NAT_D:42;
then 1 < ((((i + 1) -' (len h11)) + 2) -' 1) + 1 by Lm1, NAT_1:13;
then A631: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 in dom h2 by A629, A620, FINSEQ_3:25;
then A632: h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1) in rng h2 by FUNCT_1:def 3;
then A633: h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1) <= 1 by A29, BORSUK_1:40, XXREAL_1:1;
(((i + 1) -' (len h11)) + 2) -' 1 < ((((i + 1) -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
then A634: h2 . ((((i + 1) -' (len h11)) + 2) -' 1) < h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1) by A30, A630, A631, SEQM_3:def 1;
A635: i + 1 <= (len h11) + (len (mid (h21,2,((len h21) -' 1)))) by A594, FINSEQ_1:22;
(len h11) + 1 <= i + 1 by A39, A616, NAT_1:13;
then A636: h0 . (i + 1) = (mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) by A635, FINSEQ_1:23;
(i + 1) - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by A635, XREAL_1:9;
then h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A636, A623, A622, FINSEQ_6:118;
then A637: h0 . (i + 1) = g2 . (h2 . ((((i + 1) -' (len h11)) + 2) -' 1)) by A630, FUNCT_1:13;
A638: h2 . ((((i + 1) -' (len h11)) + 2) -' 1) in rng h2 by A630, FUNCT_1:def 3;
then A639: h0 . (i + 1) in Lower_Arc P by A23, A131, A29, A637, BORSUK_1:40, FUNCT_1:def 3;
(i + 1) + 1 in dom h0 by A595, A598, FINSEQ_3:25;
then A640: h0 /. ((i + 1) + 1) = h0 . ((i + 1) + 1) by PARTFUN1:def 6;
h0 . ((i + 1) + 1) = (mid (h21,2,((len h21) -' 1))) . (((i + 1) + 1) - (len h11)) by A39, A36, A595, A625, FINSEQ_1:23;
then A641: h0 . ((i + 1) + 1) = h21 . (((((i + 1) + 1) -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A624, A617, A626, FINSEQ_6:118;
then A642: h0 . ((i + 1) + 1) = g2 . (h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1)) by A628, A631, FUNCT_1:13;
then A643: h0 . ((i + 1) + 1) in Lower_Arc P by A23, A131, A29, A632, BORSUK_1:40, FUNCT_1:def 3;
(i + 1) - (len h11) < ((len h11) + ((len h2) - 2)) - (len h11) by A47, A36, A52, A55, A57, A594, XREAL_1:9;
then ((i + 1) - (len h11)) + 2 < ((len h2) - 2) + 2 by XREAL_1:6;
then A644: h0 /. ((i + 1) + 1) <> W-min P by A46, A34, A35, A32, A623, A641, A620, A628, A631, A640;
i + 1 in dom h0 by A594, A597, FINSEQ_3:25;
then A645: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 6;
( 0 <= h2 . ((((i + 1) -' (len h11)) + 2) -' 1) & h2 . ((((i + 1) -' (len h11)) + 2) -' 1) <= 1 ) by A29, A638, BORSUK_1:40, XXREAL_1:1;
then LE h0 /. (i + 1),h0 /. ((i + 1) + 1), Lower_Arc P, E-max P, W-min P by A21, A22, A23, A24, A25, A637, A642, A634, A645, A640, A633, Th18;
hence LE h0 /. (i + 1),h0 /. (i + 2),P by A645, A640, A639, A643, A644, JORDAN6:def 10; :: thesis:

end;

suppose A646: i + 1 = len h1 ; :: thesis:

then (len h1) + 1 <= (len h11) + (len (mid (h21,2,((len h21) -' 1)))) by A595, FINSEQ_1:22;
then A647: ((i + 1) + 1) - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by A646, XREAL_1:9;
then 1 <= ((i + 1) + 1) -' (len h11) by A39, A596, A646, XREAL_1:233;
then 1 < (((i + 1) + 1) -' (len h11)) + (2 - 1) by NAT_1:13;
then A648: 0 < ((((i + 1) + 1) -' (len h11)) + 2) - 1 ;
A649: ((i + 1) + 1) - (len h11) = ((i + 1) + 1) -' (len h11) by A39, A596, A646, XREAL_1:233;
len h1 in dom h0 by A594, A597, A646, FINSEQ_3:25;
then A650: h0 /. (len h1) = h0 . (len h1) by PARTFUN1:def 6;
set j = (((i + 1) -' (len h11)) + 2) -' 1;
A651: 0 + 2 <= ((i + 1) -' (len h11)) + 2 by XREAL_1:6;
then A652: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 = ((((i + 1) -' (len h11)) + (1 + 1)) - 1) + 1 by Lm1, NAT_D:39, NAT_D:42
.= ((i + 1) -' (len h11)) + (1 + 1) ;
2 -' 1 <= (((i + 1) -' (len h11)) + 2) -' 1 by A651, NAT_D:42;
then A653: 1 < ((((i + 1) -' (len h11)) + 2) -' 1) + 1 by Lm1, NAT_1:13;
( (len h1) - (len h11) = (len h1) -' (len h11) & (i + 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) ) by A39, A47, A36, A52, A55, A57, A594, XREAL_1:9, XREAL_1:233;
then ((i + 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A646, XREAL_1:6;
then A654: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 in dom h2 by A652, A653, FINSEQ_3:25;
then A655: h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1) in rng h2 by FUNCT_1:def 3;
h0 . (len h1) = E-max P by A39, A255, A597, A646, FINSEQ_1:64;
then A656: h0 . (i + 1) in Upper_Arc P by A1, A646, Th1;
(i + 1) + 1 in dom h0 by A595, A598, FINSEQ_3:25;
then A657: h0 /. ((i + 1) + 1) = h0 . ((i + 1) + 1) by PARTFUN1:def 6;
h0 . ((i + 1) + 1) = (mid (h21,2,((len h21) -' 1))) . (((i + 1) + 1) - (len h11)) by A39, A36, A595, A646, FINSEQ_1:23;
then A658: h0 . ((i + 1) + 1) = h21 . (((((i + 1) + 1) -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A646, A649, A647, FINSEQ_6:118;
A659: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 = ((((i + 1) - (len h11)) + 2) - 1) + 1 by A39, A646, Lm1, XREAL_0:def 2
.= ((((i + 1) + 1) -' (len h11)) + 2) -' 1 by A649, A648, XREAL_0:def 2 ;
then h0 . ((i + 1) + 1) = g2 . (h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1)) by A658, A654, FUNCT_1:13;
then A660: h0 . ((i + 1) + 1) in Lower_Arc P by A23, A131, A29, A655, BORSUK_1:40, FUNCT_1:def 3;
(i + 1) - (len h11) < ((len h11) + ((len h2) - 2)) - (len h11) by A47, A36, A52, A55, A57, A594, XREAL_1:9;
then ((i + 1) - (len h11)) + 2 < ((len h2) - 2) + 2 by XREAL_1:6;
then ((((i + 1) -' (len h11)) + 2) -' 1) + 1 < len h2 by A39, A646, A652, XREAL_0:def 2;
then h0 /. ((i + 1) + 1) <> W-min P by A46, A34, A35, A32, A658, A659, A654, A657;
hence LE h0 /. (i + 1),h0 /. (i + 2),P by A646, A650, A657, A660, A656, JORDAN6:def 10; :: thesis:

end;

thus for i being Nat st 1 <= i & i + 1 < len h0 holds
(Segment ((h0 /. i),(h0 /. (i + 1)),P)) /\ (Segment ((h0 /. (i + 1)),(h0 /. (i + 2)),P)) = {(h0 /. (i + 1))} :: thesis:

proof

let i be Nat; :: thesis:
assume A661: ( 1 <= i & i + 1 < len h0 ) ; :: thesis:
then A662: ( LE h0 /. i,h0 /. (i + 1),P & h0 /. (i + 1) <> W-min P ) by A256;
( h0 /. i <> h0 /. (i + 1) & LE h0 /. (i + 1),h0 /. (i + 2),P ) by A592, A256, A661;
hence (Segment ((h0 /. i),(h0 /. (i + 1)),P)) /\ (Segment ((h0 /. (i + 1)),(h0 /. (i + 2)),P)) = {(h0 /. (i + 1))} by A1, A662, Th10; :: thesis:

end;

A663: 2 in dom h0 by A201, FINSEQ_3:25;
(len h0) -' 1 <> 1 by A59, Lm2;
then A664: h0 /. ((len h0) -' 1) <> h0 /. 1 by A67, A78, A203, PARTFUN2:10;
A665: len h1 in dom h1 by A16, FINSEQ_3:25;
thus (Segment ((h0 /. (len h0)),(h0 /. 1),P)) /\ (Segment ((h0 /. 1),(h0 /. 2),P)) = {(h0 /. 1)} :: thesis:

proof

defpred S₁[ Nat] means ( $1 + 2 <= len h0 implies LE h0 /. 2,h0 /. ($1 + 2),P );
set j = (((len h0) -' (len h11)) + 2) -' 1;
A666: (len h0) - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by FINSEQ_1:22;
A667: h0 /. 2 = h0 . 2 by A663, PARTFUN1:def 6;
A668: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A669: ( k + 2 <= len h0 implies LE h0 /. 2,h0 /. (k + 2),P ) ; :: thesis:

now :: thesis:

A670: (k + 1) + 1 = k + 2 ;
A671: (k + 1) + 2 = (k + 2) + 1 ;
assume A672: (k + 1) + 2 <= len h0 ; :: thesis:
then k + 2 < len h0 by A671, NAT_1:13;
then LE h0 /. (k + 2),h0 /. ((k + 2) + 1),P by A592, A671, A670, NAT_1:11;
hence LE h0 /. 2,h0 /. ((k + 1) + 2),P by A1, A669, A672, JORDAN6:58, NAT_1:13; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

(len h0) -' 2 = (len h0) - 2 by A65, A14, XREAL_1:233, XXREAL_0:2;
then A673: ((len h0) -' 2) + 2 = len h0 ;
0 + 2 <= ((len h0) -' (len h11)) + 2 by XREAL_1:6;
then A674: 1 <= (((len h0) -' (len h11)) + 2) -' 1 by Lm1, NAT_D:42;
(((len h0) -' (len h11)) + 2) -' 1 <= len h21 by A36, A52, A55, A57, A252, NAT_D:44;
then A675: (((len h0) -' (len h11)) + 2) -' 1 in dom h2 by A46, A674, FINSEQ_3:25;
( h0 . 2 = g1 . (h1 . 2) & h1 . 2 in rng h1 ) by A15, A40, FUNCT_1:13, FUNCT_1:def 3;
then A676: h0 /. 2 in Upper_Arc P by A5, A132, A11, A667, BORSUK_1:40, FUNCT_1:def 3;
(Upper_Arc P) \/ (Lower_Arc P) = P by A1, JORDAN6:50;
then h0 /. 2 in P by A676, XBOOLE_0:def 3;
then A677: S₁[ 0 ] by A1, JORDAN6:56;
A678: for i being Nat holds S₁[i] from NAT_1:sch 2(A677, A668);
A679: h11 . 2 <> W-min P by A38, A17, A71, A15, A20;
( ((len h1) + 1) - (len h1) <= (len h0) - (len h1) & h0 . (len h0) = (mid (h21,2,((len h21) -' 1))) . ((len h0) - (len h11)) ) by A39, A36, A549, A62, A64, FINSEQ_1:23, XXREAL_0:2;
then h0 . (len h0) = h21 . ((((len h0) -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A252, A666, FINSEQ_6:118;
then A680: h0 . (len h0) = g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) by A675, FUNCT_1:13;

A681: now :: thesis:

h2 . ((((len h0) -' (len h11)) + 2) -' 1) in rng h2 by A675, FUNCT_1:def 3;
then A682: g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) in rng g2 by A131, A29, BORSUK_1:40, FUNCT_1:def 3;
assume h0 /. 2 = h0 /. (len h0) ; :: thesis:
then h0 /. 2 in (Upper_Arc P) /\ (Lower_Arc P) by A23, A75, A676, A680, A682, XBOOLE_0:def 4;
then h0 /. 2 in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
then h11 . 2 = E-max P by A40, A679, A667, TARSKI:def 2;
hence contradiction by A38, A665, A255, A14, A15, A20; :: thesis:

end;

h0 /. 2 <> W-min P by A663, A40, A679, PARTFUN1:def 6;
hence (Segment ((h0 /. (len h0)),(h0 /. 1),P)) /\ (Segment ((h0 /. 1),(h0 /. 2),P)) = {(h0 /. 1)} by A1, A73, A681, A678, A673, Th12; :: thesis:

end;

A683: ((len h0) -' 1) + 1 = len h0 by A16, A65, XREAL_1:235, XXREAL_0:2;
then ( LE h0 /. ((len h0) -' 1),h0 /. (((len h0) -' 1) + 1),P & h0 /. (((len h0) -' 1) + 1) <> W-min P ) by A256, A202;
hence (Segment ((h0 /. ((len h0) -' 1)),(h0 /. (len h0)),P)) /\ (Segment ((h0 /. (len h0)),(h0 /. 1),P)) = {(h0 /. (len h0))} by A1, A73, A683, A664, Th11; :: thesis:
LE h0 /. ((len h0) -' 1),h0 /. (((len h0) -' 1) + 1),P by A256, A202, A200;
hence Segment ((h0 /. ((len h0) -' 1)),(h0 /. (len h0)),P) misses Segment ((h0 /. 1),(h0 /. 2),P) by A1, A683, A333, A229, A207, Th13; :: thesis:
thus for i, j being Nat st 1 <= i & i < j & j < len h0 & i,j aren't_adjacent holds
Segment ((h0 /. i),(h0 /. (i + 1)),P) misses Segment ((h0 /. j),(h0 /. (j + 1)),P) :: thesis:

proof

let i, j be Nat; :: thesis:
assume that
A684: 1 <= i and
A685: i < j and
A686: j < len h0 and
A687: i,j aren't_adjacent ; :: thesis:
A688: 1 < j by A684, A685, XXREAL_0:2;
i < len h0 by A685, A686, XXREAL_0:2;
then A689: i + 1 <= len h0 by NAT_1:13;
then A690: ( LE h0 /. i,h0 /. (i + 1),P & h0 /. i <> h0 /. (i + 1) ) by A256, A684;
A691: i + 1 <= j by A685, NAT_1:13;
then A692: i + 1 < len h0 by A686, XXREAL_0:2;
A693: not j = i + 1 by A687, GOBRD10:def 1;
then A694: i + 1 < j by A691, XXREAL_0:1;

A695: now :: thesis:

assume A696: h0 /. (i + 1) = h0 /. j ; :: thesis:

per cases ;

suppose A697: i + 1 <= len h1 ; :: thesis:

A698: 1 < i + 1 by A684, NAT_1:13;
then A699: i + 1 in dom h1 by A697, FINSEQ_3:25;
then A700: h1 . (i + 1) in rng h1 by FUNCT_1:def 3;
i + 1 in dom h0 by A689, A698, FINSEQ_3:25;
then A701: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 6;
A702: h0 . (i + 1) = h11 . (i + 1) by A39, A697, A698, FINSEQ_1:64;
then h0 . (i + 1) = g1 . (h1 . (i + 1)) by A699, FUNCT_1:13;
then A703: h0 . (i + 1) in Upper_Arc P by A5, A132, A11, A700, BORSUK_1:40, FUNCT_1:def 3;

per cases ;

suppose A704: j <= len h1 ; :: thesis:

j in dom h0 by A686, A688, FINSEQ_3:25;
then A705: h0 /. j = h0 . j by PARTFUN1:def 6;
( h0 . j = h11 . j & j in dom h1 ) by A39, A688, A704, FINSEQ_1:64, FINSEQ_3:25;
hence contradiction by A38, A20, A693, A696, A699, A701, A702, A705; :: thesis:

end;

suppose A706: j > len h1 ; :: thesis:

end;

suppose A720: i + 1 > len h1 ; :: thesis:

end;

A743: j + 1 <= len h0 by A686, NAT_1:13;
A744: 1 < i + 1 by A684, NAT_1:13;
A745: 1 <= i + 1 by A684, NAT_1:13;
A746: i + 1 < len h0 by A686, A691, XXREAL_0:2;
A747: LE h0 /. (i + 1),h0 /. j,P

proof

per cases ;

suppose A748: i + 1 <= len h1 ; :: thesis:

per cases ;

suppose A749: j <= len h1 ; :: thesis:

A750: 1 < j by A694, A745, XXREAL_0:2;
then A751: j in dom h1 by A749, FINSEQ_3:25;
then A752: h1 . j in rng h1 by FUNCT_1:def 3;
then A753: h1 . j <= 1 by A11, BORSUK_1:40, XXREAL_1:1;
j in dom h0 by A686, A750, FINSEQ_3:25;
then A754: h0 /. j = h0 . j by PARTFUN1:def 6;
h0 . j = h11 . j by A39, A749, A750, FINSEQ_1:64;
then A755: g1 . (h1 . j) = h0 /. j by A751, A754, FUNCT_1:13;
then A756: h0 /. j in Upper_Arc P by A5, A132, A11, A752, BORSUK_1:40, FUNCT_1:def 3;
i + 1 in dom h0 by A745, A692, FINSEQ_3:25;
then A757: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 6;
A758: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, JORDAN6:def 8;
A759: i + 1 in dom h1 by A745, A748, FINSEQ_3:25;
then A760: h1 . (i + 1) in rng h1 by FUNCT_1:def 3;
then A761: ( 0 <= h1 . (i + 1) & h1 . (i + 1) <= 1 ) by A11, BORSUK_1:40, XXREAL_1:1;
h0 . (i + 1) = h11 . (i + 1) by A39, A745, A748, FINSEQ_1:64;
then A762: g1 . (h1 . (i + 1)) = h0 /. (i + 1) by A759, A757, FUNCT_1:13;
then A763: h0 /. (i + 1) in Upper_Arc P by A5, A132, A11, A760, BORSUK_1:40, FUNCT_1:def 3;
h1 . (i + 1) <= h1 . j by A12, A694, A759, A751, SEQM_3:def 1;
then LE h0 /. (i + 1),h0 /. j, Upper_Arc P, W-min P, E-max P by A4, A5, A6, A7, A758, A762, A761, A755, A753, Th18;
hence LE h0 /. (i + 1),h0 /. j,P by A763, A756, JORDAN6:def 10; :: thesis:

end;

suppose A764: j > len h1 ; :: thesis:

end;

suppose A780: i + 1 > len h1 ; :: thesis:

end;

LE h0 /. j,h0 /. (j + 1),P by A256, A688, A743;
hence Segment ((h0 /. i),(h0 /. (i + 1)),P) misses Segment ((h0 /. j),(h0 /. (j + 1)),P) by A1, A690, A747, A695, Th13; :: thesis:

end;

let i be Nat; :: thesis:
assume that
A812: 1 < i and
A813: i + 1 < len h0 ; :: thesis:
A814: 1 < i + 1 by A812, NAT_1:13;
then A815: i + 1 in dom h0 by A813, FINSEQ_3:25;
A816: 1 <= (len h0) - (len h1) by A549, A62, XXREAL_0:2;

A817: now :: thesis:

assume A818: h0 /. (i + 1) = h0 /. (len h0) ; :: thesis:

per cases ;

suppose A819: i + 1 <= len h1 ; :: thesis:

end;

suppose A832: i + 1 > len h1 ; :: thesis:

set k = (((len h0) -' (len h11)) + 2) -' 1;
set j0 = (((i + 1) -' (len h11)) + 2) -' 1;
A833: 0 + 2 <= ((len h0) -' (len h11)) + 2 by XREAL_1:6;
then A834: 2 -' 1 <= (((len h0) -' (len h11)) + 2) -' 1 by NAT_D:42;
(((len h0) -' (len h11)) + 2) -' 1 <= len h21 by A36, A52, A55, A57, A252, NAT_D:44;
then A835: (((len h0) -' (len h11)) + 2) -' 1 in dom h2 by A46, A834, Lm1, FINSEQ_3:25;
i + 1 <= (len h11) + (len (mid (h21,2,((len h21) -' 1)))) by A813, FINSEQ_1:22;
then A836: (i + 1) - (len h11) <= ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by XREAL_1:9;
A837: (len h1) + 1 <= i + 1 by A832, NAT_1:13;
then ((len h11) + 1) - (len h11) <= (i + 1) - (len h11) by A39, XREAL_1:9;
then A838: (i + 1) -' (len h11) = (i + 1) - (len h11) by NAT_D:39;
(len h0) -' (len h11) = (len h0) - (len h11) by A36, A57, XREAL_0:def 2;
then (i + 1) -' (len h11) < (len h0) -' (len h11) by A813, A838, XREAL_1:9;
then A839: ((i + 1) -' (len h11)) + 2 < ((len h0) -' (len h11)) + 2 by XREAL_1:6;
1 <= i + 1 by A812, NAT_1:13;
then i + 1 in dom h0 by A813, FINSEQ_3:25;
then A840: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 6;
A841: (((len h0) -' (len h11)) + 2) -' 1 = (((len h0) -' (len h11)) + 2) - 1 by A833, Lm1, NAT_D:39, NAT_D:42;
A842: (i + 1) - (len h11) = (i + 1) -' (len h11) by A39, A832, XREAL_1:233;
(i + 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A39, A47, A36, A52, A55, A57, A813, XREAL_1:9;
then ((i + 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A39, A842, XREAL_1:6;
then A843: (((i + 1) -' (len h11)) + 2) -' 1 <= len h21 by A47, NAT_D:44;
A844: 0 + 2 <= ((i + 1) -' (len h11)) + 2 by XREAL_1:6;
then 2 -' 1 <= (((i + 1) -' (len h11)) + 2) -' 1 by NAT_D:42;
then A845: (((i + 1) -' (len h11)) + 2) -' 1 in dom h2 by A46, A843, Lm1, FINSEQ_3:25;
( h0 . (i + 1) = (mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) & ((len h1) + 1) - (len h1) <= (i + 1) - (len h1) ) by A39, A36, A813, A837, FINSEQ_1:23, XREAL_1:9;
then A846: h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A842, A836, FINSEQ_6:118;
(((i + 1) -' (len h11)) + 2) -' 1 = (((i + 1) -' (len h11)) + 2) - 1 by A844, Lm1, NAT_D:39, NAT_D:42;
then A847: (((i + 1) -' (len h11)) + 2) -' 1 < (((len h0) -' (len h11)) + 2) -' 1 by A841, A839, XREAL_1:9;
h0 . (len h0) = (mid (h21,2,((len h21) -' 1))) . ((len h0) - (len h11)) by A39, A36, A64, FINSEQ_1:23;
then h0 . (len h0) = h21 . ((((len h0) -' (len h11)) + 2) -' 1) by A47, A36, A51, A52, A49, A48, A53, A55, A57, A63, A252, FINSEQ_6:118;
hence contradiction by A46, A75, A32, A818, A846, A845, A840, A847, A835; :: thesis:

end;

h0 . (len h0) = (mid (h21,2,((len h21) -' 1))) . ((len h0) - (len h11)) by A39, A36, A64, FINSEQ_1:23;
then A848: h0 . (len h0) = h21 . ((((len h0) -' (len h11)) + 2) -' 1) by A39, A36, A48, A56, A50, A54, A816, A252, FINSEQ_6:118;
then A849: h0 . (len h0) in Lower_Arc P by A23, A131, A29, A253, BORSUK_1:40, FUNCT_1:def 3;
A850: LE h0 /. (i + 1),h0 /. (len h0),P

proof

per cases ;

suppose A851: i + 1 <= len h1 ; :: thesis:

then i + 1 in dom h1 by A814, FINSEQ_3:25;
then h1 . (i + 1) in rng h1 by FUNCT_1:def 3;
then A852: g1 . (h1 . (i + 1)) in rng g1 by A132, A11, BORSUK_1:40, FUNCT_1:def 3;
A853: h0 /. (i + 1) = h0 . (i + 1) by A815, PARTFUN1:def 6;
i + 1 in dom h1 by A814, A851, FINSEQ_3:25;
then A854: h11 . (i + 1) = g1 . (h1 . (i + 1)) by FUNCT_1:13;
h0 . (i + 1) = h11 . (i + 1) by A39, A814, A851, FINSEQ_1:64;
hence LE h0 /. (i + 1),h0 /. (len h0),P by A5, A75, A130, A849, A854, A853, A852, JORDAN6:def 10; :: thesis:

end;

suppose A855: i + 1 > len h1 ; :: thesis:

then (len h1) + 1 <= i + 1 by NAT_1:13;
then A856: ((len h1) + 1) - (len h1) <= (i + 1) - (len h1) by XREAL_1:9;
then A857: (i + 1) -' (len h11) = (i + 1) - (len h11) by A39, NAT_D:39;
A858: (i + 1) - (len h11) < ((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) by A36, A813, XREAL_1:9;
A859: i + 1 < (len h11) + (len (mid (h21,2,((len h21) -' 1)))) by A813, FINSEQ_1:22;
(len h11) + 1 <= i + 1 by A39, A855, NAT_1:13;
then A860: h0 . (i + 1) = (mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) by A859, FINSEQ_1:23
.= h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A39, A48, A56, A50, A54, A858, A856, A857, FINSEQ_6:118 ;
set j0 = (((i + 1) -' (len h11)) + 2) -' 1;
set k = (((len h0) -' (len h11)) + 2) -' 1;
0 + 1 <= ((((len h0) -' (len h11)) + 1) + 1) - 1 by XREAL_1:6;
then A861: (((len h0) -' (len h11)) + 2) -' 1 = (((len h0) -' (len h11)) + 2) - 1 by NAT_D:39;
A862: (((len h0) -' (len h11)) + 2) -' 1 <= len h21 by A36, A52, A55, A57, A252, NAT_D:44;
then A863: (((len h0) -' (len h11)) + 2) -' 1 in dom h21 by A43, Lm1, FINSEQ_3:25;
then h2 . ((((len h0) -' (len h11)) + 2) -' 1) in rng h2 by A46, FUNCT_1:def 3;
then A864: h2 . ((((len h0) -' (len h11)) + 2) -' 1) <= 1 by A29, BORSUK_1:40, XXREAL_1:1;
(((len h0) -' (len h11)) + 2) -' 1 in dom h21 by A43, A862, Lm1, FINSEQ_3:25;
then A865: h21 . ((((len h0) -' (len h11)) + 2) -' 1) = g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) by A46, FUNCT_1:13;
A866: (i + 1) - (len h11) = (i + 1) -' (len h11) by A39, A855, XREAL_1:233;
(i + 1) - (len h11) <= ((len h11) + ((len h2) - 2)) - (len h11) by A47, A36, A52, A55, A57, A813, XREAL_1:9;
then ((i + 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A866, XREAL_1:6;
then A867: (((i + 1) -' (len h11)) + 2) -' 1 <= len h21 by A47, NAT_D:44;
h0 . (len h0) in Lower_Arc P by A23, A131, A29, A848, A253, BORSUK_1:40, FUNCT_1:def 3;
then A868: h0 /. (len h0) in Lower_Arc P by A74, PARTFUN1:def 6;
A869: 0 + 2 <= ((i + 1) -' (len h11)) + 2 by XREAL_1:6;
then 2 -' 1 <= (((i + 1) -' (len h11)) + 2) -' 1 by NAT_D:42;
then A870: (((i + 1) -' (len h11)) + 2) -' 1 in dom h2 by A46, A867, Lm1, FINSEQ_3:25;
then A871: h2 . ((((i + 1) -' (len h11)) + 2) -' 1) in rng h2 by FUNCT_1:def 3;
then A872: ( 0 <= h2 . ((((i + 1) -' (len h11)) + 2) -' 1) & h2 . ((((i + 1) -' (len h11)) + 2) -' 1) <= 1 ) by A29, BORSUK_1:40, XXREAL_1:1;
(i + 1) - (len h11) < (len h0) - (len h11) by A813, XREAL_1:9;
then A873: ((i + 1) -' (len h11)) + 2 < ((len h0) -' (len h11)) + 2 by A252, A866, XREAL_1:6;
h0 . (len h0) = (mid (h21,2,((len h21) -' 1))) . ((len h0) - (len h11)) by A39, A36, A64, FINSEQ_1:23;
then A874: h0 . (len h0) = h21 . ((((len h0) -' (len h11)) + 2) -' 1) by A39, A36, A48, A56, A50, A54, A816, A252, FINSEQ_6:118;
A875: h0 /. (i + 1) = h0 . (i + 1) by A815, PARTFUN1:def 6;
g2 . (h2 . ((((i + 1) -' (len h11)) + 2) -' 1)) in rng g2 by A131, A29, A871, BORSUK_1:40, FUNCT_1:def 3;
then A876: h0 . (i + 1) in Lower_Arc P by A23, A860, A870, FUNCT_1:13;
(((i + 1) -' (len h11)) + 2) -' 1 = (((i + 1) -' (len h11)) + 2) - 1 by A869, Lm1, NAT_D:39, NAT_D:42;
then (((i + 1) -' (len h11)) + 2) -' 1 < (((len h0) -' (len h11)) + 2) -' 1 by A861, A873, XREAL_1:9;
then A877: h2 . ((((i + 1) -' (len h11)) + 2) -' 1) < h2 . ((((len h0) -' (len h11)) + 2) -' 1) by A30, A46, A863, A870, SEQM_3:def 1;
h0 . (i + 1) = g2 . (h2 . ((((i + 1) -' (len h11)) + 2) -' 1)) by A860, A870, FUNCT_1:13;
then LE h0 /. (i + 1),h0 /. (len h0), Lower_Arc P, E-max P, W-min P by A21, A22, A23, A24, A25, A75, A874, A865, A864, A872, A877, A875, Th18;
hence LE h0 /. (i + 1),h0 /. (len h0),P by A130, A875, A876, A868, JORDAN6:def 10; :: thesis:

end;

i < len h0 by A813, NAT_1:13;
then A878: i in dom h0 by A812, FINSEQ_3:25;
then h0 /. i = h0 . i by PARTFUN1:def 6;
then A879: h0 /. i <> W-min P by A72, A67, A78, A812, A878;
LE h0 /. i,h0 /. (i + 1),P by A256, A812, A813;
hence Segment ((h0 /. (len h0)),(h0 /. 1),P) misses Segment ((h0 /. i),(h0 /. (i + 1)),P) by A1, A72, A68, A879, A850, A817, Th14; :: thesis: