let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for m being Nat st m > k holds
(Upper_Appr C) . m meets Ball (w,r) )
assume r > 0 ; :: thesis: ex k being Nat st
for m being Nat st m > k holds
(Upper_Appr C) . m meets Ball (w,r)
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: for m being Nat st m > k holds
(Upper_Appr C) . m meets Ball (w,r)
let m be 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)
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;
reconsider p = E-max (L~ (Cage (C,m))) as Point of (Euclid 2) by EUCLID:67;
A7: E-max (L~ (Cage (C,m))) in Upper_Arc (L~ (Cage (C,m))) by JORDAN7:1;
A8: 1 + 1 <= len (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) by GOBOARD7:34, XXREAL_0:2;
then A9: (left_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1)) /\ (right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1)) = LSeg ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by GOBOARD5:31;
Cage (C,m) is_sequence_on Gauge (C,m) by JORDAN9:def 1;
then A10: Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m))))) is_sequence_on Gauge (C,m) by REVROT_1:34;
E-max (L~ (Cage (C,m))) in rng (Cage (C,m)) by SPRECT_2:46;
then A11: E-max (L~ (Cage (C,m))) = (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 by FINSEQ_6:92;
then (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 = E-max (L~ (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m))))))) by REVROT_1:33;
then consider i, j being Nat such that
A12: [i,(j + 1)] in Indices (Gauge (C,m)) and
A13: [i,j] in Indices (Gauge (C,m)) and
A14: (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 = (Gauge (C,m)) * (i,(j + 1)) and
A15: (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. (1 + 1) = (Gauge (C,m)) * (i,j) by A8, A10, JORDAN1I:23;
A16: i <= len (Gauge (C,m)) by A12, MATRIX_0:32;
i > 1 by A8, A10, A12, A13, A14, A15, JORDAN1I:16;
then A17: i - 1 > 1 - 1 by XREAL_1:14;
then A18: i -' 1 = i - 1 by XREAL_0:def 2;
then A19: i -' 1 <= len (Gauge (C,m)) by A16, XREAL_1:146, XXREAL_0:2;
i - 1 in NAT by A17, INT_1:3;
then A20: i - 1 >= 0 + 1 by A17, NAT_1:13;
then A21: (i -' 1) + 1 = i by NAT_D:43;
right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) = right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(GoB (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))))) by A8, JORDAN1H:23
.= right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(GoB (Cage (C,m)))) by REVROT_1:28
.= right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(Gauge (C,m))) by JORDAN1H:44 ;
then A22: right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) = cell ((Gauge (C,m)),(i -' 1),j) by A8, A10, A12, A13, A14, A15, GOBRD13:28;
A23: j + 1 <= width (Gauge (C,m)) by A12, MATRIX_0:32;
1 <= j + 1 by NAT_1:11;
then A24: [(i -' 1),(j + 1)] in Indices (Gauge (C,m)) by A23, A20, A18, A19, MATRIX_0:30;
A25: 1 <= j by A13, MATRIX_0:32;
j <= width (Gauge (C,m)) by A13, MATRIX_0:32;
then A26: [(i -' 1),j] in Indices (Gauge (C,m)) by A25, A20, A18, A19, MATRIX_0:30;
[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 -' 1),j)),((Gauge (C,m)) * ((i -' 1),(j + 1)))) by A26, A24, GOBRD14:9;
then A27: (((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2) < r / 2 by A26, A24, A5, GOBRD14:6;
[(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 -' 1),j)),((Gauge (C,m)) * (((i -' 1) + 1),j))) by A13, A21, A26, GOBRD14:10;
then (((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1) < r / 2 by A13, A21, A26, A6, GOBRD14:5;
then A28: ((((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1)) + ((((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2)) < (r / 2) + (r / 2) by A27, XREAL_1:8;
A29: E-max C in right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by JORDAN1I:7;
then A30: (E-max C) `1 <= ((Gauge (C,m)) * (((i -' 1) + 1),j)) `1 by A22, A25, A23, A20, A21, A16, JORDAN9:17;
(Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 in LSeg ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by A8, TOPREAL1:21;
then A31: E-max (L~ (Cage (C,m))) in right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by A11, A9, XBOOLE_0:def 4;
then A32: ((Gauge (C,m)) * ((i -' 1),j)) `1 <= (E-max (L~ (Cage (C,m)))) `1 by A22, A25, A23, A20, A21, A16, JORDAN9:17;
A33: ((Gauge (C,m)) * ((i -' 1),j)) `2 <= (E-max (L~ (Cage (C,m)))) `2 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A34: (E-max (L~ (Cage (C,m)))) `1 <= ((Gauge (C,m)) * (((i -' 1) + 1),j)) `1 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A35: (E-max (L~ (Cage (C,m)))) `2 <= ((Gauge (C,m)) * ((i -' 1),(j + 1))) `2 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A36: (E-max C) `2 <= ((Gauge (C,m)) * ((i -' 1),(j + 1))) `2 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A37: ((Gauge (C,m)) * ((i -' 1),j)) `2 <= (E-max C) `2 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17;
((Gauge (C,m)) * ((i -' 1),j)) `1 <= (E-max C) `1 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17;
then dist ((E-max C),(E-max (L~ (Cage (C,m))))) <= ((((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1)) + ((((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2)) by A30, A37, A36, A32, A34, A33, A35, TOPREAL6:95;
then dist ((E-max C),(E-max (L~ (Cage (C,m))))) < r by A28, XXREAL_0:2;
then dist (w,p) < r by TOPREAL6:def 1;
then A38: 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 A7, A38, XBOOLE_0:3; :: thesis: verum