let C be Simple_closed_curve; :: thesis: for i, n, j being Element of NAT
for p being Point of (TOP-REAL 2)
for r being real number
for q being Point of (Euclid 2) st 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) & r > 0 & p = q & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r / 4 & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r / 4 & p in cell (Gauge C,n),i,j holds
cell (Gauge C,n),i,j c= Ball q,r
let i, n, j be Element of NAT ; :: thesis: for p being Point of (TOP-REAL 2)
for r being real number
for q being Point of (Euclid 2) st 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) & r > 0 & p = q & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r / 4 & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r / 4 & p in cell (Gauge C,n),i,j holds
cell (Gauge C,n),i,j c= Ball q,r
let p be Point of (TOP-REAL 2); :: thesis: for r being real number
for q being Point of (Euclid 2) st 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) & r > 0 & p = q & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r / 4 & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r / 4 & p in cell (Gauge C,n),i,j holds
cell (Gauge C,n),i,j c= Ball q,r
let r be real number ; :: thesis: for q being Point of (Euclid 2) st 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) & r > 0 & p = q & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r / 4 & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r / 4 & p in cell (Gauge C,n),i,j holds
cell (Gauge C,n),i,j c= Ball q,r
let q be Point of (Euclid 2); :: thesis: ( 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) & r > 0 & p = q & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r / 4 & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r / 4 & p in cell (Gauge C,n),i,j implies cell (Gauge C,n),i,j c= Ball q,r )
assume that
A1: 1 <= i and
A2: i + 1 <= len (Gauge C,n) and
A3: 1 <= j and
A4: j + 1 <= width (Gauge C,n) and
A5: r > 0 and
A6: p = q and
A7: dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r / 4 and
A8: dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r / 4 and
A9: p in cell (Gauge C,n),i,j ; :: thesis: cell (Gauge C,n),i,j c= Ball q,r
set G = Gauge C,n;
set I = i;
set J = j;
set l = r / 4;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in cell (Gauge C,n),i,j or x in Ball q,r )
assume A10: x in cell (Gauge C,n),i,j ; :: thesis: x in Ball q,r
then reconsider Q = q, X = x as Point of (TOP-REAL 2) by Lm5;
A11: Q `1 <= ((Gauge C,n) * (i + 1),j) `1 by A1, A2, A3, A4, A6, A9, JORDAN9:19;
A12: ((Gauge C,n) * i,j) `2 <= Q `2 by A1, A2, A3, A4, A6, A9, JORDAN9:19;
A13: ((Gauge C,n) * i,j) `1 <= X `1 by A1, A2, A3, A4, A10, JORDAN9:19;
j < j + 1 by XREAL_1:31;
then A14: j <= width (Gauge C,n) by A4, XXREAL_0:2;
i < i + 1 by XREAL_1:31;
then A15: i <= len (Gauge C,n) by A2, XXREAL_0:2;
then A16: [i,j] in Indices (Gauge C,n) by A1, A3, A14, MATRIX_1:37;
A17: X `2 <= ((Gauge C,n) * i,(j + 1)) `2 by A1, A2, A3, A4, A10, JORDAN9:19;
A18: ((Gauge C,n) * i,j) `2 <= X `2 by A1, A2, A3, A4, A10, JORDAN9:19;
A19: Q `2 <= ((Gauge C,n) * i,(j + 1)) `2 by A1, A2, A3, A4, A6, A9, JORDAN9:19;
A20: X `1 <= ((Gauge C,n) * (i + 1),j) `1 by A1, A2, A3, A4, A10, JORDAN9:19;
1 <= j + 1 by A3, XREAL_1:31;
then [i,(j + 1)] in Indices (Gauge C,n) by A1, A4, A15, MATRIX_1:37;
then A21: (((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 ) < r / 4 by A7, A16, Th3;
1 <= 1 + i by NAT_1:11;
then [(i + 1),j] in Indices (Gauge C,n) by A2, A3, A14, MATRIX_1:37;
then (((Gauge C,n) * (i + 1),j) `1 ) - (((Gauge C,n) * i,j) `1 ) < r / 4 by A8, A16, Th2;
then A22: ((((Gauge C,n) * (i + 1),j) `1 ) - (((Gauge C,n) * i,j) `1 )) + ((((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 )) <= (r / 4) + (r / 4) by A21, XREAL_1:9;
((Gauge C,n) * i,j) `1 <= Q `1 by A1, A2, A3, A4, A6, A9, JORDAN9:19;
then dist Q,X <= ((((Gauge C,n) * (i + 1),j) `1 ) - (((Gauge C,n) * i,j) `1 )) + ((((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 )) by A11, A12, A19, A13, A20, A18, A17, TOPREAL6:104;
then A23: dist p,X <= (r / 4) + (r / 4) by A6, A22, XXREAL_0:2;
reconsider x9 = x as Point of (Euclid 2) by A10, Lm3;
2 * (r / 4) < r by A5, Lm4;
then dist X,p < r by A23, XXREAL_0:2;
then dist x9,q < r by A6, TOPREAL6:def 1;
hence x in Ball q,r by METRIC_1:12; :: thesis: verum