let C be Simple_closed_curve; :: thesis:
reconsider w = W-min C as Point of (Euclid 2) by EUCLID:67;
A1: for r being Real st r > 0 holds
ex k being Nat st
for m being Nat st m > k holds
(Upper_Appr C) . m meets Ball (w,r)

proof

let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then r / 2 > 0 ;
then consider k being Nat such that
1 < k and
A2: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) < r / 2 and
A3: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) < r / 2 by GOBRD14:11;
reconsider k = k as Nat ;
take k ; :: thesis:
let m be Nat; :: thesis:
assume A4: m > k ; :: thesis:
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) by A4, Th9;
then A5: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < r / 2 by A2, XXREAL_0:2;
dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) by A4, Th11;
then A6: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < r / 2 by A3, XXREAL_0:2;
A7: 1 + 1 <= len (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) by GOBOARD7:34, XXREAL_0:2;
then A8: (left_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1)) /\ (right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1)) = LSeg ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by GOBOARD5:31;
reconsider p = W-min (L~ (Cage (C,m))) as Point of (Euclid 2) by EUCLID:67;
A9: W-min (L~ (Cage (C,m))) in Upper_Arc (L~ (Cage (C,m))) by JORDAN7:1;
Cage (C,m) is_sequence_on Gauge (C,m) by JORDAN9:def 1;
then A10: Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m))))) is_sequence_on Gauge (C,m) by REVROT_1:34;
W-min (L~ (Cage (C,m))) in rng (Cage (C,m)) by SPRECT_2:43;
then A11: W-min (L~ (Cage (C,m))) = (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 by FINSEQ_6:92;
then (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 = W-min (L~ (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m))))))) by REVROT_1:33;
then consider i, j being Nat such that
A12: [i,j] in Indices (Gauge (C,m)) and
A13: [i,(j + 1)] in Indices (Gauge (C,m)) and
A14: (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 = (Gauge (C,m)) * (i,j) and
A15: (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. (1 + 1) = (Gauge (C,m)) * (i,(j + 1)) by A7, A10, JORDAN1I:21;
A16: 1 <= j by A12, MATRIX_0:32;
i < len (Gauge (C,m)) by A7, A10, A12, A13, A14, A15, JORDAN1I:14;
then A17: i + 1 <= len (Gauge (C,m)) by NAT_1:13;
A18: 1 <= i + 1 by NAT_1:11;
j <= width (Gauge (C,m)) by A12, MATRIX_0:32;
then A19: [(i + 1),j] in Indices (Gauge (C,m)) by A16, A18, A17, MATRIX_0:30;
[(1 + 1),1] in Indices (Gauge (C,m)) by Th7;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ m) by Th5, GOBRD14:10;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) by A12, A19, GOBRD14:10;
then A20: (((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1) < r / 2 by A12, A19, A6, GOBRD14:5;
[1,(1 + 1)] in Indices (Gauge (C,m)) by Th6;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ m) by Th5, GOBRD14:9;
then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) by A12, A13, GOBRD14:9;
then (((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2) < r / 2 by A12, A13, A5, GOBRD14:6;
then A21: ((((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1)) + ((((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2)) < (r / 2) + (r / 2) by A20, XREAL_1:8;
A22: 1 <= i by A12, MATRIX_0:32;
right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) = right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(GoB (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))))) by A7, JORDAN1H:23
.= right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(GoB (Cage (C,m)))) by REVROT_1:28
.= right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(Gauge (C,m))) by JORDAN1H:44 ;
then A23: right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) = cell ((Gauge (C,m)),i,j) by A7, A10, A12, A13, A14, A15, GOBRD13:22;
A24: j + 1 <= width (Gauge (C,m)) by A13, MATRIX_0:32;
(Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 in LSeg ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by A7, TOPREAL1:21;
then A25: W-min (L~ (Cage (C,m))) in right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by A11, A8, XBOOLE_0:def 4;
then A26: ((Gauge (C,m)) * (i,j)) `1 <= (W-min (L~ (Cage (C,m)))) `1 by A23, A22, A16, A24, A17, JORDAN9:17;
A27: W-min C in right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by JORDAN1I:6;
then A28: (W-min C) `1 <= ((Gauge (C,m)) * ((i + 1),j)) `1 by A23, A22, A16, A24, A17, JORDAN9:17;
A29: ((Gauge (C,m)) * (i,j)) `2 <= (W-min (L~ (Cage (C,m)))) `2 by A25, A23, A22, A16, A24, A17, JORDAN9:17;
A30: (W-min (L~ (Cage (C,m)))) `1 <= ((Gauge (C,m)) * ((i + 1),j)) `1 by A25, A23, A22, A16, A24, A17, JORDAN9:17;
A31: (W-min (L~ (Cage (C,m)))) `2 <= ((Gauge (C,m)) * (i,(j + 1))) `2 by A25, A23, A22, A16, A24, A17, JORDAN9:17;
A32: (W-min C) `2 <= ((Gauge (C,m)) * (i,(j + 1))) `2 by A27, A23, A22, A16, A24, A17, JORDAN9:17;
A33: ((Gauge (C,m)) * (i,j)) `2 <= (W-min C) `2 by A27, A23, A22, A16, A24, A17, JORDAN9:17;
((Gauge (C,m)) * (i,j)) `1 <= (W-min C) `1 by A27, A23, A22, A16, A24, A17, JORDAN9:17;
then dist ((W-min C),(W-min (L~ (Cage (C,m))))) <= ((((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1)) + ((((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2)) by A28, A33, A32, A26, A30, A29, A31, TOPREAL6:95;
then dist ((W-min C),(W-min (L~ (Cage (C,m))))) < r by A21, XXREAL_0:2;
then dist (w,p) < r by TOPREAL6:def 1;
then A34: p in Ball (w,r) by METRIC_1:11;
(Upper_Appr C) . m = Upper_Arc (L~ (Cage (C,m))) by JORDAN19:def 1;
hence (Upper_Appr C) . m meets Ball (w,r) by A9, A34, XBOOLE_0:3; :: thesis:

end;

North_Arc C = Lim_inf (Upper_Appr C) by JORDAN19:def 3;
hence W-min C in North_Arc C by A1, KURATO_2:14; :: thesis: