let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
let e be Real; :: thesis:
assume A1: ( P is being_simple_closed_curve & e > 0 ) ; :: thesis:
then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by JORDAN6:def 8;
then consider g1 being Function of I[01] ,(TOP-REAL 2) such that
A3: ( g1 is continuous & g1 is one-to-one ) and
A4: rng g1 = Upper_Arc P and
A5: ( g1 . 0 = W-min P & g1 . 1 = E-max P ) by Th18;
A6: dom g1 = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
A7: ( 0 in dom g1 & 1 in dom g1 ) by Lm5, BORSUK_1:83, FUNCT_2:def 1;
A8: ( E-max P in Upper_Arc P & W-min P in Upper_Arc P ) by A1, Th1;
consider h1 being FinSequence of REAL such that
A9: ( h1 . 1 = 0 & h1 . (len h1) = 1 & 5 <= len h1 & rng h1 c= the carrier of I[01] & h1 is increasing & ( for i being Element of 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 A1, A3, A5, UNIFORM1:15;
A10: h1 is one-to-one by A9;
A11: 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
A12: ( g2 is continuous & g2 is one-to-one ) and
A13: rng g2 = Lower_Arc P and
A14: ( g2 . 0 = E-max P & g2 . 1 = W-min P ) by Th18;
A15: dom g2 = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
consider h2 being FinSequence of REAL such that
A16: ( h2 . 1 = 0 & h2 . (len h2) = 1 & 5 <= len h2 & rng h2 c= the carrier of I[01] & h2 is increasing & ( for i being Element of 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 A1, A12, A14, UNIFORM1:15;
A17: ((len h2) - 1) - 1 < len h2 by Lm4;
A18: h2 is one-to-one by A16;
h1 is FinSequence of the carrier of I[01] by A9, FINSEQ_1:def 4;
then reconsider h11 = g1 * h1 as FinSequence of the carrier of (TOP-REAL 2) by FINSEQ_2:36;
A19: rng h1 c= dom g1 by A9, FUNCT_2:def 1;
then A20: dom h1 = dom h11 by RELAT_1:46;
then A21: len h1 = len h11 by FINSEQ_3:31;
h2 is FinSequence of the carrier of I[01] by A16, FINSEQ_1:def 4;
then reconsider h21 = g2 * h2 as FinSequence of the carrier of (TOP-REAL 2) by FINSEQ_2:36;
dom g2 = the carrier of I[01] by FUNCT_2:def 1;
then A22: dom h2 = dom h21 by A16, RELAT_1:46;
then A23: len h2 = len h21 by FINSEQ_3:31;
A24: 1 <= len h1 by A9, XXREAL_0:2;
then A25: 1 in dom h1 by FINSEQ_3:27;
A26: len h1 in dom h1 by A24, FINSEQ_3:27;
A27: 1 <= len h2 by A16, XXREAL_0:2;
then A28: 1 in dom h2 by FINSEQ_3:27;
A29: len h2 in dom h2 by A27, FINSEQ_3:27;
A30: h21 . 1 = E-max P by A14, A16, A28, FUNCT_1:23;
A31: h21 . (len h2) = W-min P by A14, A16, A29, FUNCT_1:23;
A32: 1 in dom g2 by Lm5, BORSUK_1:83, FUNCT_2:def 1;
A33: dom g1 = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then A34: 1 in dom (g1 * h1) by A9, A25, Lm5, FUNCT_1:21;
A35: len h1 in dom h1 by A24, FINSEQ_3:27;
h1 . (len h1) in dom g1 by A9, A33, XXREAL_1:1;
then A36: len h1 in dom (g1 * h1) by A26, FUNCT_1:21;
then A37: h11 . (len h1) = E-max P by A5, A9, FUNCT_1:22;
reconsider h0 = h11 ^ (mid h21,2,((len h21) -' 1)) as FinSequence of the carrier of (TOP-REAL 2) ;
A38: h11 . 1 = W-min P by A5, A9, A34, FUNCT_1:22;
take h0 ; :: thesis:
thus A39: h0 . 1 = W-min P by A34, A38, FINSEQ_1:def 7; :: thesis:
A40: len h0 = (len h11) + (len (mid h21,2,((len h21) -' 1))) by FINSEQ_1:35;
2 <= len h21 by A16, A23, XXREAL_0:2;
then A41: (1 + 1) - 1 <= (len h21) - 1 by XREAL_1:11;
then A42: (len h21) -' 1 = (len h21) - 1 by XREAL_0:def 2;
len h21 <= (len h21) + 1 by NAT_1:12;
then (len h21) - 1 <= ((len h21) + 1) - 1 by XREAL_1:11;
then A43: ( 2 <= len h21 & 1 <= (len h21) -' 1 & (len h21) -' 1 <= len h21 ) by A16, A23, A41, XREAL_0:def 2, XXREAL_0:2;
3 < len h21 by A16, A23, XXREAL_0:2;
then A44: (2 + 1) - 1 < (len h21) - 1 by XREAL_1:11;
then A45: 2 < (len h21) -' 1 by A41, NAT_D:39;
then A46: ((len h21) -' 1) -' 2 = ((len h21) -' 1) - 2 by XREAL_1:235;
A47: len (mid h21,2,((len h21) -' 1)) = (((len h21) -' 1) -' 2) + 1 by A43, A45, JORDAN3:27;
then A48: len h0 = (len h1) + ((len h2) - 2) by A20, A23, A40, A42, A46, FINSEQ_3:31;
A49: (3 + 2) - 2 <= (len h2) - 2 by A16, XREAL_1:11;
then A50: 1 <= (len h2) - 2 by XXREAL_0:2;
then A51: (len h1) + 1 <= len h0 by A21, A23, A40, A42, A46, A47, XREAL_1:9;
then A52: len h0 > len h1 by NAT_1:13;
then A53: 1 < len h0 by A24, XXREAL_0:2;
then A54: len h0 in dom h0 by FINSEQ_3:27;
then A55: h0 /. (len h0) = h0 . (len h0) by PARTFUN1:def 8;
A56: 1 <= (len h0) - (len h1) by A48, A49, XXREAL_0:2;
A57: (len h0) - (len h11) = (len h0) -' (len h11) by A21, A52, XREAL_1:235;
A58: 2 < len h1 by A9, XXREAL_0:2;
then A59: 2 in dom h1 by FINSEQ_3:27;
A60: 1 + 1 <= len h0 by A52, A58, XXREAL_0:2;
then A61: 2 in dom h0 by FINSEQ_3:27;
A62: h0 . 2 = h11 . 2 by A21, A58, FINSEQ_1:85;
A63: 1 in dom h0 by A53, FINSEQ_3:27;
then A64: h0 /. 1 = h0 . 1 by PARTFUN1:def 8;
A65: h0 /. 1 = W-min P by A39, A63, PARTFUN1:def 8;
A66: h11 is one-to-one by A3, A10, FUNCT_1:46;
A67: h21 is one-to-one by A12, A18, FUNCT_1:46;
thus A68: h0 is one-to-one :: thesis:

proof

let x, y be set ; :: according to FUNCT_1:def 8 :: thesis:
assume A69: ( x in dom h0 & y in dom h0 & h0 . x = h0 . y ) ; :: thesis:
then reconsider nx = x, ny = y as Element of NAT ;
A70: ( 1 <= nx & nx <= len h0 ) by A69, FINSEQ_3:27;
A71: ( 1 <= ny & ny <= len h0 ) by A69, FINSEQ_3:27;

per cases ;

suppose nx <= len h1 ; :: thesis:

then A72: nx in dom h1 by A70, FINSEQ_3:27;
then A73: h1 . nx in rng h1 by FUNCT_1:def 5;
A74: h0 . nx = h11 . nx by A20, A72, FINSEQ_1:def 7
.= g1 . (h1 . nx) by A20, A72, FUNCT_1:22 ;
then A75: h0 . nx in Upper_Arc P by A4, A19, A73, FUNCT_1:def 5;

per cases ;

suppose ny <= len h1 ; :: thesis:

then A76: ny in dom h1 by A71, FINSEQ_3:27;
then A77: h1 . ny in rng h1 by FUNCT_1:def 5;
h0 . ny = h11 . ny by A20, A76, FINSEQ_1:def 7
.= g1 . (h1 . ny) by A76, FUNCT_1:23 ;
then h1 . nx = h1 . ny by A3, A19, A69, A73, A74, A77, FUNCT_1:def 8;
hence x = y by A10, A72, A76, FUNCT_1:def 8; :: thesis:

end;

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

then A79: (len h1) + 1 <= ny by NAT_1:13;
A80: ( (len h11) + 1 <= ny & ny <= (len h11) + (len (mid h21,2,((len h21) -' 1))) ) by A21, A71, A78, FINSEQ_1:35, NAT_1:13;
then A81: h0 . ny = (mid h21,2,((len h21) -' 1)) . (ny - (len h11)) by FINSEQ_1:36;
A82: ny - (len h11) = ny -' (len h11) by A21, A78, XREAL_1:235;
A83: ny - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A80, XREAL_1:11;
A84: ((len h1) + 1) - (len h1) <= ny - (len h1) by A79, XREAL_1:11;
then A85: ( 1 <= ny -' (len h11) & ny -' (len h11) <= len (mid h21,2,((len h21) -' 1)) ) by A21, A78, A83, XREAL_1:235;
A86: h0 . ny = h21 . (((ny -' (len h11)) + 2) -' 1) by A21, A43, A45, A81, A82, A83, A84, JORDAN3:27;
A87: 1 + 1 <= (((ny -' (len h11)) + 1) + 1) - 1 by A85, XREAL_1:8;
A88: 0 + 2 <= (ny -' (len h11)) + 2 by XREAL_1:8;
ny - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A71, XREAL_1:11;
then A89: (ny -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A82, XREAL_1:8;
then A90: ((ny -' (len h11)) + 2) - 1 <= (len h2) - 1 by XREAL_1:11;
A91: ( 1 <= ((ny -' (len h11)) + 2) -' 1 & ((ny -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A88, A89, Lm1, NAT_D:42, NAT_D:44;
then A92: ((ny -' (len h11)) + 2) -' 1 in dom h21 by FINSEQ_3:27;
then h0 . ny in rng h21 by A86, FUNCT_1:def 5;
then h0 . ny in rng g2 by FUNCT_1:25;
then h0 . nx in (Upper_Arc P) /\ (Lower_Arc P) by A13, A69, A75, XBOOLE_0:def 4;
then A93: h0 . nx in {(W-min P),(E-max P)} by A1, JORDAN6:65;
A94: ((ny -' (len h11)) + 2) -' 1 <= (len h2) - 1 by A90, A91, NAT_D:39;
A95: 2 <= ((ny -' (len h11)) + 2) -' 1 by A87, A91, NAT_D:39;

per cases by A93, TARSKI:def 2;

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

then h21 . (((ny -' (len h11)) + 2) -' 1) = W-min P by A21, A43, A45, A69, A81, A82, A83, A84, JORDAN3:27;
then len h21 = ((ny -' (len h11)) + 2) -' 1 by A22, A23, A29, A31, A67, A92, FUNCT_1:def 8;
then (len h21) + 1 <= ((len h21) - 1) + 1 by A23, A94, XREAL_1:8;
then ((len h21) + 1) - (len h21) <= (len h21) - (len h21) by XREAL_1:11;
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 A22, A28, A30, A67, A69, A86, A92, FUNCT_1:def 8;
hence x = y by A95; :: thesis:

end;

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

then A97: (len h1) + 1 <= nx by NAT_1:13;
A98: ( (len h11) + 1 <= nx & nx <= (len h11) + (len (mid h21,2,((len h21) -' 1))) ) by A21, A70, A96, FINSEQ_1:35, NAT_1:13;
then A99: h0 . nx = (mid h21,2,((len h21) -' 1)) . (nx - (len h11)) by FINSEQ_1:36;
A100: nx - (len h11) = nx -' (len h11) by A21, A96, XREAL_1:235;
A101: nx - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A98, XREAL_1:11;
A102: ((len h1) + 1) - (len h1) <= nx - (len h1) by A97, XREAL_1:11;
then A103: ( 1 <= nx -' (len h11) & nx -' (len h11) <= len (mid h21,2,((len h21) -' 1)) ) by A21, A96, A101, XREAL_1:235;
A104: h0 . nx = h21 . (((nx -' (len h11)) + 2) -' 1) by A21, A43, A45, A99, A100, A101, A102, JORDAN3:27;
A105: 1 + 1 <= (((nx -' (len h11)) + 1) + 1) - 1 by A103, XREAL_1:8;
A106: 0 + 2 <= (nx -' (len h11)) + 2 by XREAL_1:8;
nx - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A70, XREAL_1:11;
then A107: (nx -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A100, XREAL_1:8;
then A108: ((nx -' (len h11)) + 2) - 1 <= (len h2) - 1 by XREAL_1:11;
A109: ( 1 <= ((nx -' (len h11)) + 2) -' 1 & ((nx -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A106, A107, Lm1, NAT_D:42, NAT_D:44;
then A110: ((nx -' (len h11)) + 2) -' 1 in dom h21 by FINSEQ_3:27;
then h0 . nx in rng h21 by A104, FUNCT_1:def 5;
then A111: h0 . nx in Lower_Arc P by A13, FUNCT_1:25;

per cases ;

suppose ny <= len h1 ; :: thesis:

then A112: ny in dom h1 by A71, FINSEQ_3:27;
then A113: h1 . ny in rng h1 by FUNCT_1:def 5;
h0 . ny = h11 . ny by A20, A112, FINSEQ_1:def 7
.= g1 . (h1 . ny) by A20, A112, FUNCT_1:22 ;
then h0 . ny in rng g1 by A19, A113, FUNCT_1:def 5;
then h0 . ny in (Upper_Arc P) /\ (Lower_Arc P) by A4, A69, A111, XBOOLE_0:def 4;
then A114: h0 . ny in {(W-min P),(E-max P)} by A1, JORDAN6:65;
A115: ((nx -' (len h11)) + 2) -' 1 <= (len h2) - 1 by A108, A109, NAT_D:39;
A116: 2 <= ((nx -' (len h11)) + 2) -' 1 by A105, A109, NAT_D:39;

per cases by A114, TARSKI:def 2;

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

then len h21 = ((nx -' (len h11)) + 2) -' 1 by A22, A23, A29, A31, A67, A69, A104, A110, FUNCT_1:def 8;
then (len h21) + 1 <= ((len h21) - 1) + 1 by A23, A115, XREAL_1:8;
then ((len h21) + 1) - (len h21) <= (len h21) - (len h21) by XREAL_1:11;
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 A21, A43, A45, A69, A99, A100, A101, A102, JORDAN3:27;
then 1 = ((nx -' (len h11)) + 2) -' 1 by A22, A28, A30, A67, A110, FUNCT_1:def 8;
hence x = y by A116; :: thesis:

end;

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

then A118: (len h1) + 1 <= ny by NAT_1:13;
then A119: h0 . ny = (mid h21,2,((len h21) -' 1)) . (ny - (len h11)) by A21, A40, A71, FINSEQ_1:36;
A120: ny - (len h11) = ny -' (len h11) by A21, A117, XREAL_1:235;
A121: ny - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A71, XREAL_1:11;
((len h1) + 1) - (len h1) <= ny - (len h1) by A118, XREAL_1:11;
then A122: h0 . ny = h21 . (((ny -' (len h11)) + 2) -' 1) by A21, A43, A45, A119, A120, A121, JORDAN3:27;
A123: 0 + 2 <= (ny -' (len h11)) + 2 by XREAL_1:8;
ny - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A71, XREAL_1:11;
then (ny -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A120, XREAL_1:8;
then A124: ( 1 <= ((ny -' (len h11)) + 2) -' 1 & ((ny -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A123, Lm1, NAT_D:42, NAT_D:44;
then ((ny -' (len h11)) + 2) -' 1 in dom h21 by FINSEQ_3:27;
then ((nx -' (len h1)) + 2) -' 1 = ((ny -' (len h1)) + 2) -' 1 by A21, A67, A69, A104, A110, A122, FUNCT_1:def 8;
then ((nx -' (len h1)) + 2) - 1 = ((ny -' (len h1)) + 2) -' 1 by A21, A109, NAT_D:39;
then (nx -' (len h1)) + (2 - 1) = ((ny -' (len h1)) + 2) - 1 by A21, A124, NAT_D:39;
then ((len h1) + nx) - (len h1) = (len h1) + (ny - (len h1)) by A21, A100, A120, XCMPLX_1:29;
hence x = y ; :: thesis:

end;

then A125: h0 /. (len h0) <> W-min P by A24, A39, A52, A54, A55, A63, FUNCT_1:def 8;
(3 + 2) - 2 <= (len h2) - 2 by A16, XREAL_1:11;
then A126: 5 + 3 <= (len h1) + ((len h2) - 2) by A9, XREAL_1:9;
hence 8 <= len h0 by A20, A23, A40, A42, A46, A47, FINSEQ_3:31; :: thesis:
A127: rng (g1 * h1) c= rng g1 by RELAT_1:45;
A128: rng (mid h21,2,((len h21) -' 1)) c= rng h21 by JORDAN3:28;
rng (g2 * h2) c= rng g2 by RELAT_1:45;
then rng (mid h21,2,((len h21) -' 1)) c= rng g2 by A128, XBOOLE_1:1;
then (rng h11) \/ (rng (mid h21,2,((len h21) -' 1))) c= (Upper_Arc P) \/ (Lower_Arc P) by A4, A13, A127, XBOOLE_1:13;
then rng h0 c= (Upper_Arc P) \/ (Lower_Arc P) by FINSEQ_1:44;
hence rng h0 c= P by A1, JORDAN6:def 9; :: thesis:
thus for i being Element of NAT st 1 <= i & i < len h0 holds
LE h0 /. i,h0 /. (i + 1),P :: thesis:

proof

let i be Element of NAT ; :: thesis:
assume A129: ( 1 <= i & i < len h0 ) ; :: thesis:
then A130: i + 1 <= len h0 by NAT_1:13;
A131: 1 < i + 1 by A129, NAT_1:13;
A132: i < i + 1 by NAT_1:13;

per cases ;

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

then A134: i + 1 <= len h1 by NAT_1:13;
A135: h0 . i = h11 . i by A21, A129, A133, FINSEQ_1:85;
A136: i in dom h1 by A129, A133, FINSEQ_3:27;
then A137: h0 . i = g1 . (h1 . i) by A135, FUNCT_1:23;
A138: h1 . i in rng h1 by A136, FUNCT_1:def 5;
then A139: ( 0 <= h1 . i & h1 . i <= 1 ) by A9, BORSUK_1:83, XXREAL_1:1;
A140: h0 . (i + 1) = h11 . (i + 1) by A21, A131, A134, FINSEQ_1:85;
A141: i + 1 in dom h1 by A131, A134, FINSEQ_3:27;
then A142: h0 . (i + 1) = g1 . (h1 . (i + 1)) by A140, FUNCT_1:23;
A143: h1 . (i + 1) in rng h1 by A141, FUNCT_1:def 5;
then A144: ( 0 <= h1 . (i + 1) & h1 . (i + 1) <= 1 ) by A9, BORSUK_1:83, XXREAL_1:1;
A145: h1 . i < h1 . (i + 1) by A9, A132, A136, A141, SEQM_3:def 1;
i in dom h0 by A129, FINSEQ_3:27;
then A146: h0 /. i = h0 . i by PARTFUN1:def 8;
i + 1 in dom h0 by A130, A131, FINSEQ_3:27;
then A147: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
A148: g1 . (h1 . i) in rng g1 by A6, A9, A138, BORSUK_1:83, FUNCT_1:def 5;
A149: h0 . (i + 1) in Upper_Arc P by A4, A6, A9, A142, A143, BORSUK_1:83, FUNCT_1:def 5;
LE h0 /. i,h0 /. (i + 1), Upper_Arc P, W-min P, E-max P by A2, A3, A4, A5, A137, A139, A142, A144, A145, A146, A147, Th19;
hence LE h0 /. i,h0 /. (i + 1),P by A4, A137, A146, A147, A148, A149, JORDAN6:def 10; :: thesis:

end;

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

per cases by A150, XXREAL_0:1;

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

then A152: (len h1) + 1 <= i by NAT_1:13;
(len h11) + 1 <= i by A21, A151, NAT_1:13;
then A153: h0 . i = (mid h21,2,((len h21) -' 1)) . (i - (len h11)) by A40, A129, FINSEQ_1:36;
A154: i - (len h11) = i -' (len h11) by A21, A151, XREAL_1:235;
A155: i - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A129, XREAL_1:11;
((len h1) + 1) - (len h1) <= i - (len h1) by A152, XREAL_1:11;
then A156: h0 . i = h21 . (((i -' (len h11)) + 2) -' 1) by A21, A43, A45, A153, A154, A155, JORDAN3:27;
A157: (len h1) + 1 <= i + 1 by A152, NAT_1:13;
then A158: h0 . (i + 1) = (mid h21,2,((len h21) -' 1)) . ((i + 1) - (len h11)) by A21, A40, A130, FINSEQ_1:36;
i + 1 > len h11 by A21, A151, NAT_1:13;
then A159: (i + 1) - (len h11) = (i + 1) -' (len h11) by XREAL_1:235;
A160: (i + 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A130, XREAL_1:11;
A161: ((len h1) + 1) - (len h1) <= (i + 1) - (len h1) by A157, XREAL_1:11;
then A162: h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A158, A159, A160, JORDAN3:27;
A163: 1 < ((i + 1) -' (len h11)) + (2 - 1) by A21, A159, A161, NAT_1:13;
then A164: 0 < (((i + 1) -' (len h11)) + 2) - 1 ;
A165: (((i + 1) -' (len h11)) + 2) - 1 = (((i + 1) -' (len h11)) + 2) -' 1 by A163, XREAL_0:def 2;
A166: 0 + 2 <= (i -' (len h11)) + 2 by XREAL_1:8;
i - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A129, XREAL_1:11;
then A167: (i -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A154, XREAL_1:8;
then A168: ( 1 <= ((i -' (len h11)) + 2) -' 1 & ((i -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A166, Lm1, NAT_D:42, NAT_D:44;
set j = ((i -' (len h11)) + 2) -' 1;
A169: (((i -' (len h11)) + 2) -' 1) + 1 = ((((i -' (len h11)) + 1) + 1) - 1) + 1 by A168, NAT_D:39
.= (i -' (len h11)) + 2 ;
A170: (((i -' (len h11)) + 2) -' 1) + 1 = (((i - (len h11)) + 2) - 1) + 1 by A154, A168, NAT_D:39
.= (((i + 1) -' (len h11)) + 2) -' 1 by A159, A164, XREAL_0:def 2 ;
A171: ((i -' (len h11)) + 2) -' 1 in dom h2 by A22, A168, FINSEQ_3:27;
then A172: h0 . i = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by A156, FUNCT_1:23;
A173: h2 . (((i -' (len h11)) + 2) -' 1) in rng h2 by A171, FUNCT_1:def 5;
then A174: ( 0 <= h2 . (((i -' (len h11)) + 2) -' 1) & h2 . (((i -' (len h11)) + 2) -' 1) <= 1 ) by A16, BORSUK_1:83, XXREAL_1:1;
A175: ((i -' (len h11)) + 2) -' 1 < (((i -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
A176: 1 < (((i -' (len h11)) + 2) -' 1) + 1 by A168, NAT_1:13;
then A177: (((i -' (len h11)) + 2) -' 1) + 1 in dom h2 by A167, A169, FINSEQ_3:27;
then A178: h0 . (i + 1) = g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) by A162, A170, FUNCT_1:23;
A179: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by A177, FUNCT_1:def 5;
then A180: ( 0 <= h2 . ((((i -' (len h11)) + 2) -' 1) + 1) & h2 . ((((i -' (len h11)) + 2) -' 1) + 1) <= 1 ) by A16, BORSUK_1:83, XXREAL_1:1;
A181: h2 . (((i -' (len h11)) + 2) -' 1) < h2 . ((((i -' (len h11)) + 2) -' 1) + 1) by A16, A171, A175, A177, SEQM_3:def 1;
i in dom h0 by A129, FINSEQ_3:27;
then A182: h0 /. i = h0 . i by PARTFUN1:def 8;
i + 1 in dom h0 by A130, A131, FINSEQ_3:27;
then A183: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
A184: h0 . i in Lower_Arc P by A13, A15, A16, A172, A173, BORSUK_1:83, FUNCT_1:def 5;
A185: h0 . (i + 1) in Lower_Arc P by A13, A15, A16, A178, A179, BORSUK_1:83, FUNCT_1:def 5;
(i + 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A130, XREAL_1:11;
then A186: ((i + 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A159, XREAL_1:8;
then A187: (((i + 1) -' (len h11)) + 2) - 1 <= (len h2) - 1 by XREAL_1:11;
len h2 < (len h2) + 1 by NAT_1:13;
then (len h2) - 1 < ((len h2) + 1) - 1 by XREAL_1:11;
then (((i + 1) -' (len h11)) + 2) -' 1 < len h2 by A165, A187, XXREAL_0:2;
then A188: (((i + 1) -' (len h11)) + 2) -' 1 in dom h2 by A170, A176, FINSEQ_3:27;

A189: now

assume h0 /. (i + 1) = W-min P ; :: thesis:
then len h21 = (((i + 1) -' (len h11)) + 2) -' 1 by A22, A23, A29, A31, A67, A162, A183, A188, FUNCT_1:def 8;
then ((len h21) + 1) - (len h21) <= (len h21) - (len h21) by A23, A165, A186, XREAL_1:11;
then ((len h21) + 1) - (len h21) <= 0 ;
hence contradiction ; :: thesis:

end;

LE h0 /. i,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P by A11, A12, A13, A14, A172, A174, A178, A180, A181, A182, A183, Th19;
hence LE h0 /. i,h0 /. (i + 1),P by A182, A183, A184, A185, A189, JORDAN6:def 10; :: thesis:

end;

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

then A191: h0 . (i + 1) = (mid h21,2,((len h21) -' 1)) . ((i + 1) - (len h11)) by A21, A40, A130, FINSEQ_1:36;
A192: (i + 1) - (len h11) = (i + 1) -' (len h11) by A21, A132, A190, XREAL_1:235;
(i + 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A130, XREAL_1:11;
then A193: h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A190, A191, A192, JORDAN3:27;
A194: h0 . i = h11 . i by A21, A129, A190, FINSEQ_1:85;
i in dom h1 by A129, A190, FINSEQ_3:27;
then A195: h0 . i = E-max P by A5, A9, A190, A194, FUNCT_1:23;
i in dom h0 by A129, FINSEQ_3:27;
then h0 /. i = E-max P by A195, PARTFUN1:def 8;
then A196: h0 /. i in Upper_Arc P by A1, Th1;
set j = ((i -' (len h11)) + 2) -' 1;
(len h11) -' (len h11) = (len h11) - (len h11) by XREAL_1:235
.= 0 ;
then A197: ((i -' (len h11)) + 2) -' 1 = 2 - 1 by A21, A190, XREAL_1:235;
then A198: (((i -' (len h11)) + 2) -' 1) + 1 <= len h2 by A16, XXREAL_0:2;
A199: (((i + 1) -' (len h11)) + 2) -' 1 = (1 + 2) -' 1 by A21, A190, NAT_D:34
.= 2 by NAT_D:34 ;
A200: (((i -' (len h11)) + 2) -' 1) + 1 in dom h2 by A197, A198, FINSEQ_3:27;
then A201: h0 . (i + 1) = g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) by A193, A197, A199, FUNCT_1:23;
A202: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by A200, FUNCT_1:def 5;
i + 1 in dom h0 by A130, A131, FINSEQ_3:27;
then A203: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
A204: h0 . (i + 1) in Lower_Arc P by A13, A15, A16, A201, A202, BORSUK_1:83, FUNCT_1:def 5;
2 <= len h21 by A16, A23, XXREAL_0:2;
then A205: 2 in dom h21 by FINSEQ_3:27;
len h21 <> (((i + 1) -' (len h11)) + 2) -' 1 by A16, A23, A199;
then h0 /. (i + 1) <> W-min P by A22, A23, A29, A31, A67, A193, A199, A203, A205, FUNCT_1:def 8;
hence LE h0 /. i,h0 /. (i + 1),P by A196, A203, A204, JORDAN6:def 10; :: thesis:

end;

thus for i being Element of 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 Element of NAT ; :: thesis:
let W be Subset of (Euclid 2); :: thesis:
assume A206: ( 1 <= i & i < len h0 & W = Segment (h0 /. i),(h0 /. (i + 1)),P ) ; :: thesis:
then A207: i + 1 <= len h0 by NAT_1:13;
A208: 1 < i + 1 by A206, NAT_1:13;
A209: i < i + 1 by NAT_1:13;

per cases by XXREAL_0:1;

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

then A211: i + 1 <= len h1 by NAT_1:13;
A212: h0 . i = h11 . i by A21, A206, A210, FINSEQ_1:85;
A213: i in dom h1 by A206, A210, FINSEQ_3:27;
then A214: h11 . i = g1 . (h1 . i) by FUNCT_1:23;
then A215: h0 . i = g1 . (h1 . i) by A21, A206, A210, FINSEQ_1:85;
A216: h1 . i in rng h1 by A213, FUNCT_1:def 5;
then A217: ( 0 <= h1 . i & h1 . i <= 1 ) by A9, BORSUK_1:83, XXREAL_1:1;
A218: h0 . (i + 1) = h11 . (i + 1) by A21, A208, A211, FINSEQ_1:85;
A219: i + 1 in dom h1 by A208, A211, FINSEQ_3:27;
then A220: h0 . (i + 1) = g1 . (h1 . (i + 1)) by A218, FUNCT_1:23;
A221: h1 . (i + 1) in rng h1 by A219, FUNCT_1:def 5;
then A222: ( 0 <= h1 . (i + 1) & h1 . (i + 1) <= 1 ) by A9, BORSUK_1:83, XXREAL_1:1;
A223: h1 . i < h1 . (i + 1) by A9, A209, A213, A219, SEQM_3:def 1;
i in dom h0 by A206, FINSEQ_3:27;
then A224: h0 /. i = h0 . i by PARTFUN1:def 8;
i + 1 in dom h0 by A207, A208, FINSEQ_3:27;
then A225: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
A226: h0 . i in Upper_Arc P by A4, A6, A9, A215, A216, BORSUK_1:83, FUNCT_1:def 5;
A227: h0 . (i + 1) in Upper_Arc P by A4, A6, A9, A220, A221, BORSUK_1:83, FUNCT_1:def 5;
A228: h1 /. i = h1 . i by A206, A210, FINSEQ_4:24;
A229: h1 /. (i + 1) = h1 . (i + 1) by A208, A211, FINSEQ_4:24;
then reconsider Q1 = [.(h1 /. i),(h1 /. (i + 1)).] as Subset of I[01] by A9, A216, A221, A228, BORSUK_1:83, XXREAL_2:def 12;
A230: Segment (h0 /. i),(h0 /. (i + 1)),P c= g1 .: [.(h1 /. i),(h1 /. (i + 1)).]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A231: x in Segment (h0 /. i),(h0 /. (i + 1)),P ; :: thesis:
A232: h0 /. (i + 1) <> W-min P by A20, A25, A38, A66, A208, A218, A219, A225, FUNCT_1:def 8;
then x in { p where p is Point of (TOP-REAL 2) : ( LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) } by A231, Def1;
then consider p being Point of (TOP-REAL 2) such that
A233: ( p = x & LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) ;
A234: ( ( 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 A233, JORDAN6:def 10;
A235: ( ( 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 A233, JORDAN6:def 10;

now

per cases by A211, XXREAL_0:1;

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

then A236: h0 /. (i + 1) <> E-max P by A20, A26, A37, A66, A218, A219, A225, FUNCT_1:def 8;

A237: now

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

end;

then A238: ( p in Upper_Arc P & h0 /. (i + 1) in Upper_Arc P ) by A233, JORDAN6:def 10;
A239: LE p,h0 /. (i + 1), Upper_Arc P, W-min P, E-max P by A233, A237, JORDAN6:def 10;
then A240: p <> E-max P by A2, A236, JORDAN6:70;

per cases by A206, XXREAL_0:1;

suppose i > 1 ; :: thesis:

then A241: h0 /. i <> W-min P by A20, A25, A38, A66, A213, A214, A215, A224, FUNCT_1:def 8;
A242: h11 . i <> E-max P by A20, A26, A37, A66, A210, A213, FUNCT_1:def 8;

now

assume h0 /. i in Lower_Arc P ; :: thesis:
then h0 /. i in (Upper_Arc P) /\ (Lower_Arc P) by A224, A226, XBOOLE_0:def 4;
then h0 /. i in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
hence contradiction by A212, A224, A241, A242, TARSKI:def 2; :: thesis:

end;

then A243: ( ( 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 A233, JORDAN6:def 10;
then A244: p <> W-min P by A2, A241, JORDAN6:69;

A245: now

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

end;

then consider z being set such that
A246: ( z in dom g1 & p = g1 . z ) by A4, A243, FUNCT_1:def 5;
reconsider rz = z as Real by A6, A246;
A247: g1 . (h1 /. i) = h0 /. i by A206, A210, A212, A214, A224, FINSEQ_4:24;
A248: ( 0 <= h1 /. i & h1 /. i <= 1 & g1 . (h1 /. (i + 1)) = h0 /. (i + 1) ) by A206, A208, A210, A211, A217, A220, A225, FINSEQ_4:24;
h1 . (i + 1) in rng h1 by A219, FUNCT_1:def 5;
then A249: ( 0 <= h1 /. (i + 1) & h1 /. (i + 1) <= 1 ) by A9, A229, BORSUK_1:83, XXREAL_1:1;
take z = z; :: thesis:
thus z in dom g1 by A246; :: thesis:
A250: ( 0 <= rz & rz <= 1 ) by A246, BORSUK_1:83, XXREAL_1:1;
then A251: h1 /. i <= rz by A3, A4, A5, A243, A245, A246, A247, A248, Th20;
rz <= h1 /. (i + 1) by A3, A4, A5, A239, A246, A248, A249, A250, Th20;
hence z in [.(h1 /. i),(h1 /. (i + 1)).] by A251, XXREAL_1:1; :: thesis:
thus x = g1 . z by A233, A246; :: thesis:

end;

suppose A252: i = 1 ; :: thesis:

now

per cases ;

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

now

end;

then consider z being set such that
A254: ( z in dom g1 & p = g1 . z ) by A4, A234, FUNCT_1:def 5;
reconsider rz = z as Real by A6, A254;
take rz = rz; :: thesis:
A255: g1 . (h1 /. (1 + 1)) = h0 /. (1 + 1) by A211, A220, A225, A252, FINSEQ_4:24;
h1 . (1 + 1) in rng h1 by A219, A252, FUNCT_1:def 5;
then A256: ( 0 <= h1 /. (1 + 1) & h1 /. (1 + 1) <= 1 ) by A9, A229, A252, BORSUK_1:83, XXREAL_1:1;
A257: ( 0 <= rz & rz <= 1 ) by A254, BORSUK_1:83, XXREAL_1:1;
A258: h1 /. 1 <= rz by A9, A228, A252, A254, BORSUK_1:83, XXREAL_1:1;
rz <= h1 /. (1 + 1) by A3, A4, A5, A239, A252, A254, A255, A256, A257, Th20;
hence ( rz in dom g1 & rz in [.(h1 /. 1),(h1 /. (1 + 1)).] & x = g1 . rz ) by A233, A254, A258, XXREAL_1:1; :: thesis:

end;

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

thus 0 in [.(h1 /. 1),(h1 /. (1 + 1)).] by A9, A223, A228, A229, A252, XXREAL_1:1; :: thesis:
thus x = g1 . 0 by A5, A233, A259; :: thesis:

end;

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

end;

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

then A261: h0 /. (i + 1) = E-max P by A5, A9, A26, A218, A225, FUNCT_1:23;
A262: ( p in Upper_Arc P or p in Lower_Arc P ) by A233, JORDAN6:def 10;

A263: now

assume A264: ( p in Lower_Arc P & not p in Upper_Arc P ) ; :: thesis:
then LE h0 /. (i + 1),p, Lower_Arc P, E-max P, W-min P by A11, A261, JORDAN5C:10;
hence contradiction by A8, A11, A235, A261, A264, JORDAN5C:12; :: thesis:

end;

then A265: LE p,h0 /. (i + 1), Upper_Arc P, W-min P, E-max P by A2, A261, A262, JORDAN5C:10;

per cases ;

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

now

per cases ;

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

A268: now

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

end;

then consider z being set such that
A269: ( z in dom g1 & p = g1 . z ) by A4, A234, FUNCT_1:def 5;
reconsider rz = z as Real by A6, A269;
take rz = rz; :: thesis:
A270: g1 . (h1 /. (i + 1)) = h0 /. (i + 1) by A208, A211, A220, A225, FINSEQ_4:24;
h1 . (i + 1) in rng h1 by A219, FUNCT_1:def 5;
then A271: ( 0 <= h1 /. (i + 1) & h1 /. (i + 1) <= 1 ) by A9, A229, BORSUK_1:83, XXREAL_1:1;
A272: ( 0 <= rz & rz <= 1 ) by A269, BORSUK_1:83, XXREAL_1:1;
then A273: h1 /. i <= rz by A3, A4, A5, A212, A214, A217, A224, A228, A234, A268, A269, Th20;
rz <= h1 /. (i + 1) by A3, A4, A5, A265, A269, A270, A271, A272, Th20;
hence ( rz in dom g1 & rz in [.(h1 /. i),(h1 /. (i + 1)).] & x = g1 . rz ) by A233, A269, A273, XXREAL_1:1; :: thesis:

end;

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

then h11 . i = W-min P by A2, A212, A224, A234, JORDAN6:69;
then i = 1 by A20, A25, A38, A66, A213, FUNCT_1:def 8;
then 0 in [.(h1 /. i),(h1 /. (i + 1)).] by A9, A223, A228, A229, XXREAL_1:1;
hence ex y being set st
( y in dom g1 & y in [.(h1 /. i),(h1 /. (i + 1)).] & x = g1 . y ) by A5, A7, A233, A274; :: 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 A275: p = E-max P ; :: thesis:

1 in [.(h1 /. i),(h1 /. (i + 1)).] by A9, A223, A228, A229, A260, XXREAL_1:1;
hence ex y being set st
( y in dom g1 & y in [.(h1 /. i),(h1 /. (i + 1)).] & x = g1 . y ) by A5, A33, A233, A275, Lm5; :: thesis:

end;

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

end;

g1 .: [.(h1 /. i),(h1 /. (i + 1)).] c= Segment (h0 /. i),(h0 /. (i + 1)),P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in g1 .: [.(h1 /. i),(h1 /. (i + 1)).] ; :: thesis:
then consider y being set such that
A276: ( y in dom g1 & y in [.(h1 /. i),(h1 /. (i + 1)).] & x = g1 . y ) by FUNCT_1:def 12;
A277: x in Upper_Arc P by A4, A276, FUNCT_1:def 5;
then reconsider p1 = x as Point of (TOP-REAL 2) ;
reconsider sy = y as Real by A276;
A278: g1 . (h1 /. i) = h0 /. i by A206, A210, A215, A224, FINSEQ_4:24;
A279: ( h1 /. i <= sy & sy <= h1 /. (i + 1) ) by A276, XXREAL_1:1;
A280: ( 0 <= h1 /. i & h1 /. i <= 1 ) by A206, A210, A217, FINSEQ_4:24;
A281: ( 0 <= sy & sy <= 1 ) by A276, BORSUK_1:83, XXREAL_1:1;
then A282: LE h0 /. i,p1, Upper_Arc P, W-min P, E-max P by A2, A3, A4, A5, A276, A278, A279, A280, Th19;
LE p1,h0 /. (i + 1), Upper_Arc P, W-min P, E-max P by A2, A3, A4, A5, A220, A222, A225, A229, A276, A279, A281, Th19;
then A283: ( LE h0 /. i,p1,P & LE p1,h0 /. (i + 1),P ) by A224, A225, A226, A227, A277, A282, JORDAN6:def 10;
A284: not h0 /. (i + 1) = W-min P by A20, A25, A38, A66, A208, A218, A219, A225, FUNCT_1:def 8;
x in { p where p is Point of (TOP-REAL 2) : ( LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) } by A283;
hence x in Segment (h0 /. i),(h0 /. (i + 1)),P by A284, Def1; :: thesis:

end;

then W = g1 .: Q1 by A206, A230, XBOOLE_0:def 10;
hence diameter W < e by A9, A206, A210; :: thesis:

end;

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

then A286: (len h1) + 1 <= i by NAT_1:13;
( (len h11) + 1 <= i & i <= (len h11) + (len (mid h21,2,((len h21) -' 1))) ) by A21, A206, A285, FINSEQ_1:35, NAT_1:13;
then A287: h0 . i = (mid h21,2,((len h21) -' 1)) . (i - (len h11)) by FINSEQ_1:36;
A288: i - (len h11) = i -' (len h11) by A21, A285, XREAL_1:235;
A289: i - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A206, XREAL_1:11;
((len h1) + 1) - (len h1) <= i - (len h1) by A286, XREAL_1:11;
then A290: h0 . i = h21 . (((i -' (len h11)) + 2) -' 1) by A21, A43, A45, A287, A288, A289, JORDAN3:27;
A291: (len h1) + 1 <= i + 1 by A286, NAT_1:13;
then A292: h0 . (i + 1) = (mid h21,2,((len h21) -' 1)) . ((i + 1) - (len h11)) by A21, A40, A207, FINSEQ_1:36;
i + 1 > len h11 by A21, A285, NAT_1:13;
then A293: (i + 1) - (len h11) = (i + 1) -' (len h11) by XREAL_1:235;
A294: (i + 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A207, XREAL_1:11;
A295: ((len h1) + 1) - (len h1) <= (i + 1) - (len h1) by A291, XREAL_1:11;
then A296: h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A292, A293, A294, JORDAN3:27;
1 < ((i + 1) -' (len h11)) + (2 - 1) by A21, A293, A295, NAT_1:13;
then A297: 0 < (((i + 1) -' (len h11)) + 2) - 1 ;
A298: 0 + 2 <= (i -' (len h11)) + 2 by XREAL_1:8;
i - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A206, XREAL_1:11;
then A299: (i -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A288, XREAL_1:8;
then A300: ((i -' (len h11)) + 2) - 1 <= (len h2) - 1 by XREAL_1:11;
A301: ( 1 <= ((i -' (len h11)) + 2) -' 1 & ((i -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A298, A299, Lm1, NAT_D:42, NAT_D:44;
len h2 < (len h2) + 1 by NAT_1:13;
then (len h2) - 1 < ((len h2) + 1) - 1 by XREAL_1:11;
then A302: ((i -' (len h11)) + 2) - 1 < len h2 by A300, XXREAL_0:2;
A303: ((i -' (len h11)) + 2) -' 1 = ((i -' (len h11)) + 2) - 1 by A301, NAT_D:39;
set j = ((i -' (len h11)) + 2) -' 1;
(len h1) + 1 <= i by A285, NAT_1:13;
then ((len h11) + 1) - (len h11) <= i - (len h11) by A21, XREAL_1:11;
then 1 <= i -' (len h11) by NAT_D:39;
then 1 + 2 <= (i -' (len h11)) + 2 by XREAL_1:8;
then (1 + 2) - 1 <= ((i -' (len h11)) + 2) - 1 by XREAL_1:11;
then A304: 1 < ((i -' (len h11)) + 2) -' 1 by A303, XXREAL_0:2;
i - (len h11) < ((len h11) + ((len h2) - 2)) - (len h11) by A23, A40, A42, A46, A47, A206, XREAL_1:11;
then A305: (i - (len h11)) + 2 < ((len h2) - 2) + 2 by XREAL_1:8;
A306: ((i -' (len h11)) + 2) -' 1 < len h2 by A301, A302, NAT_D:39;
A307: (((i -' (len h11)) + 2) -' 1) + 1 = ((((i -' (len h11)) + 1) + 1) - 1) + 1 by A301, NAT_D:39
.= (i -' (len h11)) + (1 + 1) ;
A308: (((i -' (len h11)) + 2) -' 1) + 1 = (((i + 1) -' (len h11)) + 2) -' 1 by A288, A293, A297, A303, XREAL_0:def 2;
A309: ((i -' (len h11)) + 2) -' 1 in dom h2 by A22, A301, FINSEQ_3:27;
then A310: h0 . i = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by A290, FUNCT_1:23;
A311: h2 . (((i -' (len h11)) + 2) -' 1) in rng h2 by A309, FUNCT_1:def 5;
A312: 1 < (((i -' (len h11)) + 2) -' 1) + 1 by A301, NAT_1:13;
then A313: (((i -' (len h11)) + 2) -' 1) + 1 in dom h2 by A299, A307, FINSEQ_3:27;
then A314: h0 . (i + 1) = g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) by A296, A308, FUNCT_1:23;
A315: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by A313, FUNCT_1:def 5;
i in dom h0 by A206, FINSEQ_3:27;
then A316: h0 /. i = h0 . i by PARTFUN1:def 8;
i + 1 in dom h0 by A207, A208, FINSEQ_3:27;
then A317: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) in rng g2 by A15, A16, A311, BORSUK_1:83, FUNCT_1:def 5;
then A318: h0 . i in Lower_Arc P by A13, A290, A309, FUNCT_1:23;
A319: h0 . (i + 1) in Lower_Arc P by A13, A15, A16, A314, A315, BORSUK_1:83, FUNCT_1:def 5;
A320: 0 <= h2 . (((i -' (len h11)) + 2) -' 1) by A16, A311, BORSUK_1:83, XXREAL_1:1;
A321: h2 . (((i -' (len h11)) + 2) -' 1) <= 1 by A16, A311, BORSUK_1:83, XXREAL_1:1;
A322: g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) = h0 /. (i + 1) by A296, A308, A313, A317, FUNCT_1:23;
A323: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) <= 1 by A16, A315, BORSUK_1:83, XXREAL_1:1;
A324: h2 /. (((i -' (len h11)) + 2) -' 1) = h2 . (((i -' (len h11)) + 2) -' 1) by A301, A306, FINSEQ_4:24;
A325: h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) = h2 . ((((i -' (len h11)) + 2) -' 1) + 1) by A299, A307, A312, FINSEQ_4:24;
then reconsider Q1 = [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] as Subset of I[01] by A16, A311, A315, A324, BORSUK_1:83, XXREAL_2:def 12;
A326: Segment (h0 /. i),(h0 /. (i + 1)),P c= g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A327: x in Segment (h0 /. i),(h0 /. (i + 1)),P ; :: thesis:
h0 /. (i + 1) <> W-min P by A22, A29, A31, A67, A288, A296, A305, A307, A308, A313, A317, FUNCT_1:def 8;
then x in { p where p is Point of (TOP-REAL 2) : ( LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) } by A327, Def1;
then consider p being Point of (TOP-REAL 2) such that
A328: ( p = x & LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) ;
A329: ( ( 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 A328, JORDAN6:def 10;
A330: ((i -' (len h11)) + 2) -' 1 < len h2 by A299, A307, NAT_1:13;
A331: h0 /. (i + 1) <> E-max P by A22, A28, A30, A67, A296, A308, A312, A313, A317, FUNCT_1:def 8;
A332: h21 . ((((i -' (len h11)) + 2) -' 1) + 1) <> W-min P by A22, A29, A31, A67, A288, A305, A307, A313, FUNCT_1:def 8;

now

assume h0 /. (i + 1) in Upper_Arc P ; :: thesis:
then h0 /. (i + 1) in (Upper_Arc P) /\ (Lower_Arc P) by A317, A319, XBOOLE_0:def 4;
then h0 /. (i + 1) in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
hence contradiction by A296, A308, A317, A331, A332, TARSKI:def 2; :: thesis:

end;

then A333: ( ( 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 A328, JORDAN6:def 10;
A334: h0 /. i <> W-min P by A22, A29, A31, A67, A290, A309, A316, A330, FUNCT_1:def 8;
A335: h21 . (((i -' (len h11)) + 2) -' 1) <> E-max P by A22, A28, A30, A67, A304, A309, FUNCT_1:def 8;

A336: now

assume h0 /. i in Upper_Arc P ; :: thesis:
then h0 /. i in (Upper_Arc P) /\ (Lower_Arc P) by A316, A318, XBOOLE_0:def 4;
then h0 /. i in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
hence contradiction by A290, A316, A334, A335, TARSKI:def 2; :: thesis:

end;

then A337: LE h0 /. i,p, Lower_Arc P, E-max P, W-min P by A328, JORDAN6:def 10;
A338: h0 /. i <> E-max P by A22, A28, A30, A67, A290, A304, A309, A316, FUNCT_1:def 8;

A339: now

assume p in Upper_Arc P ; :: thesis:
then p in (Upper_Arc P) /\ (Lower_Arc P) by A329, A336, 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 A11, A329, A336, A338, JORDAN6:69; :: thesis:

end;

then A340: LE p,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P by A328, JORDAN6:def 10;
consider z being set such that
A341: ( z in dom g2 & p = g2 . z ) by A13, A333, A339, FUNCT_1:def 5;
reconsider rz = z as Real by A15, A341;
A342: g2 . (h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)) = h0 /. (i + 1) by A296, A308, A313, A317, A325, FUNCT_1:23;
A343: ( 0 <= h2 /. (((i -' (len h11)) + 2) -' 1) & h2 /. (((i -' (len h11)) + 2) -' 1) <= 1 ) by A16, A311, A324, BORSUK_1:83, XXREAL_1:1;
h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by A313, FUNCT_1:def 5;
then ( 0 <= rz & rz <= 1 & 0 <= h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) & h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) <= 1 ) by A16, A325, A341, BORSUK_1:83, XXREAL_1:1;
then ( rz <= h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) & h2 /. (((i -' (len h11)) + 2) -' 1) <= rz ) by A12, A13, A14, A310, A316, A324, A337, A340, A341, A342, A343, Th20;
then rz in [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] by XXREAL_1:1;
hence x in g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] by A328, A341, FUNCT_1:def 12; :: thesis:

end;

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 set ; :: 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 set such that
A344: ( y in dom g2 & y in [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] & x = g2 . y ) by FUNCT_1:def 12;
A345: x in Lower_Arc P by A13, A344, FUNCT_1:def 5;
then reconsider p1 = x as Point of (TOP-REAL 2) ;
reconsider sy = y as Real by A344;
A346: ( h2 /. (((i -' (len h11)) + 2) -' 1) <= sy & sy <= h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) ) by A344, XXREAL_1:1;
A347: ( 0 <= sy & sy <= 1 ) by A344, BORSUK_1:83, XXREAL_1:1;
A348: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) <> 1 by A16, A29, A288, A305, A307, A313, FUNCT_1:def 8;

A349: now

assume p1 = W-min P ; :: thesis:
then 1 = sy by A12, A14, A32, A344, FUNCT_1:def 8;
hence contradiction by A323, A325, A346, A348, XXREAL_0:1; :: thesis:

end;

A350: h0 /. (i + 1) <> W-min P by A22, A29, A31, A67, A288, A296, A305, A307, A308, A313, A317, FUNCT_1:def 8;
A351: LE h0 /. i,p1, Lower_Arc P, E-max P, W-min P by A11, A12, A13, A14, A310, A316, A320, A321, A324, A344, A346, A347, Th19;
LE p1,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P by A11, A12, A13, A14, A322, A323, A325, A344, A346, A347, Th19;
then ( LE h0 /. i,p1,P & LE p1,h0 /. (i + 1),P ) by A316, A317, A318, A319, A345, A349, A350, A351, 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 ) } ;
hence x in Segment (h0 /. i),(h0 /. (i + 1)),P by A350, Def1; :: thesis:

end;

then W = g2 .: Q1 by A206, A326, XBOOLE_0:def 10;
hence diameter W < e by A16, A301, A306; :: thesis:

end;

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

then A353: h0 . i = E-max P by A21, A37, A206, FINSEQ_1:85;
A354: i - (len h11) = i -' (len h11) by A21, A352, XREAL_1:235;
A355: h0 . (i + 1) = (mid h21,2,((len h21) -' 1)) . ((i + 1) - (len h11)) by A21, A40, A207, A352, FINSEQ_1:36;
A356: (i + 1) - (len h11) = (i + 1) -' (len h11) by A21, A209, A352, XREAL_1:235;
A357: (i + 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A207, XREAL_1:11;
then ( 1 <= (i + 1) -' (len h11) & (i + 1) -' (len h11) <= len (mid h21,2,((len h21) -' 1)) ) by A21, A209, A352, XREAL_1:235;
then 1 < ((i + 1) -' (len h11)) + (2 - 1) by NAT_1:13;
then A358: 0 < (((i + 1) -' (len h11)) + 2) - 1 ;
A359: 0 + 2 <= (i -' (len h11)) + 2 by XREAL_1:8;
i - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A206, XREAL_1:11;
then A360: (i -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A354, XREAL_1:8;
then A361: ((i -' (len h11)) + 2) - 1 <= (len h2) - 1 by XREAL_1:11;
A362: ( 1 <= ((i -' (len h11)) + 2) -' 1 & ((i -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A359, A360, Lm1, NAT_D:42, NAT_D:44;
len h2 < (len h2) + 1 by NAT_1:13;
then (len h2) - 1 < ((len h2) + 1) - 1 by XREAL_1:11;
then A363: ((i -' (len h11)) + 2) - 1 < len h2 by A361, XXREAL_0:2;
A364: ((i -' (len h11)) + 2) -' 1 = ((i -' (len h11)) + 2) - 1 by A362, NAT_D:39;
set j = ((i -' (len h11)) + 2) -' 1;
(len h1) -' (len h11) = (len h11) - (len h11) by A21, XREAL_0:def 2;
then A365: (0 + 2) - 1 = (((len h1) -' (len h11)) + 2) - 1 ;
i - (len h11) < ((len h11) + ((len h2) - 2)) - (len h11) by A23, A40, A42, A46, A47, A206, XREAL_1:11;
then A366: (i - (len h11)) + 2 < ((len h2) - 2) + 2 by XREAL_1:8;
A367: (((i -' (len h11)) + 2) -' 1) + 1 = ((((i -' (len h11)) + 1) + 1) - 1) + 1 by A362, NAT_D:39
.= (i -' (len h11)) + (1 + 1) ;
then A368: (((i -' (len h11)) + 2) -' 1) + 1 < len h2 by A21, A352, A366, XREAL_0:def 2;
A369: (((i -' (len h11)) + 2) -' 1) + 1 = (((i - (len h11)) + 2) - 1) + 1 by A21, A352, A364, XREAL_0:def 2
.= (((i + 1) -' (len h11)) + 2) -' 1 by A356, A358, XREAL_0:def 2 ;
A370: ((i -' (len h11)) + 2) -' 1 in dom h2 by A22, A362, FINSEQ_3:27;
then A371: h21 . (((i -' (len h11)) + 2) -' 1) = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by FUNCT_1:23;
A372: h0 . i = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by A14, A16, A352, A353, A365, NAT_D:39;
A373: h2 . (((i -' (len h11)) + 2) -' 1) in rng h2 by A370, FUNCT_1:def 5;
A374: 1 < (((i -' (len h11)) + 2) -' 1) + 1 by A362, NAT_1:13;
A375: h0 . (i + 1) = h21 . ((((i -' (len h11)) + 2) -' 1) + 1) by A21, A43, A45, A352, A355, A356, A357, A369, JORDAN3:27;
A376: (((i -' (len h11)) + 2) -' 1) + 1 in dom h2 by A360, A367, A374, FINSEQ_3:27;
then A377: h0 . (i + 1) = g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) by A375, FUNCT_1:23;
A378: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by A376, FUNCT_1:def 5;
i in dom h0 by A206, FINSEQ_3:27;
then A379: h0 /. i = h0 . i by PARTFUN1:def 8;
i + 1 in dom h0 by A207, A208, FINSEQ_3:27;
then A380: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) in rng g2 by A15, A16, A373, BORSUK_1:83, FUNCT_1:def 5;
then A381: h0 . i in Lower_Arc P by A13, A14, A16, A352, A353, A365, NAT_D:39;
A382: h0 . (i + 1) in Lower_Arc P by A13, A15, A16, A377, A378, BORSUK_1:83, FUNCT_1:def 5;
A383: ( 1 <= ((i -' (len h11)) + 2) -' 1 & ((i -' (len h11)) + 2) -' 1 < len h2 ) by A362, A363, NAT_D:39;
A384: g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) = h0 /. (i + 1) by A375, A376, A380, FUNCT_1:23;
A385: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) <= 1 by A16, A378, BORSUK_1:83, XXREAL_1:1;
A386: h2 /. (((i -' (len h11)) + 2) -' 1) = h2 . (((i -' (len h11)) + 2) -' 1) by A383, FINSEQ_4:24;
A387: h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) = h2 . ((((i -' (len h11)) + 2) -' 1) + 1) by A360, A367, A374, FINSEQ_4:24;
then reconsider Q1 = [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] as Subset of I[01] by A16, A373, A378, A386, BORSUK_1:83, XXREAL_2:def 12;
A388: Segment (h0 /. i),(h0 /. (i + 1)),P c= g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A389: x in Segment (h0 /. i),(h0 /. (i + 1)),P ; :: thesis:
h0 /. (i + 1) <> W-min P by A22, A29, A31, A67, A368, A375, A376, A380, FUNCT_1:def 8;
then x in { p where p is Point of (TOP-REAL 2) : ( LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) } by A389, Def1;
then consider p being Point of (TOP-REAL 2) such that
A390: ( p = x & LE h0 /. i,p,P & LE p,h0 /. (i + 1),P ) ;
A391: ( ( 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 A390, JORDAN6:def 10;
(((i -' (len h11)) + 2) -' 1) + 1 < len h2 by A21, A352, A366, A367, XREAL_0:def 2;
then A392: ((i -' (len h11)) + 2) -' 1 < len h2 by NAT_1:13;
A393: not h0 /. (i + 1) = E-max P by A22, A28, A30, A67, A374, A375, A376, A380, FUNCT_1:def 8;
A394: h0 /. (i + 1) in Lower_Arc P by A13, A15, A16, A377, A378, A380, BORSUK_1:83, FUNCT_1:def 5;

now

assume h0 /. (i + 1) in Upper_Arc P ; :: thesis:
then h0 /. (i + 1) in (Upper_Arc P) /\ (Lower_Arc P) by A394, 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 A375, A380, A393, TARSKI:def 2;
hence contradiction by A22, A29, A31, A67, A368, A376, FUNCT_1:def 8; :: thesis:

end;

then A395: ( ( 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 A390, JORDAN6:def 10;
A396: h0 /. i <> W-min P by A22, A29, A31, A67, A370, A371, A372, A379, A392, FUNCT_1:def 8;
dom (g1 * h1) c= dom h0 by FINSEQ_1:39;
then A397: h0 /. i = E-max P by A36, A352, A353, PARTFUN1:def 8;

A398: now

assume A399: not p in Lower_Arc P ; :: thesis:
then p = E-max P by A2, A391, A397, JORDAN6:70;
hence contradiction by A1, A399, Th1; :: thesis:

end;

A400: now

assume p in Upper_Arc P ; :: thesis:
then p in (Upper_Arc P) /\ (Lower_Arc P) by A398, XBOOLE_0:def 4;
then A401: p in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
p <> W-min P by A2, A391, A396, JORDAN6:69;
hence p = E-max P by A401, TARSKI:def 2; :: thesis:

end;

then A402: LE p,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P by A11, A395, JORDAN5C:10;
p in rng g2 by A1, A13, A390, A400, Th1, JORDAN6:def 10;
then consider z being set such that
A403: ( z in dom g2 & p = g2 . z ) by FUNCT_1:def 5;
reconsider rz = z as Real by A15, A403;
A404: g2 . (h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)) = h0 /. (i + 1) by A360, A367, A374, A377, A380, FINSEQ_4:24;
h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by A376, FUNCT_1:def 5;
then ( 0 <= rz & rz <= 1 & 0 <= h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) & h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) <= 1 ) by A16, A387, A403, BORSUK_1:83, XXREAL_1:1;
then ( rz <= h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) & h2 /. (((i -' (len h11)) + 2) -' 1) <= rz ) by A12, A13, A14, A16, A352, A365, A386, A402, A403, A404, Th20, NAT_D:39;
then rz in [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] by XXREAL_1:1;
hence x in g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] by A390, A403, FUNCT_1:def 12; :: thesis:

end;

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 set ; :: 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 set such that
A405: ( y in dom g2 & y in [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] & x = g2 . y ) by FUNCT_1:def 12;
A406: x in Lower_Arc P by A13, A405, FUNCT_1:def 5;
then reconsider p1 = x as Point of (TOP-REAL 2) ;
reconsider sy = y as Real by A405;
A407: ( h2 /. (((i -' (len h11)) + 2) -' 1) <= sy & sy <= h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) ) by A405, XXREAL_1:1;
A408: ( 0 <= sy & sy <= 1 ) by A405, BORSUK_1:83, XXREAL_1:1;
A409: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) <> 1 by A16, A29, A368, A376, FUNCT_1:def 8;

A410: now

assume p1 = W-min P ; :: thesis:
then 1 = sy by A12, A14, A32, A405, FUNCT_1:def 8;
hence contradiction by A385, A387, A407, A409, XXREAL_0:1; :: thesis:

end;

A411: h0 /. (i + 1) <> W-min P by A22, A29, A31, A67, A368, A375, A376, A380, FUNCT_1:def 8;
LE h0 /. i,p1, Lower_Arc P, E-max P, W-min P by A11, A12, A13, A14, A353, A379, A405, A408, Th19;
then A412: LE h0 /. i,p1,P by A379, A381, A406, A410, JORDAN6:def 10;
LE p1,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P by A11, A12, A13, A14, A384, A385, A387, A405, A407, A408, Th19;
then LE p1,h0 /. (i + 1),P by A380, A382, A406, A411, 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 A412;
hence x in Segment (h0 /. i),(h0 /. (i + 1)),P by A411, Def1; :: thesis:

end;

then W = g2 .: Q1 by A206, A388, XBOOLE_0:def 10;
hence diameter W < e by A16, A383; :: thesis:

end;

thus for W being Subset of (Euclid 2) st W = Segment (h0 /. (len h0)),(h0 /. 1),P holds
diameter W < e :: thesis:

proof

let W be Subset of (Euclid 2); :: thesis:
assume A413: W = Segment (h0 /. (len h0)),(h0 /. 1),P ; :: thesis:
set i = len h0;
len h0 <= (len h11) + (len (mid h21,2,((len h21) -' 1))) by FINSEQ_1:35;
then A414: h0 . (len h0) = (mid h21,2,((len h21) -' 1)) . ((len h0) - (len h11)) by A21, A51, FINSEQ_1:36;
A415: (len h0) - (len h11) = (len h0) -' (len h11) by A21, A52, XREAL_1:235;
A416: (len h0) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by FINSEQ_1:35;
((len h1) + 1) - (len h1) <= (len h0) - (len h1) by A48, A49, XXREAL_0:2;
then A417: h0 . (len h0) = h21 . ((((len h0) -' (len h11)) + 2) -' 1) by A21, A43, A45, A414, A415, A416, JORDAN3:27;
A418: 0 + 2 <= ((len h0) -' (len h11)) + 2 by XREAL_1:8;
then A419: 2 -' 1 <= (((len h0) -' (len h11)) + 2) -' 1 by NAT_D:42;
A420: ( 1 <= (((len h0) -' (len h11)) + 2) -' 1 & (((len h0) -' (len h11)) + 2) -' 1 <= len h21 ) by A40, A42, A46, A47, A415, A418, Lm1, NAT_D:42, NAT_D:44;
len h2 < (len h2) + 1 by NAT_1:13;
then A421: (len h2) - 1 < ((len h2) + 1) - 1 by XREAL_1:11;
A422: (((len h0) -' (len h11)) + 2) -' 1 = (((len h0) -' (len h11)) + 2) - 1 by A419, Lm1, NAT_D:39;
set j = (((len h0) -' (len h11)) + 2) -' 1;
((len h11) + 1) - (len h11) <= (len h0) - (len h11) by A23, A40, A42, A46, A47, A49, XXREAL_0:2;
then 1 <= (len h0) -' (len h11) by NAT_D:39;
then 1 + 2 <= ((len h0) -' (len h11)) + 2 by XREAL_1:8;
then (1 + 2) - 1 <= (((len h0) -' (len h11)) + 2) - 1 by XREAL_1:11;
then A423: 1 < (((len h0) -' (len h11)) + 2) -' 1 by A422, XXREAL_0:2;
A424: (((len h0) -' (len h11)) + 2) -' 1 in dom h2 by A22, A420, FINSEQ_3:27;
then A425: h0 . (len h0) = g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) by A417, FUNCT_1:23;
A426: h2 . ((((len h0) -' (len h11)) + 2) -' 1) in rng h2 by A424, FUNCT_1:def 5;
then A427: ( 0 <= h2 . ((((len h0) -' (len h11)) + 2) -' 1) & h2 . ((((len h0) -' (len h11)) + 2) -' 1) <= 1 ) by A16, BORSUK_1:83, XXREAL_1:1;
A428: 1 < ((((len h0) -' (len h11)) + 2) -' 1) + 1 by A419, Lm1, NAT_1:13;
A429: h0 . (len h0) in Lower_Arc P by A13, A15, A16, A425, A426, BORSUK_1:83, FUNCT_1:def 5;

A430: now

assume h0 . (len h0) in Upper_Arc P ; :: thesis:
then h0 . (len h0) in (Upper_Arc P) /\ (Lower_Arc P) by A429, 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 A22, A23, A28, A29, A30, A31, A40, A42, A46, A47, A67, A415, A417, A421, A423, A424, FUNCT_1:def 8; :: thesis:

end;

((((len h0) -' (len h11)) + 2) -' 1) + 1 in dom h2 by A22, A40, A42, A46, A47, A415, A428, FINSEQ_3:27;
then A431: h2 . (((((len h0) -' (len h11)) + 2) -' 1) + 1) in rng h2 by FUNCT_1:def 5;
len h0 in dom h0 by A53, FINSEQ_3:27;
then A432: h0 /. (len h0) = h0 . (len h0) by PARTFUN1:def 8;
A433: 0 <= h2 . ((((len h0) -' (len h11)) + 2) -' 1) by A16, A426, BORSUK_1:83, XXREAL_1:1;
A434: h2 . ((((len h0) -' (len h11)) + 2) -' 1) <= 1 by A16, A426, BORSUK_1:83, XXREAL_1:1;
A435: h2 /. ((((len h0) -' (len h11)) + 2) -' 1) = h2 . ((((len h0) -' (len h11)) + 2) -' 1) by A23, A40, A42, A46, A47, A415, A419, A421, Lm1, FINSEQ_4:24;
A436: h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1) = h2 . (((((len h0) -' (len h11)) + 2) -' 1) + 1) by A23, A40, A42, A46, A47, A415, A428, FINSEQ_4:24;
then reconsider Q1 = [.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).] as Subset of I[01] by A16, A426, A431, A435, BORSUK_1:83, XXREAL_2:def 12;
A437: 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 set ; :: according to TARSKI:def 3 :: thesis:
assume A438: x in Segment (h0 /. (len h0)),(h0 /. 1),P ; :: thesis:
h0 /. 1 = W-min P by A39, A63, PARTFUN1:def 8;
then 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 A438, Def1;
then consider p being Point of (TOP-REAL 2) such that
A439: ( p = x & ( LE h0 /. (len h0),p,P or ( h0 /. (len h0) in P & p = W-min P ) ) ) ;
A440: (((len h0) -' (len h11)) + 2) -' 1 < ((((len h0) -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
A441: (((len h0) -' (len h11)) + 2) -' 1 in dom h2 by A23, A40, A42, A46, A47, A415, A419, A421, Lm1, FINSEQ_3:27;
((((len h0) -' (len h11)) + 2) -' 1) + 1 in dom h2 by A22, A40, A42, A46, A47, A415, A428, FINSEQ_3:27;
then h2 . ((((len h0) -' (len h11)) + 2) -' 1) < h2 . (((((len h0) -' (len h11)) + 2) -' 1) + 1) by A16, A440, A441, SEQM_3:def 1;
then A442: 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 A435, A436, XXREAL_1:1;
A443: h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1) = 1 by A16, A23, A29, A40, A42, A46, A47, A415, PARTFUN1:def 8;

now

per cases by A439;

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

then A444: ( h0 /. (len h0) in Lower_Arc P & p in Lower_Arc P & not p = W-min P & LE h0 /. (len h0),p, Lower_Arc P, E-max P, W-min P ) by A430, A432, JORDAN6:def 10;
then consider z being set such that
A445: ( z in dom g2 & p = g2 . z ) by A13, FUNCT_1:def 5;
reconsider rz = z as Real by A15, A445;
take z = z; :: thesis:
A446: ( 0 <= rz & rz <= 1 ) by A445, BORSUK_1:83, XXREAL_1:1;
then A447: h2 /. ((((len h0) -' (len h11)) + 2) -' 1) <= rz by A12, A13, A14, A425, A427, A432, A435, A444, A445, Th20;
thus z in dom g2 by A445; :: thesis:
rz <= h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1) by A16, A23, A40, A42, A46, A47, A415, A428, A446, FINSEQ_4:24;
hence ( z in [.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).] & x = g2 . z ) by A439, A445, A447, XXREAL_1:1; :: thesis:

end;

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

hence ex y being set 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 A14, A32, A439, A442, A443; :: 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 12; :: thesis:

end;

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

let x be set ; :: 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 set such that
A448: ( 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 FUNCT_1:def 12;
A449: x in Lower_Arc P by A13, A448, FUNCT_1:def 5;
then reconsider p1 = x as Point of (TOP-REAL 2) ;
reconsider sy = y as Real by A448;
A450: ( h2 /. ((((len h0) -' (len h11)) + 2) -' 1) <= sy & sy <= h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1) ) by A448, XXREAL_1:1;
A451: ( 0 <= sy & sy <= 1 ) by A448, BORSUK_1:83, XXREAL_1:1;
A452: h0 /. 1 = W-min P by A39, A63, PARTFUN1:def 8;
A453: (Upper_Arc P) \/ (Lower_Arc P) = P by A1, JORDAN6:def 9;
A454: LE h0 /. (len h0),p1, Lower_Arc P, E-max P, W-min P by A11, A12, A13, A14, A425, A432, A433, A434, A435, A448, A450, A451, Th19;

now

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 A429, A432, A453, 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 A429, A432, A449, A454, JORDAN6:def 10; :: thesis:

end;

then 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 ) ) } ;
hence x in Segment (h0 /. (len h0)),(h0 /. 1),P by A452, Def1; :: thesis:

end;

then W = g2 .: Q1 by A413, A437, XBOOLE_0:def 10;
hence diameter W < e by A16, A23, A40, A42, A46, A47, A415, A419, A421, Lm1; :: thesis:

end;

A455: for i being Element of NAT st 1 <= i & i + 1 < len h0 holds
LE h0 /. (i + 1),h0 /. (i + 2),P

proof

let i be Element of NAT ; :: thesis:
assume A456: ( 1 <= i & i + 1 < len h0 ) ; :: thesis:
then A457: (i + 1) + 1 <= len h0 by NAT_1:13;
A458: 1 < i + 1 by A456, NAT_1:13;
then A459: 1 < (i + 1) + 1 by NAT_1:13;
A460: i + 1 < (i + 1) + 1 by NAT_1:13;

per cases ;

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

then A462: (i + 1) + 1 <= len h1 by NAT_1:13;
A463: h0 . (i + 1) = h11 . (i + 1) by A21, A458, A461, FINSEQ_1:85;
A464: i + 1 in dom h1 by A458, A461, FINSEQ_3:27;
then A465: h0 . (i + 1) = g1 . (h1 . (i + 1)) by A463, FUNCT_1:23;
A466: h1 . (i + 1) in rng h1 by A464, FUNCT_1:def 5;
then A467: ( 0 <= h1 . (i + 1) & h1 . (i + 1) <= 1 ) by A9, BORSUK_1:83, XXREAL_1:1;
A468: 1 < (i + 1) + 1 by A458, NAT_1:13;
then A469: h0 . ((i + 1) + 1) = h11 . ((i + 1) + 1) by A21, A462, FINSEQ_1:85;
A470: (i + 1) + 1 in dom h1 by A462, A468, FINSEQ_3:27;
then A471: h0 . ((i + 1) + 1) = g1 . (h1 . ((i + 1) + 1)) by A469, FUNCT_1:23;
A472: h1 . ((i + 1) + 1) in rng h1 by A470, FUNCT_1:def 5;
then A473: h1 . ((i + 1) + 1) <= 1 by A9, BORSUK_1:83, XXREAL_1:1;
A474: h1 . (i + 1) < h1 . ((i + 1) + 1) by A9, A460, A464, A470, SEQM_3:def 1;
i + 1 in dom h0 by A456, A458, FINSEQ_3:27;
then A475: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
(i + 1) + 1 in dom h0 by A457, A468, FINSEQ_3:27;
then A476: h0 /. ((i + 1) + 1) = h0 . ((i + 1) + 1) by PARTFUN1:def 8;
g1 . (h1 . (i + 1)) in rng g1 by A6, A9, A466, BORSUK_1:83, FUNCT_1:def 5;
then A477: h0 /. (i + 1) in Upper_Arc P by A4, A463, A464, A475, FUNCT_1:23;
A478: h0 /. ((i + 1) + 1) in Upper_Arc P by A4, A6, A9, A471, A472, A476, BORSUK_1:83, FUNCT_1:def 5;
LE h0 /. (i + 1),h0 /. ((i + 1) + 1), Upper_Arc P, W-min P, E-max P by A2, A3, A4, A5, A465, A467, A471, A473, A474, A475, A476, Th19;
hence LE h0 /. (i + 1),h0 /. (i + 2),P by A477, A478, JORDAN6:def 10; :: thesis:

end;

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

per cases by A479, XXREAL_0:1;

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

then A481: (len h1) + 1 <= i + 1 by NAT_1:13;
A482: (len h11) + 1 <= i + 1 by A21, A480, NAT_1:13;
A483: i + 1 <= (len h11) + (len (mid h21,2,((len h21) -' 1))) by A456, FINSEQ_1:35;
then A484: h0 . (i + 1) = (mid h21,2,((len h21) -' 1)) . ((i + 1) - (len h11)) by A482, FINSEQ_1:36;
A485: (i + 1) - (len h11) = (i + 1) -' (len h11) by A21, A480, XREAL_1:235;
A486: (i + 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A483, XREAL_1:11;
((len h1) + 1) - (len h1) <= (i + 1) - (len h1) by A481, XREAL_1:11;
then A487: h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A484, A485, A486, JORDAN3:27;
A488: (len h1) + 1 <= (i + 1) + 1 by A481, NAT_1:13;
then A489: h0 . ((i + 1) + 1) = (mid h21,2,((len h21) -' 1)) . (((i + 1) + 1) - (len h11)) by A21, A40, A457, FINSEQ_1:36;
(i + 1) + 1 > len h11 by A21, A480, NAT_1:13;
then A490: ((i + 1) + 1) - (len h11) = ((i + 1) + 1) -' (len h11) by XREAL_1:235;
A491: ((i + 1) + 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A457, XREAL_1:11;
A492: ((len h1) + 1) - (len h1) <= ((i + 1) + 1) - (len h1) by A488, XREAL_1:11;
then A493: h0 . ((i + 1) + 1) = h21 . (((((i + 1) + 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A489, A490, A491, JORDAN3:27;
1 < (((i + 1) + 1) -' (len h11)) + (2 - 1) by A21, A490, A492, NAT_1:13;
then A494: 0 < ((((i + 1) + 1) -' (len h11)) + 2) - 1 ;
A495: 0 + 2 <= ((i + 1) -' (len h11)) + 2 by XREAL_1:8;
then A496: 2 -' 1 <= (((i + 1) -' (len h11)) + 2) -' 1 by NAT_D:42;
(i + 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A456, XREAL_1:11;
then A497: ((i + 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A485, XREAL_1:8;
then A498: ( 1 <= (((i + 1) -' (len h11)) + 2) -' 1 & (((i + 1) -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A495, Lm1, NAT_D:42, NAT_D:44;
A499: (((i + 1) -' (len h11)) + 2) -' 1 = (((i + 1) -' (len h11)) + 2) - 1 by A496, Lm1, NAT_D:39;
set j = (((i + 1) -' (len h11)) + 2) -' 1;
(i + 1) - (len h11) < ((len h11) + ((len h2) - 2)) - (len h11) by A23, A40, A42, A46, A47, A456, XREAL_1:11;
then A500: ((i + 1) - (len h11)) + 2 < ((len h2) - 2) + 2 by XREAL_1:8;
A501: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 = ((((i + 1) -' (len h11)) + (1 + 1)) - 1) + 1 by A496, Lm1, NAT_D:39
.= ((i + 1) -' (len h11)) + 2 ;
A502: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 = ((((i + 1) + 1) -' (len h11)) + 2) -' 1 by A485, A490, A494, A499, XREAL_0:def 2;
A503: (((i + 1) -' (len h11)) + 2) -' 1 in dom h2 by A22, A498, FINSEQ_3:27;
then A504: h0 . (i + 1) = g2 . (h2 . ((((i + 1) -' (len h11)) + 2) -' 1)) by A487, FUNCT_1:23;
A505: h2 . ((((i + 1) -' (len h11)) + 2) -' 1) in rng h2 by A503, FUNCT_1:def 5;
then A506: ( 0 <= h2 . ((((i + 1) -' (len h11)) + 2) -' 1) & h2 . ((((i + 1) -' (len h11)) + 2) -' 1) <= 1 ) by A16, BORSUK_1:83, XXREAL_1:1;
A507: (((i + 1) -' (len h11)) + 2) -' 1 < ((((i + 1) -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
1 < ((((i + 1) -' (len h11)) + 2) -' 1) + 1 by A496, Lm1, NAT_1:13;
then A508: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 in dom h2 by A497, A501, FINSEQ_3:27;
then A509: ( h0 . ((i + 1) + 1) = g2 . (h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1)) & h21 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1) = g2 . (h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1)) ) by A493, A502, FUNCT_1:23;
A510: h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1) in rng h2 by A508, FUNCT_1:def 5;
A511: h2 . ((((i + 1) -' (len h11)) + 2) -' 1) < h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1) by A16, A503, A507, A508, SEQM_3:def 1;
i + 1 in dom h0 by A456, A458, FINSEQ_3:27;
then A512: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
(i + 1) + 1 in dom h0 by A457, A459, FINSEQ_3:27;
then A513: h0 /. ((i + 1) + 1) = h0 . ((i + 1) + 1) by PARTFUN1:def 8;
A514: h0 . (i + 1) in Lower_Arc P by A13, A15, A16, A504, A505, BORSUK_1:83, FUNCT_1:def 5;
A515: h0 . ((i + 1) + 1) in Lower_Arc P by A13, A15, A16, A509, A510, BORSUK_1:83, FUNCT_1:def 5;
A516: h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1) <= 1 by A16, A510, BORSUK_1:83, XXREAL_1:1;
A517: h0 /. ((i + 1) + 1) <> W-min P by A22, A29, A31, A67, A485, A493, A500, A501, A502, A508, A513, FUNCT_1:def 8;
LE h0 /. (i + 1),h0 /. ((i + 1) + 1), Lower_Arc P, E-max P, W-min P by A11, A12, A13, A14, A504, A506, A509, A511, A512, A513, A516, Th19;
hence LE h0 /. (i + 1),h0 /. (i + 2),P by A512, A513, A514, A515, A517, JORDAN6:def 10; :: thesis:

end;

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

then A519: h0 . (len h1) = E-max P by A21, A37, A458, FINSEQ_1:85;
A520: (len h1) - (len h11) = (len h1) -' (len h11) by A21, XREAL_1:235;
A521: (len h1) + 1 <= (len h11) + (len (mid h21,2,((len h21) -' 1))) by A457, A518, FINSEQ_1:35;
A522: h0 . ((i + 1) + 1) = (mid h21,2,((len h21) -' 1)) . (((i + 1) + 1) - (len h11)) by A21, A40, A457, A518, FINSEQ_1:36;
A523: ((i + 1) + 1) - (len h11) = ((i + 1) + 1) -' (len h11) by A21, A460, A518, XREAL_1:235;
A524: ((i + 1) + 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A518, A521, XREAL_1:11;
then A525: ( 1 <= ((i + 1) + 1) -' (len h11) & ((i + 1) + 1) -' (len h11) <= len (mid h21,2,((len h21) -' 1)) ) by A21, A460, A518, XREAL_1:235;
A526: h0 . ((i + 1) + 1) = h21 . (((((i + 1) + 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A518, A522, A523, A524, JORDAN3:27;
1 < (((i + 1) + 1) -' (len h11)) + (2 - 1) by A525, NAT_1:13;
then A527: 0 < ((((i + 1) + 1) -' (len h11)) + 2) - 1 ;
0 + 2 <= ((i + 1) -' (len h11)) + 2 by XREAL_1:8;
then A528: 2 -' 1 <= (((i + 1) -' (len h11)) + 2) -' 1 by NAT_D:42;
(i + 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A456, XREAL_1:11;
then A529: ((i + 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A518, A520, XREAL_1:8;
set j = (((i + 1) -' (len h11)) + 2) -' 1;
(i + 1) - (len h11) < ((len h11) + ((len h2) - 2)) - (len h11) by A23, A40, A42, A46, A47, A456, XREAL_1:11;
then A530: ((i + 1) - (len h11)) + 2 < ((len h2) - 2) + 2 by XREAL_1:8;
A531: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 = ((((i + 1) -' (len h11)) + (1 + 1)) - 1) + 1 by A528, Lm1, NAT_D:39
.= ((i + 1) -' (len h11)) + (1 + 1) ;
then A532: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 < len h2 by A21, A518, A530, XREAL_0:def 2;
A533: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 = ((((i + 1) - (len h11)) + 2) - 1) + 1 by A21, A518, Lm1, XREAL_0:def 2
.= ((((i + 1) + 1) -' (len h11)) + 2) -' 1 by A523, A527, XREAL_0:def 2 ;
1 < ((((i + 1) -' (len h11)) + 2) -' 1) + 1 by A528, Lm1, NAT_1:13;
then A534: ((((i + 1) -' (len h11)) + 2) -' 1) + 1 in dom h2 by A529, A531, FINSEQ_3:27;
then A535: ( h0 . ((i + 1) + 1) = g2 . (h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1)) & h21 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1) = g2 . (h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1)) ) by A526, A533, FUNCT_1:23;
A536: h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1) in rng h2 by A534, FUNCT_1:def 5;
len h1 in dom h0 by A456, A458, A518, FINSEQ_3:27;
then A537: h0 /. (len h1) = h0 . (len h1) by PARTFUN1:def 8;
(i + 1) + 1 in dom h0 by A457, A459, FINSEQ_3:27;
then A538: h0 /. ((i + 1) + 1) = h0 . ((i + 1) + 1) by PARTFUN1:def 8;
A539: h0 . ((i + 1) + 1) in Lower_Arc P by A13, A15, A16, A535, A536, BORSUK_1:83, FUNCT_1:def 5;
A540: h0 . (i + 1) in Upper_Arc P by A1, A518, A519, Th1;
h0 /. ((i + 1) + 1) <> W-min P by A22, A29, A31, A67, A526, A532, A533, A534, A538, FUNCT_1:def 8;
hence LE h0 /. (i + 1),h0 /. (i + 2),P by A518, A537, A538, A539, A540, JORDAN6:def 10; :: thesis:

end;

A541: for i being Element of 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 Element of NAT ; :: thesis:
assume that
A542: 1 <= i and
A543: i + 1 <= len h0 ; :: thesis:
A544: 1 < i + 1 by A542, NAT_1:13;
A545: i < len h0 by A543, NAT_1:13;
A546: i < i + 1 by NAT_1:13;
i in dom h0 by A542, A545, FINSEQ_3:27;
then A547: h0 /. i = h0 . i by PARTFUN1:def 8;
i + 1 in dom h0 by A543, A544, FINSEQ_3:27;
then A548: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;

per cases ;

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

then A550: i + 1 <= len h1 by NAT_1:13;
A551: h0 . i = h11 . i by A21, A542, A549, FINSEQ_1:85;
A552: i in dom h1 by A542, A549, FINSEQ_3:27;
then A553: h1 . i in rng h1 by FUNCT_1:def 5;
A554: h0 . (i + 1) = h11 . (i + 1) by A21, A544, A550, FINSEQ_1:85;
A555: i + 1 in dom h1 by A544, A550, FINSEQ_3:27;
then A556: h0 . (i + 1) = g1 . (h1 . (i + 1)) by A554, FUNCT_1:23;
A557: h1 . (i + 1) in rng h1 by A555, FUNCT_1:def 5;
A558: h1 . i < h1 . (i + 1) by A9, A546, A552, A555, SEQM_3:def 1;
g1 . (h1 . i) in rng g1 by A6, A9, A553, BORSUK_1:83, FUNCT_1:def 5;
then A559: h0 . i in Upper_Arc P by A4, A551, A552, FUNCT_1:23;
A560: h0 . (i + 1) in Upper_Arc P by A4, A6, A9, A556, A557, BORSUK_1:83, FUNCT_1:def 5;
A561: g1 . (h1 . i) = h0 /. i by A547, A551, A552, FUNCT_1:23;
A562: 0 <= h1 . i by A9, A553, BORSUK_1:83, XXREAL_1:1;
A563: h1 . i <= 1 by A9, A553, BORSUK_1:83, XXREAL_1:1;
A564: h1 . (i + 1) <= 1 by A9, A557, BORSUK_1:83, XXREAL_1:1;
A565: i + 1 <> 1 by A542, NAT_1:13;
A566: i + 1 <> i ;
LE h0 /. i,h0 /. (i + 1), Upper_Arc P, W-min P, E-max P by A2, A3, A4, A5, A548, A556, A558, A561, A562, A563, A564, Th19;
hence ( LE h0 /. i,h0 /. (i + 1),P & h0 /. (i + 1) <> W-min P & h0 /. i <> h0 /. (i + 1) ) by A20, A25, A38, A66, A547, A548, A551, A552, A554, A555, A559, A560, A565, A566, FUNCT_1:def 8, JORDAN6:def 10; :: thesis:

end;

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

per cases by A567, XXREAL_0:1;

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

then A569: (len h1) + 1 <= i by NAT_1:13;
A570: ( (len h11) + 1 <= i & i <= (len h11) + (len (mid h21,2,((len h21) -' 1))) ) by A21, A545, A568, FINSEQ_1:35, NAT_1:13;
then A571: h0 . i = (mid h21,2,((len h21) -' 1)) . (i - (len h11)) by FINSEQ_1:36;
A572: i - (len h11) = i -' (len h11) by A21, A568, XREAL_1:235;
A573: i - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A570, XREAL_1:11;
((len h1) + 1) - (len h1) <= i - (len h1) by A569, XREAL_1:11;
then A574: h0 . i = h21 . (((i -' (len h11)) + 2) -' 1) by A21, A43, A45, A571, A572, A573, JORDAN3:27;
A575: (len h1) + 1 <= i + 1 by A569, NAT_1:13;
then A576: h0 . (i + 1) = (mid h21,2,((len h21) -' 1)) . ((i + 1) - (len h11)) by A21, A40, A543, FINSEQ_1:36;
i + 1 > len h11 by A21, A568, NAT_1:13;
then A577: (i + 1) - (len h11) = (i + 1) -' (len h11) by XREAL_1:235;
A578: (i + 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A543, XREAL_1:11;
A579: ((len h1) + 1) - (len h1) <= (i + 1) - (len h1) by A575, XREAL_1:11;
then A580: h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A576, A577, A578, JORDAN3:27;
1 < ((i + 1) -' (len h11)) + (2 - 1) by A21, A577, A579, NAT_1:13;
then A581: 0 < (((i + 1) -' (len h11)) + 2) - 1 ;
A582: 0 + 2 <= (i -' (len h11)) + 2 by XREAL_1:8;
then A583: 2 -' 1 <= ((i -' (len h11)) + 2) -' 1 by NAT_D:42;
i - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A545, XREAL_1:11;
then A584: (i -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A572, XREAL_1:8;
A585: 1 <= ((i -' (len h11)) + 2) -' 1 by A582, Lm1, NAT_D:42;
A586: ((i -' (len h11)) + 2) -' 1 <= len h21 by A23, A584, NAT_D:44;
set j = ((i -' (len h11)) + 2) -' 1;
i - (len h11) < ((len h11) + ((len h2) - 2)) - (len h11) by A23, A40, A42, A46, A47, A545, XREAL_1:11;
then A587: (i - (len h11)) + 2 < ((len h2) - 2) + 2 by XREAL_1:8;
A588: (((i -' (len h11)) + 2) -' 1) + 1 = (((i -' (len h11)) + (1 + 1)) - 1) + 1 by A583, Lm1, NAT_D:39
.= (i -' (len h11)) + (1 + 1) ;
A589: (((i -' (len h11)) + 2) -' 1) + 1 = (((i - (len h11)) + 2) - 1) + 1 by A572, A583, Lm1, NAT_D:39
.= (((i + 1) -' (len h11)) + 2) -' 1 by A577, A581, XREAL_0:def 2 ;
A590: ((i -' (len h11)) + 2) -' 1 in dom h2 by A22, A585, A586, FINSEQ_3:27;
then A591: h0 . i = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by A574, FUNCT_1:23;
A592: h2 . (((i -' (len h11)) + 2) -' 1) in rng h2 by A590, FUNCT_1:def 5;
A593: ((i -' (len h11)) + 2) -' 1 < (((i -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
1 < (((i -' (len h11)) + 2) -' 1) + 1 by A585, NAT_1:13;
then A594: (((i -' (len h11)) + 2) -' 1) + 1 in dom h2 by A572, A587, A588, FINSEQ_3:27;
then A595: ( h0 . (i + 1) = g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) & h21 . ((((i -' (len h11)) + 2) -' 1) + 1) = g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) ) by A580, A589, FUNCT_1:23;
A596: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by A594, FUNCT_1:def 5;
A597: h2 . (((i -' (len h11)) + 2) -' 1) < h2 . ((((i -' (len h11)) + 2) -' 1) + 1) by A16, A590, A593, A594, SEQM_3:def 1;
i in dom h0 by A542, A545, FINSEQ_3:27;
then A598: h0 /. i = h0 . i by PARTFUN1:def 8;
i + 1 in dom h0 by A543, A544, FINSEQ_3:27;
then A599: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
A600: 0 <= h2 . (((i -' (len h11)) + 2) -' 1) by A16, A592, BORSUK_1:83, XXREAL_1:1;
A601: h2 . (((i -' (len h11)) + 2) -' 1) <= 1 by A16, A592, BORSUK_1:83, XXREAL_1:1;
A602: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) <= 1 by A16, A596, BORSUK_1:83, XXREAL_1:1;
A603: h0 /. (i + 1) <> W-min P by A22, A29, A31, A67, A572, A580, A587, A588, A589, A594, A599, FUNCT_1:def 8;
A604: ((i -' (len h11)) + 2) -' 1 < (((i -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
( h0 /. i in Lower_Arc P & h0 /. (i + 1) in Lower_Arc P & LE h0 /. i,h0 /. (i + 1), Lower_Arc P, E-max P, W-min P ) by A11, A12, A13, A14, A15, A16, A591, A592, A595, A596, A597, A598, A599, A600, A601, A602, Th19, BORSUK_1:83, FUNCT_1:def 5;
hence ( LE h0 /. i,h0 /. (i + 1),P & h0 /. (i + 1) <> W-min P & h0 /. i <> h0 /. (i + 1) ) by A22, A67, A574, A580, A589, A590, A594, A598, A599, A603, A604, FUNCT_1:def 8, JORDAN6:def 10; :: thesis:

end;

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

then A606: h0 . i = E-max P by A21, A37, A542, FINSEQ_1:85;
A607: i - (len h11) = i -' (len h11) by A21, A605, XREAL_1:235;
A608: i + 1 <= (len h11) + (len (mid h21,2,((len h21) -' 1))) by A543, FINSEQ_1:35;
A609: h0 . (i + 1) = (mid h21,2,((len h21) -' 1)) . ((i + 1) - (len h11)) by A21, A40, A543, A605, FINSEQ_1:36;
A610: (i + 1) - (len h11) = (i + 1) -' (len h11) by A21, A546, A605, XREAL_1:235;
(i + 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A608, XREAL_1:11;
then A611: h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A605, A609, A610, JORDAN3:27;
A612: 0 < (((i + 1) -' (len h11)) + 2) - 1 by A21, A605, A610;
A613: 0 + 2 <= (i -' (len h11)) + 2 by XREAL_1:8;
then A614: 2 -' 1 <= ((i -' (len h11)) + 2) -' 1 by NAT_D:42;
i - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A545, XREAL_1:11;
then A615: (i -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A607, XREAL_1:8;
then A616: ( 1 <= ((i -' (len h11)) + 2) -' 1 & ((i -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A613, Lm1, NAT_D:42, NAT_D:44;
set j = ((i -' (len h11)) + 2) -' 1;
(len h1) -' (len h11) = (len h11) - (len h11) by A21, XREAL_0:def 2;
then A617: (0 + 2) - 1 = (((len h1) -' (len h11)) + 2) - 1 ;
i - (len h11) < ((len h11) + ((len h2) - 2)) - (len h11) by A23, A40, A42, A46, A47, A545, XREAL_1:11;
then A618: (i - (len h11)) + 2 < ((len h2) - 2) + 2 by XREAL_1:8;
A619: (((i -' (len h11)) + 2) -' 1) + 1 = (((i -' (len h11)) + (1 + 1)) - 1) + 1 by A614, Lm1, NAT_D:39
.= (i -' (len h11)) + 2 ;
then A620: (((i -' (len h11)) + 2) -' 1) + 1 < len h2 by A21, A605, A618, XREAL_0:def 2;
A621: (((i -' (len h11)) + 2) -' 1) + 1 = (((i - (len h11)) + 2) - 1) + 1 by A21, A605, Lm1, XREAL_0:def 2
.= (((i + 1) -' (len h11)) + 2) -' 1 by A610, A612, XREAL_0:def 2 ;
A622: ((i -' (len h11)) + 2) -' 1 in dom h2 by A22, A616, FINSEQ_3:27;
then A623: h21 . (((i -' (len h11)) + 2) -' 1) = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by FUNCT_1:23;
A624: h0 . i = g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) by A14, A16, A605, A606, A617, NAT_D:39;
1 < (((i -' (len h11)) + 2) -' 1) + 1 by A614, Lm1, NAT_1:13;
then A625: (((i -' (len h11)) + 2) -' 1) + 1 in dom h2 by A615, A619, FINSEQ_3:27;
then A626: h0 . (i + 1) = g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) by A611, A621, FUNCT_1:23;
A627: h2 . ((((i -' (len h11)) + 2) -' 1) + 1) in rng h2 by A625, FUNCT_1:def 5;
i in dom h0 by A542, A545, FINSEQ_3:27;
then A628: h0 /. i = h0 . i by PARTFUN1:def 8;
i + 1 in dom h0 by A543, A544, FINSEQ_3:27;
then A629: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
A630: h0 . (i + 1) in Lower_Arc P by A13, A15, A16, A626, A627, BORSUK_1:83, FUNCT_1:def 5;
A631: h0 . i in Upper_Arc P by A1, A606, Th1;
A632: h0 /. (i + 1) <> W-min P by A22, A29, A31, A67, A611, A620, A621, A625, A629, FUNCT_1:def 8;
(((i -' (len h11)) + 2) -' 1) + 1 <> ((i -' (len h11)) + 2) -' 1 ;
hence ( LE h0 /. i,h0 /. (i + 1),P & h0 /. (i + 1) <> W-min P & h0 /. i <> h0 /. (i + 1) ) by A22, A67, A611, A621, A622, A623, A624, A625, A628, A629, A630, A631, A632, FUNCT_1:def 8, JORDAN6:def 10; :: thesis:

end;

thus for i being Element of 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 Element of NAT ; :: thesis:
assume A633: ( 1 <= i & i + 1 < len h0 ) ; :: thesis:
then A634: ( LE h0 /. i,h0 /. (i + 1),P & h0 /. (i + 1) <> W-min P & h0 /. i <> h0 /. (i + 1) ) by A541;
A635: LE h0 /. (i + 1),h0 /. (i + 2),P by A455, A633;
then h0 /. i <> h0 /. (i + 2) by A1, A634, JORDAN6:72;
hence (Segment (h0 /. i),(h0 /. (i + 1)),P) /\ (Segment (h0 /. (i + 1)),(h0 /. (i + 2)),P) = {(h0 /. (i + 1))} by A1, A634, A635, Th10; :: thesis:

end;

thus (Segment (h0 /. (len h0)),(h0 /. 1),P) /\ (Segment (h0 /. 1),(h0 /. 2),P) = {(h0 /. 1)} :: thesis:

proof

A636: h11 . 2 <> W-min P by A20, A25, A38, A59, A66, FUNCT_1:def 8;
A637: h0 . 2 = g1 . (h1 . 2) by A59, A62, FUNCT_1:23;
A638: h1 . 2 in rng h1 by A59, FUNCT_1:def 5;
A639: h0 /. 2 = h0 . 2 by A61, PARTFUN1:def 8;
then A640: h0 /. 2 in Upper_Arc P by A4, A6, A9, A637, A638, BORSUK_1:83, FUNCT_1:def 5;
A641: ((len h1) + 1) - (len h1) <= (len h0) - (len h1) by A48, A49, XXREAL_0:2;
A642: h0 . (len h0) = (mid h21,2,((len h21) -' 1)) . ((len h0) - (len h11)) by A21, A40, A51, FINSEQ_1:36;
(len h0) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by FINSEQ_1:35;
then A643: h0 . (len h0) = h21 . ((((len h0) -' (len h11)) + 2) -' 1) by A21, A43, A45, A57, A641, A642, JORDAN3:27;
0 + 2 <= ((len h0) -' (len h11)) + 2 by XREAL_1:8;
then A644: ( 1 <= (((len h0) -' (len h11)) + 2) -' 1 & (((len h0) -' (len h11)) + 2) -' 1 <= len h21 ) by A40, A42, A46, A47, A57, Lm1, NAT_D:42, NAT_D:44;
set j = (((len h0) -' (len h11)) + 2) -' 1;
A645: (((len h0) -' (len h11)) + 2) -' 1 in dom h2 by A22, A644, FINSEQ_3:27;
then A646: h0 . (len h0) = g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) by A643, FUNCT_1:23;

A647: now

assume A648: h0 /. 2 = h0 /. (len h0) ; :: thesis:
h2 . ((((len h0) -' (len h11)) + 2) -' 1) in rng h2 by A645, FUNCT_1:def 5;
then g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) in rng g2 by A15, A16, BORSUK_1:83, FUNCT_1:def 5;
then h0 /. 2 in (Upper_Arc P) /\ (Lower_Arc P) by A13, A55, A640, A646, A648, 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 A62, A636, A639, TARSKI:def 2;
hence contradiction by A20, A35, A37, A58, A59, A66, FUNCT_1:def 8; :: thesis:

end;

defpred S₁[ Element of NAT ] means ( $1 + 2 <= len h0 implies LE h0 /. 2,h0 /. ($1 + 2),P );
(Upper_Arc P) \/ (Lower_Arc P) = P by A1, JORDAN6:65;
then h0 /. 2 in P by A640, XBOOLE_0:def 3;
then A649: S₁[ 0 ] by A1, JORDAN6:71;
A650: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A651: ( k + 2 <= len h0 implies LE h0 /. 2,h0 /. (k + 2),P ) ; :: thesis:

now

assume A652: (k + 1) + 2 <= len h0 ; :: thesis:
A653: (k + 1) + 2 = (k + 2) + 1 ;
then A654: k + 2 < len h0 by A652, NAT_1:13;
(k + 1) + 1 = k + 2 ;
then LE h0 /. (k + 2),h0 /. ((k + 2) + 1),P by A455, A653, A654, NAT_1:11;
hence LE h0 /. 2,h0 /. ((k + 1) + 2),P by A1, A651, A652, JORDAN6:73, NAT_1:13; :: thesis:

end;

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

end;

A655: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A649, A650);
(len h0) -' 2 = (len h0) - 2 by A52, A58, XREAL_1:235, XXREAL_0:2;
then ((len h0) -' 2) + 2 = len h0 ;
then ( LE h0 /. 2,h0 /. (len h0),P & h0 /. 2 <> h0 /. (len h0) & h0 /. 2 <> W-min P ) by A61, A62, A636, A647, A655, PARTFUN1:def 8;
hence (Segment (h0 /. (len h0)),(h0 /. 1),P) /\ (Segment (h0 /. 1),(h0 /. 2),P) = {(h0 /. 1)} by A1, A65, Th12; :: thesis:

end;

set i = (len h0) -' 1;
A656: ((len h0) -' 1) + 1 = len h0 by A24, A52, XREAL_1:237, XXREAL_0:2;
A657: 1 <= (len h0) -' 1 by A60, Lm3;
A658: len h0 > (1 + 1) + 1 by A21, A23, A40, A42, A46, A47, A126, XXREAL_0:2;
then A659: (len h0) -' 1 > 1 + 1 by Lm2;
A660: (len h0) -' 1 < len h0 by A53, JORDAN5B:1;
then A661: (len h0) -' 1 in dom h0 by A657, FINSEQ_3:27;
then A662: h0 /. ((len h0) -' 1) = h0 . ((len h0) -' 1) by PARTFUN1:def 8;
A663: ((len h0) -' 1) + 1 <= len h0 by A660, NAT_1:13;
A664: 1 + 1 <= len h0 by A53, NAT_1:13;
A665: LE h0 /. ((len h0) -' 1),h0 /. (((len h0) -' 1) + 1),P by A541, A657, A663;
A666: LE h0 /. 1,h0 /. (1 + 1),P by A541, A664;
1 + 1 in dom h0 by A664, FINSEQ_3:27;
then A667: h0 /. (1 + 1) = h0 . (1 + 1) by PARTFUN1:def 8;
A668: h0 /. 1 <> h0 /. (1 + 1) by A541, A664;
A669: h0 . (1 + 1) = h11 . (1 + 1) by A21, A58, FINSEQ_1:85;
A670: 1 + 1 in dom h1 by A58, FINSEQ_3:27;
then A671: h0 . (1 + 1) = g1 . (h1 . (1 + 1)) by A669, FUNCT_1:23;
A672: h1 . (1 + 1) in rng h1 by A670, FUNCT_1:def 5;
A673: 1 < (len h0) -' 1 by A659, XXREAL_0:2;

A674: now

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

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

then A676: h0 . ((len h0) -' 1) = h11 . ((len h0) -' 1) by A21, A673, FINSEQ_1:85;
A677: (len h0) -' 1 in dom h1 by A673, A675, FINSEQ_3:27;
then A678: h1 . (1 + 1) < h1 . ((len h0) -' 1) by A9, A659, A670, SEQM_3:def 1;
A679: h1 . ((len h0) -' 1) in rng h1 by A677, FUNCT_1:def 5;
A680: h0 . ((len h0) -' 1) = g1 . (h1 . ((len h0) -' 1)) by A676, A677, FUNCT_1:23;
A681: ( 0 <= h1 . ((len h0) -' 1) & h1 . ((len h0) -' 1) <= 1 ) by A9, A679, BORSUK_1:83, XXREAL_1:1;
( 0 <= h1 . (1 + 1) & h1 . (1 + 1) <= 1 ) by A9, A672, BORSUK_1:83, XXREAL_1:1;
then ( h0 /. (1 + 1) in Upper_Arc P & h0 /. ((len h0) -' 1) in Upper_Arc P & LE h0 /. (1 + 1),h0 /. ((len h0) -' 1), Upper_Arc P, W-min P, E-max P ) by A2, A3, A4, A5, A6, A9, A662, A667, A671, A672, A678, A679, A680, A681, Th19, BORSUK_1:83, FUNCT_1:def 5;
hence LE h0 /. (1 + 1),h0 /. ((len h0) -' 1),P by JORDAN6:def 10; :: thesis:

end;

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

then A683: ((len h0) -' 1) - (len h11) = ((len h0) -' 1) -' (len h11) by A21, XREAL_1:235;
A685: ((len h0) -' 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A660, XREAL_1:11;
0 + 1 <= (((((len h0) -' 1) -' (len h11)) + 1) + 1) - 1 by XREAL_1:8;
then A686: ((((len h0) -' 1) -' (len h11)) + 2) -' 1 = ((((len h0) -' 1) -' (len h11)) + 2) - 1 by NAT_D:39;
0 + 2 <= (((len h0) -' 1) -' (len h11)) + 2 by XREAL_1:8;
then A687: 2 -' 1 <= ((((len h0) -' 1) -' (len h11)) + 2) -' 1 by NAT_D:42;
((len h0) -' 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A660, XREAL_1:11;
then (((len h0) -' 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A683, XREAL_1:8;
then ((((len h0) -' 1) -' (len h11)) + 2) -' 1 <= len h21 by A23, NAT_D:44;
then A688: ((((len h0) -' 1) -' (len h11)) + 2) -' 1 in dom h21 by A687, Lm1, FINSEQ_3:27;
1 + 1 in dom h1 by A58, FINSEQ_3:27;
then A689: h11 . (1 + 1) = g1 . (h1 . (1 + 1)) by FUNCT_1:23;
A690: (len h1) + 1 <= (len h0) -' 1 by A682, NAT_1:13;
then A691: h0 . ((len h0) -' 1) = (mid h21,2,((len h21) -' 1)) . (((len h0) -' 1) - (len h11)) by A21, A40, A660, FINSEQ_1:36;
A692: ((len h1) + 1) - (len h1) <= ((len h0) -' 1) - (len h1) by A690, XREAL_1:11;
then A693: 1 <= ((len h0) -' 1) - (len h11) by A20, FINSEQ_3:31;
A694: h0 . ((len h0) -' 1) = h21 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A683, A685, A691, A692, JORDAN3:27;
(((len h0) -' 1) + 1) - 1 <= ((len h1) + ((len h2) - 2)) - 1 by A21, A23, A40, A42, A46, A47, A663, XREAL_1:11;
then ((len h0) -' 1) - (len h11) <= ((len h1) + (((len h2) - 2) - 1)) - (len h11) by XREAL_1:11;
then (((len h0) -' 1) -' (len h11)) + 2 <= (((len h2) - 2) - 1) + 2 by A21, A683, XREAL_1:8;
then A695: ((((len h0) -' 1) -' (len h11)) + 2) - 1 <= ((len h2) - 1) - 1 by XREAL_1:11;
set k = ((((len h0) -' 1) -' (len h11)) + 2) -' 1;
A696: h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) in rng h2 by A22, A688, FUNCT_1:def 5;
A697: h1 . (1 + 1) in rng h1 by A59, FUNCT_1:def 5;
A698: h0 . ((len h0) -' 1) = h21 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) by A43, A45, A683, A685, A691, A693, JORDAN3:27;
A699: ( h0 . ((len h0) -' 1) = g2 . (h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1)) & h21 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) = g2 . (h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1)) ) by A22, A688, A694, FUNCT_1:23;
A700: g1 . (h1 . (1 + 1)) in rng g1 by A6, A9, A697, BORSUK_1:83, FUNCT_1:def 5;
A701: h0 . ((len h0) -' 1) in Lower_Arc P by A13, A15, A16, A696, A699, BORSUK_1:83, FUNCT_1:def 5;
h0 /. ((len h0) -' 1) <> W-min P by A17, A22, A29, A31, A67, A662, A686, A688, A695, A698, FUNCT_1:def 8;
hence LE h0 /. (1 + 1),h0 /. ((len h0) -' 1),P by A4, A662, A667, A669, A689, A700, A701, JORDAN6:def 10; :: thesis:

end;

A702: ( LE h0 /. ((len h0) -' 1),h0 /. (((len h0) -' 1) + 1),P & h0 /. (((len h0) -' 1) + 1) <> W-min P & h0 /. ((len h0) -' 1) <> h0 /. (((len h0) -' 1) + 1) ) by A541, A656, A657;
(len h0) -' 1 <> 1 by A658, Lm2;
then h0 /. ((len h0) -' 1) <> h0 /. 1 by A63, A68, A661, PARTFUN2:17;
hence (Segment (h0 /. ((len h0) -' 1)),(h0 /. (len h0)),P) /\ (Segment (h0 /. (len h0)),(h0 /. 1),P) = {(h0 /. (len h0))} by A1, A65, A656, A702, Th11; :: thesis:

now

assume A703: h0 /. (1 + 1) = h0 /. ((len h0) -' 1) ; :: thesis:
A704: 1 + 1 in dom h1 by A58, FINSEQ_3:27;
then A705: h1 . (1 + 1) in rng h1 by FUNCT_1:def 5;
A706: h0 . (1 + 1) = h11 . (1 + 1) by A21, A58, FINSEQ_1:85;
then h0 . (1 + 1) = g1 . (h1 . (1 + 1)) by A704, FUNCT_1:23;
then A707: h0 . (1 + 1) in Upper_Arc P by A4, A6, A9, A705, BORSUK_1:83, FUNCT_1:def 5;

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

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

then A709: h0 . ((len h0) -' 1) = h11 . ((len h0) -' 1) by A21, A60, Lm3, FINSEQ_1:85;
(len h0) -' 1 in dom h1 by A657, A708, FINSEQ_3:27;
hence contradiction by A20, A66, A659, A662, A667, A703, A704, A706, A709, FUNCT_1:def 8; :: thesis:

end;

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

then A711: (len h1) + 1 <= (len h0) -' 1 by NAT_1:13;
then A712: h0 . ((len h0) -' 1) = (mid h21,2,((len h21) -' 1)) . (((len h0) -' 1) - (len h11)) by A21, A40, A660, FINSEQ_1:36;
A713: ((len h0) -' 1) - (len h11) = ((len h0) -' 1) -' (len h11) by A21, A710, XREAL_1:235;
A714: ((len h0) -' 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A660, XREAL_1:11;
((len h1) + 1) - (len h1) <= ((len h0) -' 1) - (len h1) by A711, XREAL_1:11;
then A715: h0 . ((len h0) -' 1) = h21 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A712, A713, A714, JORDAN3:27;
A716: 0 + 2 <= (((len h0) -' 1) -' (len h11)) + 2 by XREAL_1:8;
then A717: 2 -' 1 <= ((((len h0) -' 1) -' (len h11)) + 2) -' 1 by NAT_D:42;
((len h0) -' 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A660, XREAL_1:11;
then (((len h0) -' 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A713, XREAL_1:8;
then A718: ( 1 <= ((((len h0) -' 1) -' (len h11)) + 2) -' 1 & ((((len h0) -' 1) -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A716, Lm1, NAT_D:42, NAT_D:44;
A719: ((((len h0) -' 1) -' (len h11)) + 2) -' 1 = ((((len h0) -' 1) -' (len h11)) + 2) - 1 by A717, Lm1, NAT_D:39;
set k = ((((len h0) -' 1) -' (len h11)) + 2) -' 1;
((len h0) -' 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A660, XREAL_1:11;
then A720: (((len h0) -' 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A713, XREAL_1:8;
A721: ((((len h0) -' 1) -' (len h11)) + 2) -' 1 < (((((len h0) -' 1) -' (len h11)) + 2) - 1) + 1 by A719, NAT_1:13;
((len h11) + 1) - (len h11) <= ((len h0) -' 1) - (len h11) by A21, A711, XREAL_1:11;
then 1 <= ((len h0) -' 1) -' (len h11) by NAT_D:39;
then 1 + 2 <= (((len h0) -' 1) -' (len h11)) + 2 by XREAL_1:8;
then (1 + 2) - 1 <= ((((len h0) -' 1) -' (len h11)) + 2) - 1 by XREAL_1:11;
then A722: 1 < ((((len h0) -' 1) -' (len h11)) + 2) -' 1 by A719, XXREAL_0:2;
A723: ((((len h0) -' 1) -' (len h11)) + 2) -' 1 in dom h2 by A22, A718, FINSEQ_3:27;
then A724: h0 . ((len h0) -' 1) = g2 . (h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1)) by A715, FUNCT_1:23;
A725: h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) in rng h2 by A723, FUNCT_1:def 5;
(len h0) -' 1 in dom h0 by A657, A660, FINSEQ_3:27;
then A726: h0 /. ((len h0) -' 1) = h0 . ((len h0) -' 1) by PARTFUN1:def 8;
g2 . (h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1)) in rng g2 by A15, A16, A725, BORSUK_1:83, FUNCT_1:def 5;
then h0 . ((len h0) -' 1) in (Upper_Arc P) /\ (Lower_Arc P) by A13, A667, A703, A707, A724, A726, XBOOLE_0:def 4;
then h0 . ((len h0) -' 1) in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
then ( h0 . ((len h0) -' 1) = W-min P or h0 . ((len h0) -' 1) = E-max P ) by TARSKI:def 2;
hence contradiction by A22, A28, A29, A30, A31, A67, A715, A720, A721, A722, A723, FUNCT_1:def 8; :: thesis:

end;

hence Segment (h0 /. ((len h0) -' 1)),(h0 /. (len h0)),P misses Segment (h0 /. 1),(h0 /. 2),P by A1, A656, A665, A666, A668, A674, Th13; :: thesis:
thus for i, j being Element of NAT st 1 <= i & i < j & j < len h0 & not i,j are_adjacent1 holds
Segment (h0 /. i),(h0 /. (i + 1)),P misses Segment (h0 /. j),(h0 /. (j + 1)),P :: thesis:

proof

let i, j be Element of NAT ; :: thesis:
assume that
A727: 1 <= i and
A728: i < j and
A729: j < len h0 and
A730: not i,j are_adjacent1 ; :: thesis:
A731: i < len h0 by A728, A729, XXREAL_0:2;
A732: 1 < j by A727, A728, XXREAL_0:2;
A733: i + 1 <= len h0 by A731, NAT_1:13;
A734: j + 1 <= len h0 by A729, NAT_1:13;
A735: LE h0 /. i,h0 /. (i + 1),P by A541, A727, A733;
A736: LE h0 /. j,h0 /. (j + 1),P by A541, A732, A734;
A737: ( not j = i + 1 & not i = j + 1 ) by A730, GOBRD10:def 1;
A738: i + 1 <= j by A728, NAT_1:13;
then A739: i + 1 < j by A737, XXREAL_0:1;
A740: i + 1 < len h0 by A729, A738, XXREAL_0:2;
A741: h0 /. i <> h0 /. (i + 1) by A541, A727, A733;
A742: 1 < i + 1 by A727, NAT_1:13;
A743: ( 1 <= i + 1 & i + 1 < len h0 ) by A727, A729, A738, NAT_1:13, XXREAL_0:2;
A744: LE h0 /. (i + 1),h0 /. j,P

proof

per cases ;

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

per cases ;

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

A747: h0 . (i + 1) = h11 . (i + 1) by A21, A743, A745, FINSEQ_1:85;
A748: i + 1 in dom h1 by A743, A745, FINSEQ_3:27;
then A749: h1 . (i + 1) in rng h1 by FUNCT_1:def 5;
A750: 1 < j by A739, A743, XXREAL_0:2;
then A751: h0 . j = h11 . j by A21, A746, FINSEQ_1:85;
A752: j in dom h1 by A746, A750, FINSEQ_3:27;
then A753: h1 . j in rng h1 by FUNCT_1:def 5;
i + 1 in dom h0 by A743, FINSEQ_3:27;
then A754: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
j in dom h0 by A729, A750, FINSEQ_3:27;
then h0 /. j = h0 . j by PARTFUN1:def 8;
then ( Upper_Arc P is_an_arc_of W-min P, E-max P & g1 . (h1 . (i + 1)) = h0 /. (i + 1) & 0 <= h1 . (i + 1) & h1 . (i + 1) <= 1 & g1 . (h1 . j) = h0 /. j & 0 <= h1 . j & h1 . j <= 1 & h1 . (i + 1) <= h1 . j ) by A1, A9, A739, A747, A748, A749, A751, A752, A753, A754, BORSUK_1:83, FUNCT_1:23, JORDAN6:def 8, SEQM_3:def 1, XXREAL_1:1;
then ( h0 /. (i + 1) in Upper_Arc P & h0 /. j in Upper_Arc P & LE h0 /. (i + 1),h0 /. j, Upper_Arc P, W-min P, E-max P ) by A3, A4, A5, A6, A9, A749, A753, Th19, BORSUK_1:83, FUNCT_1:def 5;
hence LE h0 /. (i + 1),h0 /. j,P by JORDAN6:def 10; :: thesis:

end;

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

A757: j - (len h11) = j -' (len h11) by A21, A755, XREAL_1:235;
A759: j - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A729, XREAL_1:11;
0 + 1 <= (((j -' (len h11)) + 1) + 1) - 1 by XREAL_1:8;
then A760: ((j -' (len h11)) + 2) -' 1 = ((j -' (len h11)) + 2) - 1 by NAT_D:39;
0 + 2 <= (j -' (len h11)) + 2 by XREAL_1:8;
then A761: 2 -' 1 <= ((j -' (len h11)) + 2) -' 1 by NAT_D:42;
j - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A729, XREAL_1:11;
then (j -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A757, XREAL_1:8;
then A762: ((j -' (len h11)) + 2) -' 1 <= len h21 by A23, NAT_D:44;
then A763: ((j -' (len h11)) + 2) -' 1 in dom h21 by A761, Lm1, FINSEQ_3:27;
i + 1 in Seg (len h1) by A743, A745, FINSEQ_1:3;
then i + 1 in dom h1 by FINSEQ_1:def 3;
then A764: ( j - (len h11) = j -' (len h11) & h0 . (i + 1) = h11 . (i + 1) & ((j -' (len h11)) + 2) -' 1 in dom h21 & ((j -' (len h11)) + 2) -' 1 = ((j -' (len h11)) + 2) - 1 & j - (len h11) <= len (mid h21,2,((len h21) -' 1)) & i + 1 in dom h1 & h11 . (i + 1) = g1 . (h1 . (i + 1)) ) by A21, A742, A745, A755, A759, A761, A762, Lm1, FINSEQ_1:85, FINSEQ_3:27, FUNCT_1:23, NAT_D:39, XREAL_1:235;
A765: (len h1) + 1 <= j by A755, NAT_1:13;
then A766: h0 . j = (mid h21,2,((len h21) -' 1)) . (j - (len h11)) by A21, A40, A729, FINSEQ_1:36;
A767: ((len h1) + 1) - (len h1) <= j - (len h1) by A765, XREAL_1:11;
then A768: h0 . j = h21 . (((j -' (len h11)) + 2) -' 1) by A21, A43, A45, A757, A759, A766, JORDAN3:27;
(j + 1) - 1 <= ((len h1) + ((len h2) - 2)) - 1 by A21, A23, A40, A42, A46, A47, A734, XREAL_1:11;
then j - (len h11) <= ((len h1) + (((len h2) - 2) - 1)) - (len h11) by XREAL_1:11;
then (j -' (len h11)) + 2 <= (((len h2) - 2) - 1) + 2 by A21, A757, XREAL_1:8;
then A769: ((j -' (len h11)) + 2) - 1 <= ((len h2) - 1) - 1 by XREAL_1:11;
A770: ((len h2) - 1) - 1 < len h2 by Lm4;
set k = ((j -' (len h11)) + 2) -' 1;
A771: h2 . (((j -' (len h11)) + 2) -' 1) in rng h2 by A22, A763, FUNCT_1:def 5;
i + 1 in dom h1 by A742, A745, FINSEQ_3:27;
then A772: h1 . (i + 1) in rng h1 by FUNCT_1:def 5;
A773: h0 . j = h21 . (((j -' (len h11)) + 2) -' 1) by A21, A43, A45, A764, A766, A767, JORDAN3:27;
A774: ( h0 . j = g2 . (h2 . (((j -' (len h11)) + 2) -' 1)) & h21 . (((j -' (len h11)) + 2) -' 1) = g2 . (h2 . (((j -' (len h11)) + 2) -' 1)) ) by A22, A763, A768, FUNCT_1:23;
i + 1 in dom h0 by A743, FINSEQ_3:27;
then A775: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
j in dom h0 by A729, A732, FINSEQ_3:27;
then A776: h0 /. j = h0 . j by PARTFUN1:def 8;
A777: g1 . (h1 . (i + 1)) in rng g1 by A6, A9, A772, BORSUK_1:83, FUNCT_1:def 5;
A778: h0 . j in Lower_Arc P by A13, A15, A16, A771, A774, BORSUK_1:83, FUNCT_1:def 5;
h0 /. j <> W-min P by A22, A29, A31, A67, A760, A763, A769, A770, A773, A776, FUNCT_1:def 8;
hence LE h0 /. (i + 1),h0 /. j,P by A4, A764, A775, A776, A777, A778, JORDAN6:def 10; :: thesis:

end;

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

then A780: len h1 < j by A738, XXREAL_0:2;
A781: j - (len h11) = j -' (len h11) by A21, A738, A779, XREAL_1:235, XXREAL_0:2;
A783: j - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A729, XREAL_1:11;
0 + 1 <= (((j -' (len h11)) + 1) + 1) - 1 by XREAL_1:8;
then A784: ((j -' (len h11)) + 2) -' 1 = ((j -' (len h11)) + 2) - 1 by NAT_D:39;
0 + 2 <= (j -' (len h11)) + 2 by XREAL_1:8;
then A785: 2 -' 1 <= ((j -' (len h11)) + 2) -' 1 by NAT_D:42;
j - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A729, XREAL_1:11;
then (j -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A781, XREAL_1:8;
then A786: ((j -' (len h11)) + 2) -' 1 <= len h21 by A23, NAT_D:44;
then A787: ((j -' (len h11)) + 2) -' 1 in dom h21 by A785, Lm1, FINSEQ_3:27;
A788: ( (len h11) + 1 <= i + 1 & i + 1 < (len h11) + (len (mid h21,2,((len h21) -' 1))) ) by A21, A740, A779, FINSEQ_1:35, NAT_1:13;
A789: (i + 1) - (len h11) < ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A740, XREAL_1:11;
(len h1) + 1 <= i + 1 by A779, NAT_1:13;
then ((len h1) + 1) - (len h1) <= (i + 1) - (len h1) by XREAL_1:11;
then A790: ( 1 <= (i + 1) -' (len h11) & (i + 1) -' (len h11) = (i + 1) - (len h11) ) by A21, NAT_D:39;
A791: h0 . (i + 1) = (mid h21,2,((len h21) -' 1)) . ((i + 1) - (len h11)) by A788, FINSEQ_1:36
.= h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A43, A45, A789, A790, JORDAN3:27 ;
then A792: ( j - (len h11) = j -' (len h11) & (i + 1) - (len h11) = (i + 1) -' (len h11) & h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) & ((j -' (len h11)) + 2) -' 1 in dom h21 & (len h11) + 1 <= i + 1 & i + 1 <= (len h11) + (len (mid h21,2,((len h21) -' 1))) & ((j -' (len h11)) + 2) -' 1 = ((j -' (len h11)) + 2) - 1 & j - (len h11) <= len (mid h21,2,((len h21) -' 1)) & (i + 1) - (len h11) < len (mid h21,2,((len h21) -' 1)) ) by A21, A40, A729, A779, A780, A785, A786, A789, Lm1, FINSEQ_3:27, NAT_1:13, NAT_D:39, XREAL_1:11, XREAL_1:235;
len h1 < j by A738, A779, XXREAL_0:2;
then A793: ( (len h11) + 1 <= j & j <= (len h11) + (len (mid h21,2,((len h21) -' 1))) ) by A21, A729, FINSEQ_1:35, NAT_1:13;
then A794: h0 . j = (mid h21,2,((len h21) -' 1)) . (j - (len h11)) by FINSEQ_1:36;
A795: ((len h1) + 1) - (len h1) <= j - (len h1) by A21, A793, XREAL_1:11;
then A796: h0 . j = h21 . (((j -' (len h11)) + 2) -' 1) by A21, A43, A45, A781, A783, A794, JORDAN3:27;
A797: 0 + 2 <= ((i + 1) -' (len h11)) + 2 by XREAL_1:8;
then A798: 2 -' 1 <= (((i + 1) -' (len h11)) + 2) -' 1 by NAT_D:42;
((i + 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A23, A42, A46, A47, A792, XREAL_1:8;
then A799: ( 1 <= (((i + 1) -' (len h11)) + 2) -' 1 & (((i + 1) -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A797, Lm1, NAT_D:42, NAT_D:44;
A800: (((i + 1) -' (len h11)) + 2) -' 1 = (((i + 1) -' (len h11)) + 2) - 1 by A798, Lm1, NAT_D:39;
(j + 1) - 1 <= ((len h1) + ((len h2) - 2)) - 1 by A21, A23, A40, A42, A46, A47, A734, XREAL_1:11;
then j - (len h11) <= ((len h1) + (((len h2) - 2) - 1)) - (len h11) by XREAL_1:11;
then (j -' (len h11)) + 2 <= (((len h2) - 2) - 1) + 2 by A21, A781, XREAL_1:8;
then A801: ((j -' (len h11)) + 2) - 1 <= ((len h2) - 1) - 1 by XREAL_1:11;
A802: ((len h2) - 1) - 1 < len h2 by Lm4;
set k = ((j -' (len h11)) + 2) -' 1;
set j0 = (((i + 1) -' (len h11)) + 2) -' 1;
(i + 1) - (len h11) < j - (len h11) by A739, XREAL_1:11;
then ((i + 1) -' (len h11)) + 2 < (j -' (len h11)) + 2 by A792, XREAL_1:8;
then A803: (((i + 1) -' (len h11)) + 2) -' 1 < ((j -' (len h11)) + 2) -' 1 by A784, A800, XREAL_1:11;
A804: h21 . (((j -' (len h11)) + 2) -' 1) = g2 . (h2 . (((j -' (len h11)) + 2) -' 1)) by A22, A787, FUNCT_1:23;
A805: h2 . (((j -' (len h11)) + 2) -' 1) in rng h2 by A22, A787, FUNCT_1:def 5;
then A806: ( 0 <= h2 . (((j -' (len h11)) + 2) -' 1) & h2 . (((j -' (len h11)) + 2) -' 1) <= 1 ) by A16, BORSUK_1:83, XXREAL_1:1;
A807: (((i + 1) -' (len h11)) + 2) -' 1 in dom h2 by A22, A799, FINSEQ_3:27;
then A808: h0 . (i + 1) = g2 . (h2 . ((((i + 1) -' (len h11)) + 2) -' 1)) by A791, FUNCT_1:23;
A809: h2 . ((((i + 1) -' (len h11)) + 2) -' 1) in rng h2 by A807, FUNCT_1:def 5;
then A810: ( 0 <= h2 . ((((i + 1) -' (len h11)) + 2) -' 1) & h2 . ((((i + 1) -' (len h11)) + 2) -' 1) <= 1 ) by A16, BORSUK_1:83, XXREAL_1:1;
A811: h2 . ((((i + 1) -' (len h11)) + 2) -' 1) < h2 . (((j -' (len h11)) + 2) -' 1) by A16, A22, A787, A803, A807, SEQM_3:def 1;
A812: h0 . j = h21 . (((j -' (len h11)) + 2) -' 1) by A21, A43, A45, A792, A794, A795, JORDAN3:27;
A813: ( h0 . j = g2 . (h2 . (((j -' (len h11)) + 2) -' 1)) & h21 . (((j -' (len h11)) + 2) -' 1) = g2 . (h2 . (((j -' (len h11)) + 2) -' 1)) ) by A22, A787, A796, FUNCT_1:23;
i + 1 in dom h0 by A743, FINSEQ_3:27;
then A814: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
j in dom h0 by A729, A732, FINSEQ_3:27;
then A815: h0 /. j = h0 . j by PARTFUN1:def 8;
A816: g2 . (h2 . ((((i + 1) -' (len h11)) + 2) -' 1)) in rng g2 by A15, A16, A809, BORSUK_1:83, FUNCT_1:def 5;
A817: h0 . j in Lower_Arc P by A13, A15, A16, A805, A813, BORSUK_1:83, FUNCT_1:def 5;
A818: h0 /. j <> W-min P by A22, A29, A31, A67, A784, A787, A801, A802, A812, A815, FUNCT_1:def 8;
LE h0 /. (i + 1),h0 /. j, Lower_Arc P, E-max P, W-min P by A11, A12, A13, A14, A796, A804, A806, A808, A810, A811, A814, A815, Th19;
hence LE h0 /. (i + 1),h0 /. j,P by A13, A808, A814, A815, A816, A817, A818, JORDAN6:def 10; :: thesis:

end;

now

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

per cases ;

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

A821: 1 < i + 1 by A727, NAT_1:13;
then A822: i + 1 in dom h1 by A820, FINSEQ_3:27;
i + 1 in dom h0 by A733, A821, FINSEQ_3:27;
then A823: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
A824: h0 . (i + 1) = h11 . (i + 1) by A21, A820, A821, FINSEQ_1:85;
then A825: h0 . (i + 1) = g1 . (h1 . (i + 1)) by A822, FUNCT_1:23;
h1 . (i + 1) in rng h1 by A822, FUNCT_1:def 5;
then A826: h0 . (i + 1) in Upper_Arc P by A4, A6, A9, A825, BORSUK_1:83, FUNCT_1:def 5;

per cases ;

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

then A828: h0 . j = h11 . j by A21, A732, FINSEQ_1:85;
A829: j in dom h1 by A732, A827, FINSEQ_3:27;
j in dom h0 by A729, A732, FINSEQ_3:27;
then h0 /. j = h0 . j by PARTFUN1:def 8;
hence contradiction by A20, A66, A737, A819, A822, A823, A824, A828, A829, FUNCT_1:def 8; :: thesis:

end;

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

then A831: (len h1) + 1 <= j by NAT_1:13;
A832: ( (len h11) + 1 <= j & j <= (len h11) + (len (mid h21,2,((len h21) -' 1))) ) by A21, A729, A830, FINSEQ_1:35, NAT_1:13;
A833: h0 . j = (mid h21,2,((len h21) -' 1)) . (j - (len h11)) by A21, A40, A729, A831, FINSEQ_1:36;
A834: j - (len h11) = j -' (len h11) by A21, A830, XREAL_1:235;
A835: j - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A832, XREAL_1:11;
((len h1) + 1) - (len h1) <= j - (len h1) by A831, XREAL_1:11;
then A836: h0 . j = h21 . (((j -' (len h11)) + 2) -' 1) by A21, A43, A45, A833, A834, A835, JORDAN3:27;
A837: 0 + 2 <= (j -' (len h11)) + 2 by XREAL_1:8;
then A838: 2 -' 1 <= ((j -' (len h11)) + 2) -' 1 by NAT_D:42;
j - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A729, XREAL_1:11;
then (j -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A834, XREAL_1:8;
then A839: ( 1 <= ((j -' (len h11)) + 2) -' 1 & ((j -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A837, Lm1, NAT_D:42, NAT_D:44;
A840: ((j -' (len h11)) + 2) -' 1 = ((j -' (len h11)) + 2) - 1 by A838, Lm1, NAT_D:39;
set k = ((j -' (len h11)) + 2) -' 1;
j - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A729, XREAL_1:11;
then A841: (j -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A834, XREAL_1:8;
A842: ((j -' (len h11)) + 2) -' 1 < (((j -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
((len h11) + 1) - (len h11) <= j - (len h11) by A21, A831, XREAL_1:11;
then 1 <= j -' (len h11) by NAT_D:39;
then 1 + 2 <= (j -' (len h11)) + 2 by XREAL_1:8;
then (1 + 2) - 1 <= ((j -' (len h11)) + 2) - 1 by XREAL_1:11;
then A843: 1 < ((j -' (len h11)) + 2) -' 1 by A840, XXREAL_0:2;
A844: ((j -' (len h11)) + 2) -' 1 in dom h2 by A22, A839, FINSEQ_3:27;
then A845: h0 . j = g2 . (h2 . (((j -' (len h11)) + 2) -' 1)) by A836, FUNCT_1:23;
A846: h2 . (((j -' (len h11)) + 2) -' 1) in rng h2 by A844, FUNCT_1:def 5;
j in dom h0 by A729, A732, FINSEQ_3:27;
then A847: h0 /. j = h0 . j by PARTFUN1:def 8;
g2 . (h2 . (((j -' (len h11)) + 2) -' 1)) in rng g2 by A15, A16, A846, BORSUK_1:83, FUNCT_1:def 5;
then h0 . j in (Upper_Arc P) /\ (Lower_Arc P) by A13, A819, A823, A826, A845, A847, XBOOLE_0:def 4;
then A848: h0 . j in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
A849: h0 . j <> W-min P by A22, A29, A31, A67, A836, A840, A841, A842, A844, FUNCT_1:def 8;
h0 . j <> E-max P by A22, A28, A30, A67, A836, A843, A844, FUNCT_1:def 8;
hence contradiction by A848, A849, TARSKI:def 2; :: thesis:

end;

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

then A851: (len h1) + 1 <= i + 1 by NAT_1:13;
then A852: h0 . (i + 1) = (mid h21,2,((len h21) -' 1)) . ((i + 1) - (len h11)) by A21, A40, A733, FINSEQ_1:36;
A853: (i + 1) - (len h11) = (i + 1) -' (len h11) by A21, A850, XREAL_1:235;
A854: (i + 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A733, XREAL_1:11;
((len h1) + 1) - (len h1) <= (i + 1) - (len h1) by A851, XREAL_1:11;
then A855: h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A852, A853, A854, JORDAN3:27;
A856: 0 + 2 <= ((i + 1) -' (len h11)) + 2 by XREAL_1:8;
then A857: 2 -' 1 <= (((i + 1) -' (len h11)) + 2) -' 1 by NAT_D:42;
(i + 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A733, XREAL_1:11;
then ((i + 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A853, XREAL_1:8;
then A858: ( 1 <= (((i + 1) -' (len h11)) + 2) -' 1 & (((i + 1) -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A856, Lm1, NAT_D:42, NAT_D:44;
A859: (((i + 1) -' (len h11)) + 2) -' 1 = (((i + 1) -' (len h11)) + 2) - 1 by A857, Lm1, NAT_D:39;
set j0 = (((i + 1) -' (len h11)) + 2) -' 1;
((len h11) + 1) - (len h11) <= (i + 1) - (len h11) by A21, A851, XREAL_1:11;
then A860: (i + 1) -' (len h11) = (i + 1) - (len h11) by NAT_D:39;
A861: (((i + 1) -' (len h11)) + 2) -' 1 in dom h2 by A22, A858, FINSEQ_3:27;
1 <= i + 1 by A727, NAT_1:13;
then i + 1 in dom h0 by A733, FINSEQ_3:27;
then A862: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
A863: j > len h1 by A738, A850, XXREAL_0:2;
then A864: (len h1) + 1 <= j by NAT_1:13;
( (len h11) + 1 <= j & j <= (len h11) + (len (mid h21,2,((len h21) -' 1))) ) by A21, A729, A863, FINSEQ_1:35, NAT_1:13;
then A865: h0 . j = (mid h21,2,((len h21) -' 1)) . (j - (len h11)) by FINSEQ_1:36;
A866: j - (len h11) = j -' (len h11) by A21, A738, A850, XREAL_1:235, XXREAL_0:2;
A867: j - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A729, XREAL_1:11;
((len h1) + 1) - (len h1) <= j - (len h1) by A864, XREAL_1:11;
then A868: h0 . j = h21 . (((j -' (len h11)) + 2) -' 1) by A21, A43, A45, A865, A866, A867, JORDAN3:27;
A869: 0 + 2 <= (j -' (len h11)) + 2 by XREAL_1:8;
then A870: 2 -' 1 <= ((j -' (len h11)) + 2) -' 1 by NAT_D:42;
j - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A729, XREAL_1:11;
then (j -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A866, XREAL_1:8;
then A871: ( 1 <= ((j -' (len h11)) + 2) -' 1 & ((j -' (len h11)) + 2) -' 1 <= len h21 ) by A23, A869, Lm1, NAT_D:42, NAT_D:44;
A872: ((j -' (len h11)) + 2) -' 1 = ((j -' (len h11)) + 2) - 1 by A870, Lm1, NAT_D:39;
set k = ((j -' (len h11)) + 2) -' 1;
((len h11) + 1) - (len h11) <= j - (len h11) by A21, A864, XREAL_1:11;
then j -' (len h11) = j - (len h11) by NAT_D:39;
then (i + 1) -' (len h11) < j -' (len h11) by A739, A860, XREAL_1:11;
then ((i + 1) -' (len h11)) + 2 < (j -' (len h11)) + 2 by XREAL_1:8;
then A873: (((i + 1) -' (len h11)) + 2) -' 1 < ((j -' (len h11)) + 2) -' 1 by A859, A872, XREAL_1:11;
A874: ((j -' (len h11)) + 2) -' 1 in dom h2 by A22, A871, FINSEQ_3:27;
j in dom h0 by A729, A732, FINSEQ_3:27;
then h0 /. j = h0 . j by PARTFUN1:def 8;
hence contradiction by A22, A67, A819, A855, A861, A862, A868, A873, A874, FUNCT_1:def 8; :: thesis:

end;

hence Segment (h0 /. i),(h0 /. (i + 1)),P misses Segment (h0 /. j),(h0 /. (j + 1)),P by A1, A735, A736, A741, A744, Th13; :: thesis:

end;

let i be Element of NAT ; :: thesis:
assume that
A875: 1 < i and
A876: i + 1 < len h0 ; :: thesis:
A877: i < len h0 by A876, NAT_1:13;
A878: LE h0 /. i,h0 /. (i + 1),P by A541, A875, A876;
A879: 1 < i + 1 by A875, NAT_1:13;
A880: h0 /. i <> h0 /. (i + 1) by A541, A875, A876;
A881: i in dom h0 by A875, A877, FINSEQ_3:27;
then h0 /. i = h0 . i by PARTFUN1:def 8;
then A882: h0 /. i <> W-min P by A39, A63, A68, A875, A881, FUNCT_1:def 8;
A883: i + 1 in dom h0 by A876, A879, FINSEQ_3:27;
set k = (((len h0) -' (len h11)) + 2) -' 1;
0 + 2 <= ((len h0) -' (len h11)) + 2 by XREAL_1:8;
then A884: 2 -' 1 <= (((len h0) -' (len h11)) + 2) -' 1 by NAT_D:42;
(((len h0) -' (len h11)) + 2) -' 1 <= len h21 by A40, A42, A46, A47, A57, NAT_D:44;
then A885: (((len h0) -' (len h11)) + 2) -' 1 in dom h21 by A884, Lm1, FINSEQ_3:27;
h0 . (len h0) = (mid h21,2,((len h21) -' 1)) . ((len h0) - (len h11)) by A21, A40, A51, FINSEQ_1:36;
then A886: h0 . (len h0) = h21 . ((((len h0) -' (len h11)) + 2) -' 1) by A21, A40, A43, A45, A56, A57, JORDAN3:27;
A887: h21 . ((((len h0) -' (len h11)) + 2) -' 1) = g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) by A22, A885, FUNCT_1:23;
A888: h2 . ((((len h0) -' (len h11)) + 2) -' 1) in rng h2 by A22, A885, FUNCT_1:def 5;
then A889: h0 . (len h0) in Lower_Arc P by A13, A15, A16, A886, A887, BORSUK_1:83, FUNCT_1:def 5;
A890: LE h0 /. (i + 1),h0 /. (len h0),P

proof

per cases ;

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

then A892: h0 . (i + 1) = h11 . (i + 1) by A21, A879, FINSEQ_1:85;
i + 1 in dom h1 by A879, A891, FINSEQ_3:27;
then A893: h11 . (i + 1) = g1 . (h1 . (i + 1)) by FUNCT_1:23;
i + 1 in dom h1 by A879, A891, FINSEQ_3:27;
then A894: h1 . (i + 1) in rng h1 by FUNCT_1:def 5;
A895: h0 /. (i + 1) = h0 . (i + 1) by A883, PARTFUN1:def 8;
g1 . (h1 . (i + 1)) in rng g1 by A6, A9, A894, BORSUK_1:83, FUNCT_1:def 5;
hence LE h0 /. (i + 1),h0 /. (len h0),P by A4, A55, A125, A889, A892, A893, A895, JORDAN6:def 10; :: thesis:

end;

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

0 + 1 <= ((((len h0) -' (len h11)) + 1) + 1) - 1 by XREAL_1:8;
then A897: (((len h0) -' (len h11)) + 2) -' 1 = (((len h0) -' (len h11)) + 2) - 1 by NAT_D:39;
A898: (((len h0) -' (len h11)) + 2) -' 1 <= len h21 by A40, A42, A46, A47, A57, NAT_D:44;
then A899: (((len h0) -' (len h11)) + 2) -' 1 in dom h21 by A884, Lm1, FINSEQ_3:27;
A900: (len h11) + 1 <= i + 1 by A21, A896, NAT_1:13;
A901: i + 1 < (len h11) + (len (mid h21,2,((len h21) -' 1))) by A876, FINSEQ_1:35;
A902: (i + 1) - (len h11) < ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A40, A876, XREAL_1:11;
(len h1) + 1 <= i + 1 by A896, NAT_1:13;
then A903: ((len h1) + 1) - (len h1) <= (i + 1) - (len h1) by XREAL_1:11;
then A904: (i + 1) -' (len h11) = (i + 1) - (len h11) by A21, NAT_D:39;
A905: h0 . (i + 1) = (mid h21,2,((len h21) -' 1)) . ((i + 1) - (len h11)) by A900, A901, FINSEQ_1:36
.= h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A902, A903, A904, JORDAN3:27 ;
A906: (i + 1) - (len h11) = (i + 1) -' (len h11) by A21, A896, XREAL_1:235;
A907: (((len h0) -' (len h11)) + 2) -' 1 in dom h21 by A884, A898, Lm1, FINSEQ_3:27;
h0 . (len h0) = (mid h21,2,((len h21) -' 1)) . ((len h0) - (len h11)) by A21, A40, A51, FINSEQ_1:36;
then A908: h0 . (len h0) = h21 . ((((len h0) -' (len h11)) + 2) -' 1) by A21, A40, A43, A45, A56, A57, JORDAN3:27;
0 + 2 <= ((i + 1) -' (len h11)) + 2 by XREAL_1:8;
then A909: 2 -' 1 <= (((i + 1) -' (len h11)) + 2) -' 1 by NAT_D:42;
(i + 1) - (len h11) <= ((len h11) + ((len h2) - 2)) - (len h11) by A23, A40, A42, A46, A47, A876, XREAL_1:11;
then ((i + 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A906, XREAL_1:8;
then A910: (((i + 1) -' (len h11)) + 2) -' 1 <= len h21 by A23, NAT_D:44;
A911: (((i + 1) -' (len h11)) + 2) -' 1 = (((i + 1) -' (len h11)) + 2) - 1 by A909, Lm1, NAT_D:39;
set k = (((len h0) -' (len h11)) + 2) -' 1;
set j0 = (((i + 1) -' (len h11)) + 2) -' 1;
(i + 1) - (len h11) < (len h0) - (len h11) by A876, XREAL_1:11;
then ((i + 1) -' (len h11)) + 2 < ((len h0) -' (len h11)) + 2 by A57, A906, XREAL_1:8;
then A912: (((i + 1) -' (len h11)) + 2) -' 1 < (((len h0) -' (len h11)) + 2) -' 1 by A897, A911, XREAL_1:11;
A913: h21 . ((((len h0) -' (len h11)) + 2) -' 1) = g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) by A22, A899, FUNCT_1:23;
h2 . ((((len h0) -' (len h11)) + 2) -' 1) in rng h2 by A22, A907, FUNCT_1:def 5;
then A914: h2 . ((((len h0) -' (len h11)) + 2) -' 1) <= 1 by A16, BORSUK_1:83, XXREAL_1:1;
A915: (((i + 1) -' (len h11)) + 2) -' 1 in dom h2 by A22, A909, A910, Lm1, FINSEQ_3:27;
then A916: h0 . (i + 1) = g2 . (h2 . ((((i + 1) -' (len h11)) + 2) -' 1)) by A905, FUNCT_1:23;
A917: h2 . ((((i + 1) -' (len h11)) + 2) -' 1) in rng h2 by A915, FUNCT_1:def 5;
then A918: 0 <= h2 . ((((i + 1) -' (len h11)) + 2) -' 1) by A16, BORSUK_1:83, XXREAL_1:1;
A919: h2 . ((((i + 1) -' (len h11)) + 2) -' 1) <= 1 by A16, A917, BORSUK_1:83, XXREAL_1:1;
A920: h2 . ((((i + 1) -' (len h11)) + 2) -' 1) < h2 . ((((len h0) -' (len h11)) + 2) -' 1) by A16, A22, A907, A912, A915, SEQM_3:def 1;
A921: h0 /. (i + 1) = h0 . (i + 1) by A883, PARTFUN1:def 8;
g2 . (h2 . ((((i + 1) -' (len h11)) + 2) -' 1)) in rng g2 by A15, A16, A917, BORSUK_1:83, FUNCT_1:def 5;
then A922: h0 . (i + 1) in Lower_Arc P by A13, A905, A915, FUNCT_1:23;
h0 . (len h0) in Lower_Arc P by A13, A15, A16, A886, A887, A888, BORSUK_1:83, FUNCT_1:def 5;
then A923: h0 /. (len h0) in Lower_Arc P by A54, PARTFUN1:def 8;
LE h0 /. (i + 1),h0 /. (len h0), Lower_Arc P, E-max P, W-min P by A11, A12, A13, A14, A55, A908, A913, A914, A916, A918, A919, A920, A921, Th19;
hence LE h0 /. (i + 1),h0 /. (len h0),P by A125, A921, A922, A923, JORDAN6:def 10; :: thesis:

end;

now

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

per cases ;

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

i + 1 in dom h0 by A876, A879, FINSEQ_3:27;
then A926: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
A927: h0 . (i + 1) = h11 . (i + 1) by A21, A879, A925, FINSEQ_1:85;
A928: i + 1 in dom h1 by A879, A925, FINSEQ_3:27;
then A929: h0 . (i + 1) = g1 . (h1 . (i + 1)) by A927, FUNCT_1:23;
h1 . (i + 1) in rng h1 by A928, FUNCT_1:def 5;
then A930: h0 . (i + 1) in Upper_Arc P by A4, A6, A9, A929, BORSUK_1:83, FUNCT_1:def 5;
h0 . (len h0) = (mid h21,2,((len h21) -' 1)) . ((len h0) - (len h11)) by A21, A40, A51, FINSEQ_1:36;
then A931: h0 . (len h0) = h21 . ((((len h0) -' (len h11)) + 2) -' 1) by A21, A40, A43, A45, A56, A57, JORDAN3:27;
0 + 2 <= ((len h0) -' (len h11)) + 2 by XREAL_1:8;
then A932: 2 -' 1 <= (((len h0) -' (len h11)) + 2) -' 1 by NAT_D:42;
A933: (((len h0) -' (len h11)) + 2) -' 1 <= len h21 by A40, A42, A46, A47, A57, NAT_D:44;
A934: (((len h0) -' (len h11)) + 2) -' 1 = (((len h0) -' (len h11)) + 2) - 1 by A932, Lm1, NAT_D:39;
set k = (((len h0) -' (len h11)) + 2) -' 1;
A935: (((len h0) -' (len h11)) + 2) -' 1 < ((((len h0) -' (len h11)) + 2) -' 1) + 1 by NAT_1:13;
1 + 2 <= ((len h0) -' (len h11)) + 2 by A23, A40, A42, A46, A47, A50, A57, XREAL_1:8;
then (1 + 2) - 1 <= (((len h0) -' (len h11)) + 2) - 1 by XREAL_1:11;
then A936: 1 < (((len h0) -' (len h11)) + 2) -' 1 by A934, XXREAL_0:2;
A937: (((len h0) -' (len h11)) + 2) -' 1 in dom h2 by A22, A932, A933, Lm1, FINSEQ_3:27;
then A938: h0 . (len h0) = g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) by A931, FUNCT_1:23;
h2 . ((((len h0) -' (len h11)) + 2) -' 1) in rng h2 by A937, FUNCT_1:def 5;
then g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) in rng g2 by A15, A16, BORSUK_1:83, FUNCT_1:def 5;
then h0 . (len h0) in (Upper_Arc P) /\ (Lower_Arc P) by A13, A55, A924, A926, A930, A938, XBOOLE_0:def 4;
then A939: h0 . (len h0) in {(W-min P),(E-max P)} by A1, JORDAN6:def 9;
A940: h0 . (len h0) <> W-min P by A22, A23, A29, A31, A40, A42, A46, A47, A57, A67, A931, A935, A937, FUNCT_1:def 8;
h0 . (len h0) <> E-max P by A22, A28, A30, A67, A931, A936, A937, FUNCT_1:def 8;
hence contradiction by A939, A940, TARSKI:def 2; :: thesis:

end;

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

then A942: (len h1) + 1 <= i + 1 by NAT_1:13;
A943: i + 1 <= (len h11) + (len (mid h21,2,((len h21) -' 1))) by A876, FINSEQ_1:35;
A944: h0 . (i + 1) = (mid h21,2,((len h21) -' 1)) . ((i + 1) - (len h11)) by A21, A40, A876, A942, FINSEQ_1:36;
A945: (i + 1) - (len h11) = (i + 1) -' (len h11) by A21, A941, XREAL_1:235;
A946: (i + 1) - (len h11) <= ((len h11) + (len (mid h21,2,((len h21) -' 1)))) - (len h11) by A943, XREAL_1:11;
((len h1) + 1) - (len h1) <= (i + 1) - (len h1) by A942, XREAL_1:11;
then A947: h0 . (i + 1) = h21 . ((((i + 1) -' (len h11)) + 2) -' 1) by A21, A43, A45, A944, A945, A946, JORDAN3:27;
0 + 2 <= ((i + 1) -' (len h11)) + 2 by XREAL_1:8;
then A948: 2 -' 1 <= (((i + 1) -' (len h11)) + 2) -' 1 by NAT_D:42;
(i + 1) - (len h11) <= ((len h1) + ((len h2) - 2)) - (len h11) by A21, A23, A40, A42, A46, A47, A876, XREAL_1:11;
then ((i + 1) -' (len h11)) + 2 <= ((len h2) - 2) + 2 by A21, A945, XREAL_1:8;
then A949: (((i + 1) -' (len h11)) + 2) -' 1 <= len h21 by A23, NAT_D:44;
A950: (((i + 1) -' (len h11)) + 2) -' 1 = (((i + 1) -' (len h11)) + 2) - 1 by A948, Lm1, NAT_D:39;
set j0 = (((i + 1) -' (len h11)) + 2) -' 1;
((len h11) + 1) - (len h11) <= (i + 1) - (len h11) by A21, A942, XREAL_1:11;
then A951: (i + 1) -' (len h11) = (i + 1) - (len h11) by NAT_D:39;
A952: (((i + 1) -' (len h11)) + 2) -' 1 in dom h2 by A22, A948, A949, Lm1, FINSEQ_3:27;
1 <= i + 1 by A875, NAT_1:13;
then i + 1 in dom h0 by A876, FINSEQ_3:27;
then A953: h0 /. (i + 1) = h0 . (i + 1) by PARTFUN1:def 8;
h0 . (len h0) = (mid h21,2,((len h21) -' 1)) . ((len h0) - (len h11)) by A21, A40, A51, FINSEQ_1:36;
then A954: h0 . (len h0) = h21 . ((((len h0) -' (len h11)) + 2) -' 1) by A23, A40, A42, A43, A44, A46, A47, A50, A57, JORDAN3:27;
0 + 2 <= ((len h0) -' (len h11)) + 2 by XREAL_1:8;
then A955: 2 -' 1 <= (((len h0) -' (len h11)) + 2) -' 1 by NAT_D:42;
A956: (((len h0) -' (len h11)) + 2) -' 1 <= len h21 by A40, A42, A46, A47, A57, NAT_D:44;
A957: (((len h0) -' (len h11)) + 2) -' 1 = (((len h0) -' (len h11)) + 2) - 1 by A955, Lm1, NAT_D:39;
set k = (((len h0) -' (len h11)) + 2) -' 1;
(len h0) -' (len h11) = (len h0) - (len h11) by A23, A40, A42, A46, A47, A50, NAT_D:39;
then (i + 1) -' (len h11) < (len h0) -' (len h11) by A876, A951, XREAL_1:11;
then ((i + 1) -' (len h11)) + 2 < ((len h0) -' (len h11)) + 2 by XREAL_1:8;
then A958: (((i + 1) -' (len h11)) + 2) -' 1 < (((len h0) -' (len h11)) + 2) -' 1 by A950, A957, XREAL_1:11;
(((len h0) -' (len h11)) + 2) -' 1 in dom h2 by A22, A955, A956, Lm1, FINSEQ_3:27;
hence contradiction by A22, A55, A67, A924, A947, A952, A953, A954, A958, FUNCT_1:def 8; :: thesis:

end;

hence Segment (h0 /. (len h0)),(h0 /. 1),P misses Segment (h0 /. i),(h0 /. (i + 1)),P by A1, A39, A64, A878, A880, A882, A890, Th14; :: thesis: