let C be Simple_closed_curve; :: thesis: W-min C in North_Arc C
A1: North_Arc C = Lim_inf (Upper_Appr C) by JORDAN19:def 3;
reconsider w = W-min C as Point of (Euclid 2) by EUCLID:71;
for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball w,r

proof

let r be real number ; :: thesis: ( r > 0 implies ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball w,r )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball w,r
then r / 2 > 0 by XREAL_1:217;
then consider k being Element of 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:21;
take k ; :: thesis: for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball w,r
let m be Element of NAT ; :: thesis: ( m > k implies (Upper_Appr C) . m meets Ball w,r )
assume A4: m > k ; :: thesis: (Upper_Appr C) . m meets Ball w,r
reconsider p = W-min (L~ (Cage C,m)) as Point of (Euclid 2) by EUCLID:71;
A5: (Upper_Appr C) . m = Upper_Arc (L~ (Cage C,m)) by JORDAN19:def 1;
A6: W-min (L~ (Cage C,m)) in Upper_Arc (L~ (Cage C,m)) by JORDAN7:1;
A7: W-min (L~ (Cage C,m)) in rng (Cage C,m) by SPRECT_2:47;
A8: 1 + 1 <= len (Cage C,m) by GOBOARD7:36, XXREAL_0:2;
A9: W-min (L~ (Cage C,m)) = (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))) /. 1 by A7, FINSEQ_6:98;
A10: 1 + 1 <= len (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))) by A8, REVROT_1:14;
then A11: (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 TOPREAL1:27;
(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 A10, GOBOARD5:32;
then A12: W-min (L~ (Cage C,m)) in right_cell (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1 by A9, A11, XBOOLE_0:def 4;
A13: W-min C in right_cell (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1 by JORDAN1I:8;
A14: 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 A10, JORDAN1H:29
.= 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:52 ;
Cage C,m is_sequence_on Gauge C,m by JORDAN9:def 1;
then A15: Rotate (Cage C,m),(W-min (L~ (Cage C,m))) is_sequence_on Gauge C,m by REVROT_1:34;
(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 A9, REVROT_1:33;
then consider i, j being Element of NAT such that
A16: ( [i,j] in Indices (Gauge C,m) & [i,(j + 1)] in Indices (Gauge C,m) ) and
A17: ( (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))) /. 1 = (Gauge C,m) * i,j & (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))) /. (1 + 1) = (Gauge C,m) * i,(j + 1) ) by A10, A15, JORDAN1I:23;
A18: right_cell (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1 = cell (Gauge C,m),i,j by A10, A14, A15, A16, A17, GOBRD13:23;
A19: ( 1 <= i & 1 <= j & j + 1 <= width (Gauge C,m) ) by A16, MATRIX_1:39;
A20: 1 <= i + 1 by NAT_1:11;
A21: j <= width (Gauge C,m) by A16, MATRIX_1:39;
i < len (Gauge C,m) by A10, A15, A16, A17, JORDAN1I:16;
then A22: i + 1 <= len (Gauge C,m) by NAT_1:13;
then A23: [(i + 1),j] in Indices (Gauge C,m) by A19, A20, A21, MATRIX_1:37;
( ((Gauge C,m) * i,j) `1 <= (W-min C) `1 & (W-min C) `1 <= ((Gauge C,m) * (i + 1),j) `1 & ((Gauge C,m) * i,j) `2 <= (W-min C) `2 & (W-min C) `2 <= ((Gauge C,m) * i,(j + 1)) `2 & ((Gauge C,m) * i,j) `1 <= (W-min (L~ (Cage C,m))) `1 & (W-min (L~ (Cage C,m))) `1 <= ((Gauge C,m) * (i + 1),j) `1 & ((Gauge C,m) * i,j) `2 <= (W-min (L~ (Cage C,m))) `2 & (W-min (L~ (Cage C,m))) `2 <= ((Gauge C,m) * i,(j + 1)) `2 ) by A12, A13, A18, A19, A22, JORDAN9:19;
then A24: 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 TOPREAL6:104;
A25: [1,(1 + 1)] in Indices (Gauge C,m) by Th6;
[(1 + 1),1] in Indices (Gauge C,m) by Th7;
then A26: dist ((Gauge C,m) * 1,1),((Gauge C,m) * (1 + 1),1) = ((E-bound C) - (W-bound C)) / (2 |^ m) by Th5, GOBRD14:20;
A27: dist ((Gauge C,m) * 1,1),((Gauge C,m) * 1,(1 + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ m) by A25, Th5, GOBRD14:19;
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 A28: 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 A29: dist ((Gauge C,m) * 1,1),((Gauge C,m) * 2,1) < r / 2 by A3, XXREAL_0:2;
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 A16, A27, GOBRD14:19;
then A30: (((Gauge C,m) * i,(j + 1)) `2 ) - (((Gauge C,m) * i,j) `2 ) < r / 2 by A16, A28, GOBRD14:16;
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 A16, A23, A26, GOBRD14:20;
then (((Gauge C,m) * (i + 1),j) `1 ) - (((Gauge C,m) * i,j) `1 ) < r / 2 by A16, A23, A29, GOBRD14:15;
then ((((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 A30, XREAL_1:10;
then dist (W-min C),(W-min (L~ (Cage C,m))) < r by A24, XXREAL_0:2;
then dist w,p < r by TOPREAL6:def 1;
then p in Ball w,r by METRIC_1:12;
hence (Upper_Appr C) . m meets Ball w,r by A5, A6, XBOOLE_0:3; :: thesis: verum

end;

hence W-min C in North_Arc C by A1, KURATO_2:48; :: thesis: verum