let C be Simple_closed_curve; :: thesis: for p being Point of (TOP-REAL 2) st W-bound C < p `1 & p `1 < E-bound C & p in North_Arc C holds
not p in South_Arc C
let p be Point of (TOP-REAL 2); :: thesis: ( W-bound C < p `1 & p `1 < E-bound C & p in North_Arc C implies not p in South_Arc C )
reconsider p9 = p as Point of (Euclid 2) by EUCLID:22;
assume that
A1: W-bound C < p `1 and
A2: p `1 < E-bound C and
A3: p in North_Arc C and
A4: p in South_Arc C ; :: thesis: contradiction
set s = min (((p `1) - (W-bound C)),((E-bound C) - (p `1)));
A5: W-bound C = (W-bound C) + 0 ;
A6: p `1 = (p `1) + 0 ;
A7: (p `1) - (W-bound C) > 0 by A1, A5, XREAL_1:20;
(E-bound C) - (p `1) > 0 by A2, A6, XREAL_1:20;
then A8: min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) > 0 by A7, XXREAL_0:15;

now :: thesis: for r being Real st 0 < r & r < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) holds
Ball (p9,r) meets Upper_Arc C

let r be Real; :: thesis: ( 0 < r & r < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) implies Ball (p9,r) meets Upper_Arc C )
reconsider rr = r as Real ;
assume that
A9: 0 < r and
A10: r < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) ; :: thesis: Ball (p9,r) meets Upper_Arc C
A11: r / 8 > 0 by A9, XREAL_1:139;
reconsider G = Ball (p9,(r / 8)) as a_neighborhood of p by A9, GOBOARD6:2, XREAL_1:139;
consider k1 being Nat such that
A12: for m being Nat st m > k1 holds
(Upper_Appr C) . m meets G by A3, KURATO_2:def 1;
consider k2 being Nat such that
A13: for m being Nat st m > k2 holds
(Lower_Appr C) . m meets G by A4, KURATO_2:def 1;
reconsider k = max (k1,k2) as Nat by TARSKI:1;
A14: k >= k1 by XXREAL_0:25;
set z9 = max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)));
set z = max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8));
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8) >= 1 by A11, XREAL_1:181, XXREAL_0:25;
then log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))) >= log (2,1) by PRE_FF:10;
then log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))) >= 0 by POWER:51;
then reconsider m9 = [\(log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))))/] as Nat by INT_1:53;
A15: 2 to_power (m9 + 1) > 0 by POWER:34;
set N = 2 to_power (m9 + 1);
log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))) < (m9 + 1) * 1 by INT_1:29;
then log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))) < (m9 + 1) * (log (2,2)) by POWER:52;
then log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))) < log (2,(2 to_power (m9 + 1))) by POWER:55;
then (max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8) < 2 to_power (m9 + 1) by A15, PRE_FF:10;
then ((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)) * (r / 8) < (2 to_power (m9 + 1)) * (r / 8) by A11, XREAL_1:68;
then max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8)) < (2 to_power (m9 + 1)) * (r / 8) by A11, XCMPLX_1:87;
then (max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) < ((2 to_power (m9 + 1)) * (r / 8)) / (2 to_power (m9 + 1)) by A15, XREAL_1:74;
then (max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) < ((r / 8) / (2 to_power (m9 + 1))) * (2 to_power (m9 + 1)) ;
then A16: (max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) < r / 8 by A15, XCMPLX_1:87;
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) >= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A15, XREAL_1:72, XXREAL_0:25;
then A17: (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) < r / 8 by A16, XXREAL_0:2;
reconsider W = max (k,m9) as Nat by TARSKI:1;
set m = W + 1;
A18: len (Gauge (C,(W + 1))) = width (Gauge (C,(W + 1))) by JORDAN8:def 1;
max (k,m9) >= k by XXREAL_0:25;
then max (k,m9) >= k1 by A14, XXREAL_0:2;
then W + 1 > k1 by NAT_1:13;
then (Upper_Appr C) . (W + 1) meets G by A12;
then Upper_Arc (L~ (Cage (C,(W + 1)))) meets G by Def1;
then consider p1 being object such that
A19: p1 in Upper_Arc (L~ (Cage (C,(W + 1)))) and
A20: p1 in G by XBOOLE_0:3;
reconsider p1 = p1 as Point of (TOP-REAL 2) by A19;
reconsider p19 = p1 as Point of (Euclid 2) by EUCLID:22;
set f = Upper_Seq (C,(W + 1));
A21: Upper_Arc (L~ (Cage (C,(W + 1)))) = L~ (Upper_Seq (C,(W + 1))) by JORDAN1G:55;
then consider i1 being Nat such that
A22: 1 <= i1 and
A23: i1 + 1 <= len (Upper_Seq (C,(W + 1))) and
A24: p1 in LSeg (((Upper_Seq (C,(W + 1))) /. i1),((Upper_Seq (C,(W + 1))) /. (i1 + 1))) by A19, SPPOL_2:14;
reconsider c1 = (Upper_Seq (C,(W + 1))) /. i1 as Point of (Euclid 2) by EUCLID:22;
reconsider c2 = (Upper_Seq (C,(W + 1))) /. (i1 + 1) as Point of (Euclid 2) by EUCLID:22;
A25: Upper_Seq (C,(W + 1)) is_sequence_on Gauge (C,(W + 1)) by JORDAN1G:4;
i1 < len (Upper_Seq (C,(W + 1))) by A23, NAT_1:13;
then i1 in Seg (len (Upper_Seq (C,(W + 1)))) by A22, FINSEQ_1:1;
then A26: i1 in dom (Upper_Seq (C,(W + 1))) by FINSEQ_1:def 3;
then consider ii1, jj1 being Nat such that
A27: [ii1,jj1] in Indices (Gauge (C,(W + 1))) and
A28: (Upper_Seq (C,(W + 1))) /. i1 = (Gauge (C,(W + 1))) * (ii1,jj1) by A25, GOBOARD1:def 9;
A29: N-bound C > (S-bound C) + 0 by TOPREAL5:16;
A30: E-bound C > (W-bound C) + 0 by TOPREAL5:17;
A31: (N-bound C) - (S-bound C) > 0 by A29, XREAL_1:20;
A32: (E-bound C) - (W-bound C) > 0 by A30, XREAL_1:20;
A33: 2 |^ (m9 + 1) > 0 by A15, POWER:41;
max (k,m9) >= m9 by XXREAL_0:25;
then W + 1 > m9 by NAT_1:13;
then W + 1 >= m9 + 1 by NAT_1:13;
then A34: 2 |^ (W + 1) >= 2 |^ (m9 + 1) by PREPOWER:93;
then A35: ((N-bound C) - (S-bound C)) / (2 |^ (W + 1)) <= ((N-bound C) - (S-bound C)) / (2 |^ (m9 + 1)) by A31, A33, XREAL_1:118;
A36: ((E-bound C) - (W-bound C)) / (2 |^ (W + 1)) <= ((E-bound C) - (W-bound C)) / (2 |^ (m9 + 1)) by A32, A33, A34, XREAL_1:118;
A37: ((N-bound C) - (S-bound C)) / (2 to_power (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A15, XREAL_1:72, XXREAL_0:25;
A38: ((E-bound C) - (W-bound C)) / (2 to_power (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A15, XREAL_1:72, XXREAL_0:25;
A39: ((N-bound C) - (S-bound C)) / (2 |^ (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A37, POWER:41;
A40: ((E-bound C) - (W-bound C)) / (2 |^ (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A38, POWER:41;
A41: ((N-bound C) - (S-bound C)) / (2 |^ (W + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A35, A39, XXREAL_0:2;
A42: ((E-bound C) - (W-bound C)) / (2 |^ (W + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A36, A40, XXREAL_0:2;
then dist (((Upper_Seq (C,(W + 1))) /. i1),((Upper_Seq (C,(W + 1))) /. (i1 + 1))) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A22, A23, A25, A41, Th6;
then dist (((Upper_Seq (C,(W + 1))) /. i1),((Upper_Seq (C,(W + 1))) /. (i1 + 1))) < r / 8 by A17, XXREAL_0:2;
then dist (c1,c2) < r / 8 by TOPREAL6:def 1;
then A43: |.(((Upper_Seq (C,(W + 1))) /. i1) - ((Upper_Seq (C,(W + 1))) /. (i1 + 1))).| < r / 8 by SPPOL_1:39;
|.(p1 - ((Upper_Seq (C,(W + 1))) /. i1)).| <= |.(((Upper_Seq (C,(W + 1))) /. i1) - ((Upper_Seq (C,(W + 1))) /. (i1 + 1))).| by A24, JGRAPH_1:36;
then A44: |.(p1 - ((Upper_Seq (C,(W + 1))) /. i1)).| < r / 8 by A43, XXREAL_0:2;
dist (p19,p9) < r / 8 by A20, METRIC_1:11;
then |.(p - p1).| < r / 8 by SPPOL_1:39;
then A45: |.(p - p1).| + |.(p1 - ((Upper_Seq (C,(W + 1))) /. i1)).| < (r / (2 * 4)) + (r / (2 * 4)) by A44, XREAL_1:8;
|.(p - ((Upper_Seq (C,(W + 1))) /. i1)).| <= |.(p - p1).| + |.(p1 - ((Upper_Seq (C,(W + 1))) /. i1)).| by TOPRNS_1:34;
then A46: |.(p - ((Upper_Seq (C,(W + 1))) /. i1)).| < r / 4 by A45, XXREAL_0:2;
then A47: dist (p9,c1) < r / 4 by SPPOL_1:39;
then A48: (Upper_Seq (C,(W + 1))) /. i1 in Ball (p9,(r / 4)) by METRIC_1:11;
A49: (Upper_Seq (C,(W + 1))) /. i1 in Upper_Arc (L~ (Cage (C,(W + 1)))) by A21, A26, SPPOL_2:44;
A50: k >= k2 by XXREAL_0:25;
max (k,m9) >= k by XXREAL_0:25;
then max (k,m9) >= k2 by A50, XXREAL_0:2;
then W + 1 > k2 by NAT_1:13;
then (Lower_Appr C) . (W + 1) meets G by A13;
then Lower_Arc (L~ (Cage (C,(W + 1)))) meets G by Def2;
then consider p2 being object such that
A51: p2 in Lower_Arc (L~ (Cage (C,(W + 1)))) and
A52: p2 in G by XBOOLE_0:3;
reconsider p2 = p2 as Point of (TOP-REAL 2) by A51;
reconsider p29 = p2 as Point of (Euclid 2) by EUCLID:22;
set g = Lower_Seq (C,(W + 1));
A53: Lower_Arc (L~ (Cage (C,(W + 1)))) = L~ (Lower_Seq (C,(W + 1))) by JORDAN1G:56;
then consider i2 being Nat such that
A54: 1 <= i2 and
A55: i2 + 1 <= len (Lower_Seq (C,(W + 1))) and
A56: p2 in LSeg (((Lower_Seq (C,(W + 1))) /. i2),((Lower_Seq (C,(W + 1))) /. (i2 + 1))) by A51, SPPOL_2:14;
reconsider d1 = (Lower_Seq (C,(W + 1))) /. i2 as Point of (Euclid 2) by EUCLID:22;
reconsider d2 = (Lower_Seq (C,(W + 1))) /. (i2 + 1) as Point of (Euclid 2) by EUCLID:22;
A57: Lower_Seq (C,(W + 1)) is_sequence_on Gauge (C,(W + 1)) by JORDAN1G:5;
i2 < len (Lower_Seq (C,(W + 1))) by A55, NAT_1:13;
then i2 in Seg (len (Lower_Seq (C,(W + 1)))) by A54, FINSEQ_1:1;
then A58: i2 in dom (Lower_Seq (C,(W + 1))) by FINSEQ_1:def 3;
then consider ii2, jj2 being Nat such that
A59: [ii2,jj2] in Indices (Gauge (C,(W + 1))) and
A60: (Lower_Seq (C,(W + 1))) /. i2 = (Gauge (C,(W + 1))) * (ii2,jj2) by A57, GOBOARD1:def 9;
dist (((Lower_Seq (C,(W + 1))) /. i2),((Lower_Seq (C,(W + 1))) /. (i2 + 1))) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A41, A42, A54, A55, A57, Th6;
then dist (((Lower_Seq (C,(W + 1))) /. i2),((Lower_Seq (C,(W + 1))) /. (i2 + 1))) < r / 8 by A17, XXREAL_0:2;
then dist (d1,d2) < r / 8 by TOPREAL6:def 1;
then A61: |.(((Lower_Seq (C,(W + 1))) /. i2) - ((Lower_Seq (C,(W + 1))) /. (i2 + 1))).| < r / 8 by SPPOL_1:39;
|.(p2 - ((Lower_Seq (C,(W + 1))) /. i2)).| <= |.(((Lower_Seq (C,(W + 1))) /. i2) - ((Lower_Seq (C,(W + 1))) /. (i2 + 1))).| by A56, JGRAPH_1:36;
then A62: |.(p2 - ((Lower_Seq (C,(W + 1))) /. i2)).| < r / 8 by A61, XXREAL_0:2;
dist (p29,p9) < r / 8 by A52, METRIC_1:11;
then |.(p - p2).| < r / 8 by SPPOL_1:39;
then A63: |.(p - p2).| + |.(p2 - ((Lower_Seq (C,(W + 1))) /. i2)).| < (r / (2 * 4)) + (r / (2 * 4)) by A62, XREAL_1:8;
|.(p - ((Lower_Seq (C,(W + 1))) /. i2)).| <= |.(p - p2).| + |.(p2 - ((Lower_Seq (C,(W + 1))) /. i2)).| by TOPRNS_1:34;
then A64: |.(p - ((Lower_Seq (C,(W + 1))) /. i2)).| < r / 4 by A63, XXREAL_0:2;
then A65: dist (p9,d1) < r / 4 by SPPOL_1:39;
then A66: (Lower_Seq (C,(W + 1))) /. i2 in Ball (p9,(r / 4)) by METRIC_1:11;
A67: (Lower_Seq (C,(W + 1))) /. i2 in Lower_Arc (L~ (Cage (C,(W + 1)))) by A53, A58, SPPOL_2:44;
set Gij = (Gauge (C,(W + 1))) * (ii2,jj1);
set Gji = (Gauge (C,(W + 1))) * (ii1,jj2);
reconsider Gij9 = (Gauge (C,(W + 1))) * (ii2,jj1), Gji9 = (Gauge (C,(W + 1))) * (ii1,jj2) as Point of (Euclid 2) by EUCLID:22;
A68: 1 <= ii1 by A27, MATRIX_0:32;
A69: ii1 <= len (Gauge (C,(W + 1))) by A27, MATRIX_0:32;
A70: 1 <= jj1 by A27, MATRIX_0:32;
A71: jj1 <= width (Gauge (C,(W + 1))) by A27, MATRIX_0:32;
A72: 1 <= ii2 by A59, MATRIX_0:32;
A73: ii2 <= len (Gauge (C,(W + 1))) by A59, MATRIX_0:32;
A74: 1 <= jj2 by A59, MATRIX_0:32;
A75: jj2 <= width (Gauge (C,(W + 1))) by A59, MATRIX_0:32;
A76: len (Upper_Seq (C,(W + 1))) >= 3 by JORDAN1E:15;
A77: len (Lower_Seq (C,(W + 1))) >= 3 by JORDAN1E:15;
A78: len (Upper_Seq (C,(W + 1))) >= 1 by A76, XXREAL_0:2;
A79: len (Lower_Seq (C,(W + 1))) >= 1 by A77, XXREAL_0:2;
A80: len (Upper_Seq (C,(W + 1))) in Seg (len (Upper_Seq (C,(W + 1)))) by A78, FINSEQ_1:1;
A81: len (Lower_Seq (C,(W + 1))) in Seg (len (Lower_Seq (C,(W + 1)))) by A79, FINSEQ_1:1;
A82: len (Upper_Seq (C,(W + 1))) in dom (Upper_Seq (C,(W + 1))) by A80, FINSEQ_1:def 3;
A83: len (Lower_Seq (C,(W + 1))) in dom (Lower_Seq (C,(W + 1))) by A81, FINSEQ_1:def 3;
A84: r / 4 < r by A9, XREAL_1:223;
A85: r / 2 < r by A9, XREAL_1:216;
A86: min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) <= (p `1) - (W-bound C) by XXREAL_0:17;
A87: min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) <= (E-bound C) - (p `1) by XXREAL_0:17;

A88: now :: thesis: not 1 >= ii1

assume 1 >= ii1 ; :: thesis: contradiction
then A89: ii1 = 1 by A68, XXREAL_0:1;
dist (p9,c1) < r by A47, A84, XXREAL_0:2;
then dist (p9,c1) < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) by A10, XXREAL_0:2;
then A90: dist (p9,c1) < (p `1) - (W-bound C) by A86, XXREAL_0:2;
A91: (p `1) - (((Upper_Seq (C,(W + 1))) /. i1) `1) <= |.((p `1) - (((Upper_Seq (C,(W + 1))) /. i1) `1)).| by ABSVALUE:4;
|.((p `1) - (((Upper_Seq (C,(W + 1))) /. i1) `1)).| <= |.(p - ((Upper_Seq (C,(W + 1))) /. i1)).| by JGRAPH_1:34;
then (p `1) - (((Upper_Seq (C,(W + 1))) /. i1) `1) <= |.(p - ((Upper_Seq (C,(W + 1))) /. i1)).| by A91, XXREAL_0:2;
then (p `1) - (W-bound (L~ (Cage (C,(W + 1))))) <= |.(p - ((Upper_Seq (C,(W + 1))) /. i1)).| by A18, A28, A70, A71, A89, JORDAN1A:73;
then (p `1) - (W-bound (L~ (Cage (C,(W + 1))))) <= dist (p9,c1) by SPPOL_1:39;
then (p `1) - (W-bound (L~ (Cage (C,(W + 1))))) < (p `1) - (W-bound C) by A90, XXREAL_0:2;
then W-bound (L~ (Cage (C,(W + 1)))) > W-bound C by XREAL_1:13;
hence contradiction by Th11; :: thesis: verum

end;

A92: now :: thesis: not ii1 >= len (Gauge (C,(W + 1)))

assume ii1 >= len (Gauge (C,(W + 1))) ; :: thesis: contradiction
then A93: ii1 = len (Gauge (C,(W + 1))) by A69, XXREAL_0:1;
((Gauge (C,(W + 1))) * ((len (Gauge (C,(W + 1)))),jj1)) `1 = E-bound (L~ (Cage (C,(W + 1)))) by A18, A70, A71, JORDAN1A:71;
then (Upper_Seq (C,(W + 1))) /. i1 = E-max (L~ (Cage (C,(W + 1)))) by A21, A26, A28, A93, JORDAN1J:46, SPPOL_2:44
.= (Upper_Seq (C,(W + 1))) /. (len (Upper_Seq (C,(W + 1)))) by JORDAN1F:7 ;
then i1 = len (Upper_Seq (C,(W + 1))) by A26, A82, PARTFUN2:10;
hence contradiction by A23, NAT_1:13; :: thesis: verum

end;

A94: now :: thesis: not ii2 <= 1

assume ii2 <= 1 ; :: thesis: contradiction
then A95: ii2 = 1 by A72, XXREAL_0:1;
((Gauge (C,(W + 1))) * (1,jj2)) `1 = W-bound (L~ (Cage (C,(W + 1)))) by A18, A74, A75, JORDAN1A:73;
then (Lower_Seq (C,(W + 1))) /. i2 = W-min (L~ (Cage (C,(W + 1)))) by A53, A58, A60, A95, JORDAN1J:47, SPPOL_2:44
.= (Lower_Seq (C,(W + 1))) /. (len (Lower_Seq (C,(W + 1)))) by JORDAN1F:8 ;
then i2 = len (Lower_Seq (C,(W + 1))) by A58, A83, PARTFUN2:10;
hence contradiction by A55, NAT_1:13; :: thesis: verum

end;

A96: now :: thesis: not ii2 >= len (Gauge (C,(W + 1)))

assume ii2 >= len (Gauge (C,(W + 1))) ; :: thesis: contradiction
then A97: ii2 = len (Gauge (C,(W + 1))) by A73, XXREAL_0:1;
dist (p9,d1) < r by A65, A84, XXREAL_0:2;
then dist (p9,d1) < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) by A10, XXREAL_0:2;
then A98: dist (p9,d1) < (E-bound C) - (p `1) by A87, XXREAL_0:2;
A99: (((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1) <= |.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| by ABSVALUE:4;
|.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| <= |.(((Lower_Seq (C,(W + 1))) /. i2) - p).| by JGRAPH_1:34;
then |.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| <= |.(p - ((Lower_Seq (C,(W + 1))) /. i2)).| by TOPRNS_1:27;
then (((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1) <= |.(p - ((Lower_Seq (C,(W + 1))) /. i2)).| by A99, XXREAL_0:2;
then (E-bound (L~ (Cage (C,(W + 1))))) - (p `1) <= |.(p - ((Lower_Seq (C,(W + 1))) /. i2)).| by A18, A60, A74, A75, A97, JORDAN1A:71;
then (E-bound (L~ (Cage (C,(W + 1))))) - (p `1) <= dist (p9,d1) by SPPOL_1:39;
then (E-bound (L~ (Cage (C,(W + 1))))) - (p `1) < (E-bound C) - (p `1) by A98, XXREAL_0:2;
then E-bound (L~ (Cage (C,(W + 1)))) < E-bound C by XREAL_1:13;
hence contradiction by Th9; :: thesis: verum

end;

A100: Ball (p9,(rr / 4)) c= Ball (p9,rr) by A84, PCOMPS_1:1;
A101: ((Gauge (C,(W + 1))) * (ii2,jj1)) `1 = ((Gauge (C,(W + 1))) * (ii2,1)) `1 by A70, A71, A72, A73, GOBOARD5:2
.= ((Lower_Seq (C,(W + 1))) /. i2) `1 by A60, A72, A73, A74, A75, GOBOARD5:2 ;
A102: ((Gauge (C,(W + 1))) * (ii2,jj1)) `2 = ((Gauge (C,(W + 1))) * (1,jj1)) `2 by A70, A71, A72, A73, GOBOARD5:1
.= ((Upper_Seq (C,(W + 1))) /. i1) `2 by A28, A68, A69, A70, A71, GOBOARD5:1 ;
A103: ((Gauge (C,(W + 1))) * (ii1,jj2)) `1 = ((Gauge (C,(W + 1))) * (ii1,1)) `1 by A68, A69, A74, A75, GOBOARD5:2
.= ((Upper_Seq (C,(W + 1))) /. i1) `1 by A28, A68, A69, A70, A71, GOBOARD5:2 ;
A104: ((Gauge (C,(W + 1))) * (ii1,jj2)) `2 = ((Gauge (C,(W + 1))) * (1,jj2)) `2 by A68, A69, A74, A75, GOBOARD5:1
.= ((Lower_Seq (C,(W + 1))) /. i2) `2 by A60, A72, A73, A74, A75, GOBOARD5:1 ;
A105: |.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| <= |.(((Lower_Seq (C,(W + 1))) /. i2) - p).| by JGRAPH_1:34;
A106: |.((((Upper_Seq (C,(W + 1))) /. i1) `2) - (p `2)).| <= |.(((Upper_Seq (C,(W + 1))) /. i1) - p).| by JGRAPH_1:34;
A107: |.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| <= |.(p - ((Lower_Seq (C,(W + 1))) /. i2)).| by A105, TOPRNS_1:27;
A108: |.((((Upper_Seq (C,(W + 1))) /. i1) `2) - (p `2)).| <= |.(p - ((Upper_Seq (C,(W + 1))) /. i1)).| by A106, TOPRNS_1:27;
A109: |.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| <= r / 4 by A64, A107, XXREAL_0:2;
|.((((Upper_Seq (C,(W + 1))) /. i1) `2) - (p `2)).| <= r / 4 by A46, A108, XXREAL_0:2;
then |.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| + |.((((Upper_Seq (C,(W + 1))) /. i1) `2) - (p `2)).| <= (r / (2 * 2)) + (r / (2 * 2)) by A109, XREAL_1:7;
then A110: |.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| + |.((((Upper_Seq (C,(W + 1))) /. i1) `2) - (p `2)).| < r by A85, XXREAL_0:2;
A111: |.((((Upper_Seq (C,(W + 1))) /. i1) `1) - (p `1)).| <= |.(((Upper_Seq (C,(W + 1))) /. i1) - p).| by JGRAPH_1:34;
A112: |.((((Lower_Seq (C,(W + 1))) /. i2) `2) - (p `2)).| <= |.(((Lower_Seq (C,(W + 1))) /. i2) - p).| by JGRAPH_1:34;
A113: |.((((Upper_Seq (C,(W + 1))) /. i1) `1) - (p `1)).| <= |.(p - ((Upper_Seq (C,(W + 1))) /. i1)).| by A111, TOPRNS_1:27;
A114: |.((((Lower_Seq (C,(W + 1))) /. i2) `2) - (p `2)).| <= |.(p - ((Lower_Seq (C,(W + 1))) /. i2)).| by A112, TOPRNS_1:27;
A115: |.((((Upper_Seq (C,(W + 1))) /. i1) `1) - (p `1)).| <= r / 4 by A46, A113, XXREAL_0:2;
|.((((Lower_Seq (C,(W + 1))) /. i2) `2) - (p `2)).| <= r / 4 by A64, A114, XXREAL_0:2;
then |.((((Upper_Seq (C,(W + 1))) /. i1) `1) - (p `1)).| + |.((((Lower_Seq (C,(W + 1))) /. i2) `2) - (p `2)).| <= (r / (2 * 2)) + (r / (2 * 2)) by A115, XREAL_1:7;
then A116: |.((((Upper_Seq (C,(W + 1))) /. i1) `1) - (p `1)).| + |.((((Lower_Seq (C,(W + 1))) /. i2) `2) - (p `2)).| < r by A85, XXREAL_0:2;
|.(((Gauge (C,(W + 1))) * (ii2,jj1)) - p).| <= |.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| + |.((((Upper_Seq (C,(W + 1))) /. i1) `2) - (p `2)).| by A101, A102, JGRAPH_1:32;
then |.(((Gauge (C,(W + 1))) * (ii2,jj1)) - p).| < r by A110, XXREAL_0:2;
then dist (Gij9,p9) < r by SPPOL_1:39;
then A117: (Gauge (C,(W + 1))) * (ii2,jj1) in Ball (p9,r) by METRIC_1:11;
|.(((Gauge (C,(W + 1))) * (ii1,jj2)) - p).| <= |.((((Upper_Seq (C,(W + 1))) /. i1) `1) - (p `1)).| + |.((((Lower_Seq (C,(W + 1))) /. i2) `2) - (p `2)).| by A103, A104, JGRAPH_1:32;
then |.(((Gauge (C,(W + 1))) * (ii1,jj2)) - p).| < r by A116, XXREAL_0:2;
then dist (Gji9,p9) < r by SPPOL_1:39;
then A118: (Gauge (C,(W + 1))) * (ii1,jj2) in Ball (p9,r) by METRIC_1:11;
A119: LSeg (((Lower_Seq (C,(W + 1))) /. i2),((Gauge (C,(W + 1))) * (ii2,jj1))) c= Ball (p9,rr) by A66, A100, A117, TOPREAL3:21;
A120: LSeg (((Gauge (C,(W + 1))) * (ii2,jj1)),((Upper_Seq (C,(W + 1))) /. i1)) c= Ball (p9,rr) by A48, A100, A117, TOPREAL3:21;
A121: LSeg (((Lower_Seq (C,(W + 1))) /. i2),((Gauge (C,(W + 1))) * (ii1,jj2))) c= Ball (p9,rr) by A66, A100, A118, TOPREAL3:21;
A122: LSeg (((Gauge (C,(W + 1))) * (ii1,jj2)),((Upper_Seq (C,(W + 1))) /. i1)) c= Ball (p9,rr) by A48, A100, A118, TOPREAL3:21;

now :: thesis: Ball (p9,r) meets Upper_Arc C

per cases ( jj2 <= jj1 or jj1 < jj2 ) ;

suppose A123: jj2 <= jj1 ; :: thesis: Ball (p9,r) meets Upper_Arc C

(LSeg (((Lower_Seq (C,(W + 1))) /. i2),((Gauge (C,(W + 1))) * (ii2,jj1)))) \/ (LSeg (((Gauge (C,(W + 1))) * (ii2,jj1)),((Upper_Seq (C,(W + 1))) /. i1))) c= Ball (p9,r)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (((Lower_Seq (C,(W + 1))) /. i2),((Gauge (C,(W + 1))) * (ii2,jj1)))) \/ (LSeg (((Gauge (C,(W + 1))) * (ii2,jj1)),((Upper_Seq (C,(W + 1))) /. i1))) or x in Ball (p9,r) )
assume A124: x in (LSeg (((Lower_Seq (C,(W + 1))) /. i2),((Gauge (C,(W + 1))) * (ii2,jj1)))) \/ (LSeg (((Gauge (C,(W + 1))) * (ii2,jj1)),((Upper_Seq (C,(W + 1))) /. i1))) ; :: thesis: x in Ball (p9,r)
then reconsider x9 = x as Point of (TOP-REAL 2) ;

now :: thesis: x9 in Ball (p9,r)

per cases ( x9 in LSeg (((Lower_Seq (C,(W + 1))) /. i2),((Gauge (C,(W + 1))) * (ii2,jj1))) or x9 in LSeg (((Gauge (C,(W + 1))) * (ii2,jj1)),((Upper_Seq (C,(W + 1))) /. i1)) ) by A124, XBOOLE_0:def 3;

suppose x9 in LSeg (((Lower_Seq (C,(W + 1))) /. i2),((Gauge (C,(W + 1))) * (ii2,jj1))) ; :: thesis: x9 in Ball (p9,r)

hence x9 in Ball (p9,r) by A119; :: thesis: verum

end;

suppose x9 in LSeg (((Gauge (C,(W + 1))) * (ii2,jj1)),((Upper_Seq (C,(W + 1))) /. i1)) ; :: thesis: x9 in Ball (p9,r)

hence x9 in Ball (p9,r) by A120; :: thesis: verum

end;

end;

end;

hence x in Ball (p9,r) ; :: thesis: verum

end;

hence Ball (p9,r) meets Upper_Arc C by A28, A49, A60, A67, A71, A74, A88, A92, A94, A96, A123, JORDAN15:48, XBOOLE_1:63; :: thesis: verum

end;

suppose A125: jj1 < jj2 ; :: thesis: Ball (p9,r) meets Upper_Arc C

(LSeg (((Upper_Seq (C,(W + 1))) /. i1),((Gauge (C,(W + 1))) * (ii1,jj2)))) \/ (LSeg (((Gauge (C,(W + 1))) * (ii1,jj2)),((Lower_Seq (C,(W + 1))) /. i2))) c= Ball (p9,r)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (((Upper_Seq (C,(W + 1))) /. i1),((Gauge (C,(W + 1))) * (ii1,jj2)))) \/ (LSeg (((Gauge (C,(W + 1))) * (ii1,jj2)),((Lower_Seq (C,(W + 1))) /. i2))) or x in Ball (p9,r) )
assume A126: x in (LSeg (((Upper_Seq (C,(W + 1))) /. i1),((Gauge (C,(W + 1))) * (ii1,jj2)))) \/ (LSeg (((Gauge (C,(W + 1))) * (ii1,jj2)),((Lower_Seq (C,(W + 1))) /. i2))) ; :: thesis: x in Ball (p9,r)
then reconsider x9 = x as Point of (TOP-REAL 2) ;

now :: thesis: x9 in Ball (p9,r)

per cases ( x9 in LSeg (((Upper_Seq (C,(W + 1))) /. i1),((Gauge (C,(W + 1))) * (ii1,jj2))) or x9 in LSeg (((Gauge (C,(W + 1))) * (ii1,jj2)),((Lower_Seq (C,(W + 1))) /. i2)) ) by A126, XBOOLE_0:def 3;

suppose x9 in LSeg (((Upper_Seq (C,(W + 1))) /. i1),((Gauge (C,(W + 1))) * (ii1,jj2))) ; :: thesis: x9 in Ball (p9,r)

hence x9 in Ball (p9,r) by A122; :: thesis: verum

end;

suppose x9 in LSeg (((Gauge (C,(W + 1))) * (ii1,jj2)),((Lower_Seq (C,(W + 1))) /. i2)) ; :: thesis: x9 in Ball (p9,r)

hence x9 in Ball (p9,r) by A121; :: thesis: verum

end;

end;

end;

hence x in Ball (p9,r) ; :: thesis: verum

end;

hence Ball (p9,r) meets Upper_Arc C by A28, A49, A60, A67, A70, A75, A88, A92, A94, A96, A125, Th25, XBOOLE_1:63; :: thesis: verum

end;

end;

end;

hence Ball (p9,r) meets Upper_Arc C ; :: thesis: verum

end;

then p in Cl (Upper_Arc C) by A8, GOBOARD6:93;
then A127: p in Upper_Arc C by PRE_TOPC:22;

now :: thesis: for r being Real st 0 < r & r < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) holds
Ball (p9,r) meets Lower_Arc C

let r be Real; :: thesis: ( 0 < r & r < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) implies Ball (p9,r) meets Lower_Arc C )
reconsider rr = r as Real ;
assume that
A128: 0 < r and
A129: r < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) ; :: thesis: Ball (p9,r) meets Lower_Arc C
A130: r / 8 > 0 by A128, XREAL_1:139;
reconsider G = Ball (p9,(r / 8)) as a_neighborhood of p by A128, GOBOARD6:2, XREAL_1:139;
consider k1 being Nat such that
A131: for m being Nat st m > k1 holds
(Upper_Appr C) . m meets G by A3, KURATO_2:def 1;
consider k2 being Nat such that
A132: for m being Nat st m > k2 holds
(Lower_Appr C) . m meets G by A4, KURATO_2:def 1;
set k = max (k1,k2);
A133: max (k1,k2) >= k1 by XXREAL_0:25;
set z9 = max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)));
set z = max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8));
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8) >= 1 by A130, XREAL_1:181, XXREAL_0:25;
then log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))) >= log (2,1) by PRE_FF:10;
then log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))) >= 0 by POWER:51;
then reconsider m9 = [\(log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))))/] as Nat by INT_1:53;
A134: 2 to_power (m9 + 1) > 0 by POWER:34;
set N = 2 to_power (m9 + 1);
log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))) < (m9 + 1) * 1 by INT_1:29;
then log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))) < (m9 + 1) * (log (2,2)) by POWER:52;
then log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))) < log (2,(2 to_power (m9 + 1))) by POWER:55;
then (max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8) < 2 to_power (m9 + 1) by A134, PRE_FF:10;
then ((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)) * (r / 8) < (2 to_power (m9 + 1)) * (r / 8) by A130, XREAL_1:68;
then max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8)) < (2 to_power (m9 + 1)) * (r / 8) by A130, XCMPLX_1:87;
then (max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) < ((2 to_power (m9 + 1)) * (r / 8)) / (2 to_power (m9 + 1)) by A134, XREAL_1:74;
then (max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) < ((r / 8) / (2 to_power (m9 + 1))) * (2 to_power (m9 + 1)) ;
then A135: (max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) < r / 8 by A134, XCMPLX_1:87;
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) >= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A134, XREAL_1:72, XXREAL_0:25;
then A136: (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) < r / 8 by A135, XXREAL_0:2;
reconsider W = max ((max (k1,k2)),m9) as Nat by TARSKI:1;
set m = W + 1;
reconsider m = W + 1 as Nat ;
A137: len (Gauge (C,m)) = width (Gauge (C,m)) by JORDAN8:def 1;
max ((max (k1,k2)),m9) >= max (k1,k2) by XXREAL_0:25;
then max ((max (k1,k2)),m9) >= k1 by A133, XXREAL_0:2;
then m > k1 by NAT_1:13;
then (Upper_Appr C) . m meets G by A131;
then Upper_Arc (L~ (Cage (C,m))) meets G by Def1;
then consider p1 being object such that
A138: p1 in Upper_Arc (L~ (Cage (C,m))) and
A139: p1 in G by XBOOLE_0:3;
reconsider p1 = p1 as Point of (TOP-REAL 2) by A138;
reconsider p19 = p1 as Point of (Euclid 2) by EUCLID:22;
set f = Upper_Seq (C,m);
A140: Upper_Arc (L~ (Cage (C,m))) = L~ (Upper_Seq (C,m)) by JORDAN1G:55;
then consider i1 being Nat such that
A141: 1 <= i1 and
A142: i1 + 1 <= len (Upper_Seq (C,m)) and
A143: p1 in LSeg (((Upper_Seq (C,m)) /. i1),((Upper_Seq (C,m)) /. (i1 + 1))) by A138, SPPOL_2:14;
reconsider c1 = (Upper_Seq (C,m)) /. i1 as Point of (Euclid 2) by EUCLID:22;
reconsider c2 = (Upper_Seq (C,m)) /. (i1 + 1) as Point of (Euclid 2) by EUCLID:22;
A144: Upper_Seq (C,m) is_sequence_on Gauge (C,m) by JORDAN1G:4;
i1 < len (Upper_Seq (C,m)) by A142, NAT_1:13;
then i1 in Seg (len (Upper_Seq (C,m))) by A141, FINSEQ_1:1;
then A145: i1 in dom (Upper_Seq (C,m)) by FINSEQ_1:def 3;
then consider ii1, jj1 being Nat such that
A146: [ii1,jj1] in Indices (Gauge (C,m)) and
A147: (Upper_Seq (C,m)) /. i1 = (Gauge (C,m)) * (ii1,jj1) by A144, GOBOARD1:def 9;
A148: N-bound C > (S-bound C) + 0 by TOPREAL5:16;
A149: E-bound C > (W-bound C) + 0 by TOPREAL5:17;
A150: (N-bound C) - (S-bound C) > 0 by A148, XREAL_1:20;
A151: (E-bound C) - (W-bound C) > 0 by A149, XREAL_1:20;
A152: 2 |^ (m9 + 1) > 0 by A134, POWER:41;
max ((max (k1,k2)),m9) >= m9 by XXREAL_0:25;
then m > m9 by NAT_1:13;
then m >= m9 + 1 by NAT_1:13;
then A153: 2 |^ m >= 2 |^ (m9 + 1) by PREPOWER:93;
then A154: ((N-bound C) - (S-bound C)) / (2 |^ m) <= ((N-bound C) - (S-bound C)) / (2 |^ (m9 + 1)) by A150, A152, XREAL_1:118;
A155: ((E-bound C) - (W-bound C)) / (2 |^ m) <= ((E-bound C) - (W-bound C)) / (2 |^ (m9 + 1)) by A151, A152, A153, XREAL_1:118;
A156: ((N-bound C) - (S-bound C)) / (2 to_power (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A134, XREAL_1:72, XXREAL_0:25;
A157: ((E-bound C) - (W-bound C)) / (2 to_power (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A134, XREAL_1:72, XXREAL_0:25;
A158: ((N-bound C) - (S-bound C)) / (2 |^ (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A156, POWER:41;
A159: ((E-bound C) - (W-bound C)) / (2 |^ (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A157, POWER:41;
A160: ((N-bound C) - (S-bound C)) / (2 |^ m) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A154, A158, XXREAL_0:2;
A161: ((E-bound C) - (W-bound C)) / (2 |^ m) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A155, A159, XXREAL_0:2;
then dist (((Upper_Seq (C,m)) /. i1),((Upper_Seq (C,m)) /. (i1 + 1))) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A141, A142, A144, A160, Th6;
then dist (((Upper_Seq (C,m)) /. i1),((Upper_Seq (C,m)) /. (i1 + 1))) < r / 8 by A136, XXREAL_0:2;
then dist (c1,c2) < r / 8 by TOPREAL6:def 1;
then A162: |.(((Upper_Seq (C,m)) /. i1) - ((Upper_Seq (C,m)) /. (i1 + 1))).| < r / 8 by SPPOL_1:39;
|.(p1 - ((Upper_Seq (C,m)) /. i1)).| <= |.(((Upper_Seq (C,m)) /. i1) - ((Upper_Seq (C,m)) /. (i1 + 1))).| by A143, JGRAPH_1:36;
then A163: |.(p1 - ((Upper_Seq (C,m)) /. i1)).| < r / 8 by A162, XXREAL_0:2;
dist (p19,p9) < r / 8 by A139, METRIC_1:11;
then |.(p - p1).| < r / 8 by SPPOL_1:39;
then A164: |.(p - p1).| + |.(p1 - ((Upper_Seq (C,m)) /. i1)).| < (r / (2 * 4)) + (r / (2 * 4)) by A163, XREAL_1:8;
|.(p - ((Upper_Seq (C,m)) /. i1)).| <= |.(p - p1).| + |.(p1 - ((Upper_Seq (C,m)) /. i1)).| by TOPRNS_1:34;
then A165: |.(p - ((Upper_Seq (C,m)) /. i1)).| < r / 4 by A164, XXREAL_0:2;
then A166: dist (p9,c1) < r / 4 by SPPOL_1:39;
then A167: (Upper_Seq (C,m)) /. i1 in Ball (p9,(r / 4)) by METRIC_1:11;
A168: (Upper_Seq (C,m)) /. i1 in Upper_Arc (L~ (Cage (C,m))) by A140, A145, SPPOL_2:44;
A169: max (k1,k2) >= k2 by XXREAL_0:25;
max ((max (k1,k2)),m9) >= max (k1,k2) by XXREAL_0:25;
then max ((max (k1,k2)),m9) >= k2 by A169, XXREAL_0:2;
then m > k2 by NAT_1:13;
then (Lower_Appr C) . m meets G by A132;
then Lower_Arc (L~ (Cage (C,m))) meets G by Def2;
then consider p2 being object such that
A170: p2 in Lower_Arc (L~ (Cage (C,m))) and
A171: p2 in G by XBOOLE_0:3;
reconsider p2 = p2 as Point of (TOP-REAL 2) by A170;
reconsider p29 = p2 as Point of (Euclid 2) by EUCLID:22;
set g = Lower_Seq (C,m);
A172: Lower_Arc (L~ (Cage (C,m))) = L~ (Lower_Seq (C,m)) by JORDAN1G:56;
then consider i2 being Nat such that
A173: 1 <= i2 and
A174: i2 + 1 <= len (Lower_Seq (C,m)) and
A175: p2 in LSeg (((Lower_Seq (C,m)) /. i2),((Lower_Seq (C,m)) /. (i2 + 1))) by A170, SPPOL_2:14;
reconsider d1 = (Lower_Seq (C,m)) /. i2 as Point of (Euclid 2) by EUCLID:22;
reconsider d2 = (Lower_Seq (C,m)) /. (i2 + 1) as Point of (Euclid 2) by EUCLID:22;
A176: Lower_Seq (C,m) is_sequence_on Gauge (C,m) by JORDAN1G:5;
i2 < len (Lower_Seq (C,m)) by A174, NAT_1:13;
then i2 in Seg (len (Lower_Seq (C,m))) by A173, FINSEQ_1:1;
then A177: i2 in dom (Lower_Seq (C,m)) by FINSEQ_1:def 3;
then consider ii2, jj2 being Nat such that
A178: [ii2,jj2] in Indices (Gauge (C,m)) and
A179: (Lower_Seq (C,m)) /. i2 = (Gauge (C,m)) * (ii2,jj2) by A176, GOBOARD1:def 9;
dist (((Lower_Seq (C,m)) /. i2),((Lower_Seq (C,m)) /. (i2 + 1))) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) by A160, A161, A173, A174, A176, Th6;
then dist (((Lower_Seq (C,m)) /. i2),((Lower_Seq (C,m)) /. (i2 + 1))) < r / 8 by A136, XXREAL_0:2;
then dist (d1,d2) < r / 8 by TOPREAL6:def 1;
then A180: |.(((Lower_Seq (C,m)) /. i2) - ((Lower_Seq (C,m)) /. (i2 + 1))).| < r / 8 by SPPOL_1:39;
|.(p2 - ((Lower_Seq (C,m)) /. i2)).| <= |.(((Lower_Seq (C,m)) /. i2) - ((Lower_Seq (C,m)) /. (i2 + 1))).| by A175, JGRAPH_1:36;
then A181: |.(p2 - ((Lower_Seq (C,m)) /. i2)).| < r / 8 by A180, XXREAL_0:2;
dist (p29,p9) < r / 8 by A171, METRIC_1:11;
then |.(p - p2).| < r / 8 by SPPOL_1:39;
then A182: |.(p - p2).| + |.(p2 - ((Lower_Seq (C,m)) /. i2)).| < (r / (2 * 4)) + (r / (2 * 4)) by A181, XREAL_1:8;
|.(p - ((Lower_Seq (C,m)) /. i2)).| <= |.(p - p2).| + |.(p2 - ((Lower_Seq (C,m)) /. i2)).| by TOPRNS_1:34;
then A183: |.(p - ((Lower_Seq (C,m)) /. i2)).| < r / 4 by A182, XXREAL_0:2;
then A184: dist (p9,d1) < r / 4 by SPPOL_1:39;
then A185: (Lower_Seq (C,m)) /. i2 in Ball (p9,(r / 4)) by METRIC_1:11;
A186: (Lower_Seq (C,m)) /. i2 in Lower_Arc (L~ (Cage (C,m))) by A172, A177, SPPOL_2:44;
set Gij = (Gauge (C,m)) * (ii2,jj1);
set Gji = (Gauge (C,m)) * (ii1,jj2);
reconsider Gij9 = (Gauge (C,m)) * (ii2,jj1), Gji9 = (Gauge (C,m)) * (ii1,jj2) as Point of (Euclid 2) by EUCLID:22;
A187: 1 <= ii1 by A146, MATRIX_0:32;
A188: ii1 <= len (Gauge (C,m)) by A146, MATRIX_0:32;
A189: 1 <= jj1 by A146, MATRIX_0:32;
A190: jj1 <= width (Gauge (C,m)) by A146, MATRIX_0:32;
A191: 1 <= ii2 by A178, MATRIX_0:32;
A192: ii2 <= len (Gauge (C,m)) by A178, MATRIX_0:32;
A193: 1 <= jj2 by A178, MATRIX_0:32;
A194: jj2 <= width (Gauge (C,m)) by A178, MATRIX_0:32;
A195: len (Upper_Seq (C,m)) >= 3 by JORDAN1E:15;
A196: len (Lower_Seq (C,m)) >= 3 by JORDAN1E:15;
A197: len (Upper_Seq (C,m)) >= 1 by A195, XXREAL_0:2;
A198: len (Lower_Seq (C,m)) >= 1 by A196, XXREAL_0:2;
A199: len (Upper_Seq (C,m)) in Seg (len (Upper_Seq (C,m))) by A197, FINSEQ_1:1;
A200: len (Lower_Seq (C,m)) in Seg (len (Lower_Seq (C,m))) by A198, FINSEQ_1:1;
A201: len (Upper_Seq (C,m)) in dom (Upper_Seq (C,m)) by A199, FINSEQ_1:def 3;
A202: len (Lower_Seq (C,m)) in dom (Lower_Seq (C,m)) by A200, FINSEQ_1:def 3;
A203: r / 4 < r by A128, XREAL_1:223;
A204: r / 2 < r by A128, XREAL_1:216;
A205: min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) <= (p `1) - (W-bound C) by XXREAL_0:17;
A206: min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) <= (E-bound C) - (p `1) by XXREAL_0:17;

A207: now :: thesis: not 1 >= ii1

assume 1 >= ii1 ; :: thesis: contradiction
then A208: ii1 = 1 by A187, XXREAL_0:1;
dist (p9,c1) < r by A166, A203, XXREAL_0:2;
then dist (p9,c1) < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) by A129, XXREAL_0:2;
then A209: dist (p9,c1) < (p `1) - (W-bound C) by A205, XXREAL_0:2;
A210: (p `1) - (((Upper_Seq (C,m)) /. i1) `1) <= |.((p `1) - (((Upper_Seq (C,m)) /. i1) `1)).| by ABSVALUE:4;
|.((p `1) - (((Upper_Seq (C,m)) /. i1) `1)).| <= |.(p - ((Upper_Seq (C,m)) /. i1)).| by JGRAPH_1:34;
then (p `1) - (((Upper_Seq (C,m)) /. i1) `1) <= |.(p - ((Upper_Seq (C,m)) /. i1)).| by A210, XXREAL_0:2;
then (p `1) - (W-bound (L~ (Cage (C,m)))) <= |.(p - ((Upper_Seq (C,m)) /. i1)).| by A137, A147, A189, A190, A208, JORDAN1A:73;
then (p `1) - (W-bound (L~ (Cage (C,m)))) <= dist (p9,c1) by SPPOL_1:39;
then (p `1) - (W-bound (L~ (Cage (C,m)))) < (p `1) - (W-bound C) by A209, XXREAL_0:2;
then W-bound (L~ (Cage (C,m))) > W-bound C by XREAL_1:13;
hence contradiction by Th11; :: thesis: verum

end;

A211: now :: thesis: not ii1 >= len (Gauge (C,m))

assume ii1 >= len (Gauge (C,m)) ; :: thesis: contradiction
then A212: ii1 = len (Gauge (C,m)) by A188, XXREAL_0:1;
((Gauge (C,m)) * ((len (Gauge (C,m))),jj1)) `1 = E-bound (L~ (Cage (C,m))) by A137, A189, A190, JORDAN1A:71;
then (Upper_Seq (C,m)) /. i1 = E-max (L~ (Cage (C,m))) by A140, A145, A147, A212, JORDAN1J:46, SPPOL_2:44
.= (Upper_Seq (C,m)) /. (len (Upper_Seq (C,m))) by JORDAN1F:7 ;
then i1 = len (Upper_Seq (C,m)) by A145, A201, PARTFUN2:10;
hence contradiction by A142, NAT_1:13; :: thesis: verum

end;

A213: now :: thesis: not ii2 <= 1

assume ii2 <= 1 ; :: thesis: contradiction
then A214: ii2 = 1 by A191, XXREAL_0:1;
((Gauge (C,m)) * (1,jj2)) `1 = W-bound (L~ (Cage (C,m))) by A137, A193, A194, JORDAN1A:73;
then (Lower_Seq (C,m)) /. i2 = W-min (L~ (Cage (C,m))) by A172, A177, A179, A214, JORDAN1J:47, SPPOL_2:44
.= (Lower_Seq (C,m)) /. (len (Lower_Seq (C,m))) by JORDAN1F:8 ;
then i2 = len (Lower_Seq (C,m)) by A177, A202, PARTFUN2:10;
hence contradiction by A174, NAT_1:13; :: thesis: verum

end;

A215: now :: thesis: not ii2 >= len (Gauge (C,m))

assume ii2 >= len (Gauge (C,m)) ; :: thesis: contradiction
then A216: ii2 = len (Gauge (C,m)) by A192, XXREAL_0:1;
dist (p9,d1) < r by A184, A203, XXREAL_0:2;
then dist (p9,d1) < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) by A129, XXREAL_0:2;
then A217: dist (p9,d1) < (E-bound C) - (p `1) by A206, XXREAL_0:2;
A218: (((Lower_Seq (C,m)) /. i2) `1) - (p `1) <= |.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| by ABSVALUE:4;
|.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| <= |.(((Lower_Seq (C,m)) /. i2) - p).| by JGRAPH_1:34;
then |.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| <= |.(p - ((Lower_Seq (C,m)) /. i2)).| by TOPRNS_1:27;
then (((Lower_Seq (C,m)) /. i2) `1) - (p `1) <= |.(p - ((Lower_Seq (C,m)) /. i2)).| by A218, XXREAL_0:2;
then (E-bound (L~ (Cage (C,m)))) - (p `1) <= |.(p - ((Lower_Seq (C,m)) /. i2)).| by A137, A179, A193, A194, A216, JORDAN1A:71;
then (E-bound (L~ (Cage (C,m)))) - (p `1) <= dist (p9,d1) by SPPOL_1:39;
then (E-bound (L~ (Cage (C,m)))) - (p `1) < (E-bound C) - (p `1) by A217, XXREAL_0:2;
then E-bound (L~ (Cage (C,m))) < E-bound C by XREAL_1:13;
hence contradiction by Th9; :: thesis: verum

end;

A219: Ball (p9,(rr / 4)) c= Ball (p9,rr) by A203, PCOMPS_1:1;
A220: ((Gauge (C,m)) * (ii2,jj1)) `1 = ((Gauge (C,m)) * (ii2,1)) `1 by A189, A190, A191, A192, GOBOARD5:2
.= ((Lower_Seq (C,m)) /. i2) `1 by A179, A191, A192, A193, A194, GOBOARD5:2 ;
A221: ((Gauge (C,m)) * (ii2,jj1)) `2 = ((Gauge (C,m)) * (1,jj1)) `2 by A189, A190, A191, A192, GOBOARD5:1
.= ((Upper_Seq (C,m)) /. i1) `2 by A147, A187, A188, A189, A190, GOBOARD5:1 ;
A222: ((Gauge (C,m)) * (ii1,jj2)) `1 = ((Gauge (C,m)) * (ii1,1)) `1 by A187, A188, A193, A194, GOBOARD5:2
.= ((Upper_Seq (C,m)) /. i1) `1 by A147, A187, A188, A189, A190, GOBOARD5:2 ;
A223: ((Gauge (C,m)) * (ii1,jj2)) `2 = ((Gauge (C,m)) * (1,jj2)) `2 by A187, A188, A193, A194, GOBOARD5:1
.= ((Lower_Seq (C,m)) /. i2) `2 by A179, A191, A192, A193, A194, GOBOARD5:1 ;
A224: |.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| <= |.(((Lower_Seq (C,m)) /. i2) - p).| by JGRAPH_1:34;
A225: |.((((Upper_Seq (C,m)) /. i1) `2) - (p `2)).| <= |.(((Upper_Seq (C,m)) /. i1) - p).| by JGRAPH_1:34;
A226: |.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| <= |.(p - ((Lower_Seq (C,m)) /. i2)).| by A224, TOPRNS_1:27;
A227: |.((((Upper_Seq (C,m)) /. i1) `2) - (p `2)).| <= |.(p - ((Upper_Seq (C,m)) /. i1)).| by A225, TOPRNS_1:27;
A228: |.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| <= r / 4 by A183, A226, XXREAL_0:2;
|.((((Upper_Seq (C,m)) /. i1) `2) - (p `2)).| <= r / 4 by A165, A227, XXREAL_0:2;
then |.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| + |.((((Upper_Seq (C,m)) /. i1) `2) - (p `2)).| <= (r / (2 * 2)) + (r / (2 * 2)) by A228, XREAL_1:7;
then A229: |.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| + |.((((Upper_Seq (C,m)) /. i1) `2) - (p `2)).| < r by A204, XXREAL_0:2;
A230: |.((((Upper_Seq (C,m)) /. i1) `1) - (p `1)).| <= |.(((Upper_Seq (C,m)) /. i1) - p).| by JGRAPH_1:34;
A231: |.((((Lower_Seq (C,m)) /. i2) `2) - (p `2)).| <= |.(((Lower_Seq (C,m)) /. i2) - p).| by JGRAPH_1:34;
A232: |.((((Upper_Seq (C,m)) /. i1) `1) - (p `1)).| <= |.(p - ((Upper_Seq (C,m)) /. i1)).| by A230, TOPRNS_1:27;
A233: |.((((Lower_Seq (C,m)) /. i2) `2) - (p `2)).| <= |.(p - ((Lower_Seq (C,m)) /. i2)).| by A231, TOPRNS_1:27;
A234: |.((((Upper_Seq (C,m)) /. i1) `1) - (p `1)).| <= r / 4 by A165, A232, XXREAL_0:2;
|.((((Lower_Seq (C,m)) /. i2) `2) - (p `2)).| <= r / 4 by A183, A233, XXREAL_0:2;
then |.((((Upper_Seq (C,m)) /. i1) `1) - (p `1)).| + |.((((Lower_Seq (C,m)) /. i2) `2) - (p `2)).| <= (r / (2 * 2)) + (r / (2 * 2)) by A234, XREAL_1:7;
then A235: |.((((Upper_Seq (C,m)) /. i1) `1) - (p `1)).| + |.((((Lower_Seq (C,m)) /. i2) `2) - (p `2)).| < r by A204, XXREAL_0:2;
|.(((Gauge (C,m)) * (ii2,jj1)) - p).| <= |.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| + |.((((Upper_Seq (C,m)) /. i1) `2) - (p `2)).| by A220, A221, JGRAPH_1:32;
then |.(((Gauge (C,m)) * (ii2,jj1)) - p).| < r by A229, XXREAL_0:2;
then dist (Gij9,p9) < r by SPPOL_1:39;
then A236: (Gauge (C,m)) * (ii2,jj1) in Ball (p9,r) by METRIC_1:11;
|.(((Gauge (C,m)) * (ii1,jj2)) - p).| <= |.((((Upper_Seq (C,m)) /. i1) `1) - (p `1)).| + |.((((Lower_Seq (C,m)) /. i2) `2) - (p `2)).| by A222, A223, JGRAPH_1:32;
then |.(((Gauge (C,m)) * (ii1,jj2)) - p).| < r by A235, XXREAL_0:2;
then dist (Gji9,p9) < r by SPPOL_1:39;
then A237: (Gauge (C,m)) * (ii1,jj2) in Ball (p9,r) by METRIC_1:11;
A238: LSeg (((Lower_Seq (C,m)) /. i2),((Gauge (C,m)) * (ii2,jj1))) c= Ball (p9,rr) by A185, A219, A236, TOPREAL3:21;
A239: LSeg (((Gauge (C,m)) * (ii2,jj1)),((Upper_Seq (C,m)) /. i1)) c= Ball (p9,rr) by A167, A219, A236, TOPREAL3:21;
A240: LSeg (((Lower_Seq (C,m)) /. i2),((Gauge (C,m)) * (ii1,jj2))) c= Ball (p9,rr) by A185, A219, A237, TOPREAL3:21;
A241: LSeg (((Gauge (C,m)) * (ii1,jj2)),((Upper_Seq (C,m)) /. i1)) c= Ball (p9,rr) by A167, A219, A237, TOPREAL3:21;

now :: thesis: Ball (p9,r) meets Lower_Arc C

per cases ( jj2 <= jj1 or jj1 < jj2 ) ;

suppose A242: jj2 <= jj1 ; :: thesis: Ball (p9,r) meets Lower_Arc C

(LSeg (((Lower_Seq (C,m)) /. i2),((Gauge (C,m)) * (ii2,jj1)))) \/ (LSeg (((Gauge (C,m)) * (ii2,jj1)),((Upper_Seq (C,m)) /. i1))) c= Ball (p9,r)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (((Lower_Seq (C,m)) /. i2),((Gauge (C,m)) * (ii2,jj1)))) \/ (LSeg (((Gauge (C,m)) * (ii2,jj1)),((Upper_Seq (C,m)) /. i1))) or x in Ball (p9,r) )
assume A243: x in (LSeg (((Lower_Seq (C,m)) /. i2),((Gauge (C,m)) * (ii2,jj1)))) \/ (LSeg (((Gauge (C,m)) * (ii2,jj1)),((Upper_Seq (C,m)) /. i1))) ; :: thesis: x in Ball (p9,r)
then reconsider x9 = x as Point of (TOP-REAL 2) ;

now :: thesis: x9 in Ball (p9,r)

per cases ( x9 in LSeg (((Lower_Seq (C,m)) /. i2),((Gauge (C,m)) * (ii2,jj1))) or x9 in LSeg (((Gauge (C,m)) * (ii2,jj1)),((Upper_Seq (C,m)) /. i1)) ) by A243, XBOOLE_0:def 3;

suppose x9 in LSeg (((Lower_Seq (C,m)) /. i2),((Gauge (C,m)) * (ii2,jj1))) ; :: thesis: x9 in Ball (p9,r)

hence x9 in Ball (p9,r) by A238; :: thesis: verum

end;

suppose x9 in LSeg (((Gauge (C,m)) * (ii2,jj1)),((Upper_Seq (C,m)) /. i1)) ; :: thesis: x9 in Ball (p9,r)

hence x9 in Ball (p9,r) by A239; :: thesis: verum

end;

end;

end;

hence x in Ball (p9,r) ; :: thesis: verum

end;

hence Ball (p9,r) meets Lower_Arc C by A147, A168, A179, A186, A190, A193, A207, A211, A213, A215, A242, JORDAN15:49, XBOOLE_1:63; :: thesis: verum

end;

suppose A244: jj1 < jj2 ; :: thesis: Ball (p9,r) meets Lower_Arc C

(LSeg (((Upper_Seq (C,m)) /. i1),((Gauge (C,m)) * (ii1,jj2)))) \/ (LSeg (((Gauge (C,m)) * (ii1,jj2)),((Lower_Seq (C,m)) /. i2))) c= Ball (p9,r)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (((Upper_Seq (C,m)) /. i1),((Gauge (C,m)) * (ii1,jj2)))) \/ (LSeg (((Gauge (C,m)) * (ii1,jj2)),((Lower_Seq (C,m)) /. i2))) or x in Ball (p9,r) )
assume A245: x in (LSeg (((Upper_Seq (C,m)) /. i1),((Gauge (C,m)) * (ii1,jj2)))) \/ (LSeg (((Gauge (C,m)) * (ii1,jj2)),((Lower_Seq (C,m)) /. i2))) ; :: thesis: x in Ball (p9,r)
then reconsider x9 = x as Point of (TOP-REAL 2) ;

now :: thesis: x9 in Ball (p9,r)

per cases ( x9 in LSeg (((Upper_Seq (C,m)) /. i1),((Gauge (C,m)) * (ii1,jj2))) or x9 in LSeg (((Gauge (C,m)) * (ii1,jj2)),((Lower_Seq (C,m)) /. i2)) ) by A245, XBOOLE_0:def 3;

suppose x9 in LSeg (((Upper_Seq (C,m)) /. i1),((Gauge (C,m)) * (ii1,jj2))) ; :: thesis: x9 in Ball (p9,r)

hence x9 in Ball (p9,r) by A241; :: thesis: verum

end;

suppose x9 in LSeg (((Gauge (C,m)) * (ii1,jj2)),((Lower_Seq (C,m)) /. i2)) ; :: thesis: x9 in Ball (p9,r)

hence x9 in Ball (p9,r) by A240; :: thesis: verum

end;

end;

end;

hence x in Ball (p9,r) ; :: thesis: verum

end;

hence Ball (p9,r) meets Lower_Arc C by A147, A168, A179, A186, A189, A194, A207, A211, A213, A215, A244, Th24, XBOOLE_1:63; :: thesis: verum

end;

end;

end;

hence Ball (p9,r) meets Lower_Arc C ; :: thesis: verum

end;

then p in Cl (Lower_Arc C) by A8, GOBOARD6:93;
then p in Lower_Arc C by PRE_TOPC:22;
then p in (Upper_Arc C) /\ (Lower_Arc C) by A127, XBOOLE_0:def 4;
then p in {(W-min C),(E-max C)} by JORDAN6:50;
then ( p = W-min C or p = E-max C ) by TARSKI:def 2;
hence contradiction by A1, A2; :: thesis: verum