proof

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

end;