let C be Simple_closed_curve; :: thesis: for i, j, n being Nat
for p being Point of (TOP-REAL 2)
for r being Real
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, j, n be Nat; :: thesis: for p being Point of (TOP-REAL 2)
for r being Real
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
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; :: 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 object ; :: 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:17;
A12: ((Gauge (C,n)) * (i,j)) `2 <= Q `2 by A1, A2, A3, A4, A6, A9, JORDAN9:17;
A13: ((Gauge (C,n)) * (i,j)) `1 <= X `1 by A1, A2, A3, A4, A10, JORDAN9:17;
j < j + 1 by XREAL_1:29;
then A14: j <= width (Gauge (C,n)) by A4, XXREAL_0:2;
i < i + 1 by XREAL_1:29;
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_0:30;
A17: X `2 <= ((Gauge (C,n)) * (i,(j + 1))) `2 by A1, A2, A3, A4, A10, JORDAN9:17;
A18: ((Gauge (C,n)) * (i,j)) `2 <= X `2 by A1, A2, A3, A4, A10, JORDAN9:17;
A19: Q `2 <= ((Gauge (C,n)) * (i,(j + 1))) `2 by A1, A2, A3, A4, A6, A9, JORDAN9:17;
A20: X `1 <= ((Gauge (C,n)) * ((i + 1),j)) `1 by A1, A2, A3, A4, A10, JORDAN9:17;
1 <= j + 1 by A3, XREAL_1:29;
then [i,(j + 1)] in Indices (Gauge (C,n)) by A1, A4, A15, MATRIX_0:30;
then A21: (((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2) < r / 4 by A7, A16, Th2;
1 <= 1 + i by NAT_1:11;
then [(i + 1),j] in Indices (Gauge (C,n)) by A2, A3, A14, MATRIX_0:30;
then (((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1) < r / 4 by A8, A16, Th1;
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:7;
((Gauge (C,n)) * (i,j)) `1 <= Q `1 by A1, A2, A3, A4, A6, A9, JORDAN9:17;
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:95;
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:11; :: thesis: verum