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;

then A127: p in Upper_Arc C by PRE_TOPC:22;

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, EUCLID:52; :: thesis: verum

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

then
p in Cl (Upper_Arc C)
by A8, GOBOARD6:93;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;

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;

end;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;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

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;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

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;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

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

A100:
Ball (p9,(rr / 4)) c= Ball (p9,rr)
by A84, PCOMPS_1: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;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

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 Cend;

hence
Ball (p9,r) meets Upper_Arc C
; :: thesis: verumper cases
( jj2 <= jj1 or jj1 < jj2 )
;

end;

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)

end;proof

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
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) ;

end;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)end;

hence
x in Ball (p9,r)
; :: thesis: verumper 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;

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)

end;proof

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
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) ;

end;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)end;

hence
x in Ball (p9,r)
; :: thesis: verumper 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;

end;

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

then
p in Cl (Lower_Arc C)
by A8, GOBOARD6:93;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;

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;

end;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;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

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;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

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;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

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

A219:
Ball (p9,(rr / 4)) c= Ball (p9,rr)
by A203, PCOMPS_1:1;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;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

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 Cend;

hence
Ball (p9,r) meets Lower_Arc C
; :: thesis: verumper cases
( jj2 <= jj1 or jj1 < jj2 )
;

end;

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)

end;proof

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
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) ;

end;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)

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

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)

end;proof

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
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) ;

end;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)

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

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, EUCLID:52; :: thesis: verum