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 & (Gauge C,n) * i,j in Ball q,r & (Gauge C,n) * (i + 1),j in Ball q,r & (Gauge C,n) * i,(j + 1) in Ball q,r & (Gauge C,n) * (i + 1),(j + 1) in Ball q,r 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 & (Gauge C,n) * i,j in Ball q,r & (Gauge C,n) * (i + 1),j in Ball q,r & (Gauge C,n) * i,(j + 1) in Ball q,r & (Gauge C,n) * (i + 1),(j + 1) in Ball q,r 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 & (Gauge C,n) * i,j in Ball q,r & (Gauge C,n) * (i + 1),j in Ball q,r & (Gauge C,n) * i,(j + 1) in Ball q,r & (Gauge C,n) * (i + 1),(j + 1) in Ball q,r 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 & (Gauge C,n) * i,j in Ball q,r & (Gauge C,n) * (i + 1),j in Ball q,r & (Gauge C,n) * i,(j + 1) in Ball q,r & (Gauge C,n) * (i + 1),(j + 1) in Ball q,r 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 & (Gauge C,n) * i,j in Ball q,r & (Gauge C,n) * (i + 1),j in Ball q,r & (Gauge C,n) * i,(j + 1) in Ball q,r & (Gauge C,n) * (i + 1),(j + 1) in Ball q,r implies cell (Gauge C,n),i,j c= Ball q,r )
assume that
A1: ( 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) ) and
A2: ( 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 & (Gauge C,n) * i,j in Ball q,r & (Gauge C,n) * (i + 1),j in Ball q,r & (Gauge C,n) * i,(j + 1) in Ball q,r & (Gauge C,n) * (i + 1),(j + 1) in Ball q,r ) ; :: thesis: cell (Gauge C,n),i,j c= Ball q,r
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 A3: x in cell (Gauge C,n),i,j ; :: thesis: x in Ball q,r
set I = i;
set J = j;
set l = r / 4;
reconsider Q = q, X = x as Point of (TOP-REAL 2) by A3, Lm5;
reconsider x' = x as Point of (Euclid 2) by A3, Lm3;
set G = Gauge C,n;
A4: 1 <= 1 + i by NAT_1:11;
( i < i + 1 & j < j + 1 ) by XREAL_1:31;
then A5: ( i <= len (Gauge C,n) & j <= width (Gauge C,n) ) by A1, XXREAL_0:2;
then A6: ( [i,j] in Indices (Gauge C,n) & [(i + 1),j] in Indices (Gauge C,n) ) by A1, A4, MATRIX_1:37;
then A7: (((Gauge C,n) * (i + 1),j) `1 ) - (((Gauge C,n) * i,j) `1 ) < r / 4 by A2, Th2;
1 <= j + 1 by A1, XREAL_1:31;
then [i,(j + 1)] in Indices (Gauge C,n) by A1, A5, MATRIX_1:37;
then A8: (((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 ) < r / 4 by A2, A6, Th3;
A9: ( ((Gauge C,n) * i,j) `1 <= Q `1 & Q `1 <= ((Gauge C,n) * (i + 1),j) `1 ) by A1, A2, JORDAN9:19;
A10: ( ((Gauge C,n) * i,j) `2 <= Q `2 & Q `2 <= ((Gauge C,n) * i,(j + 1)) `2 ) by A1, A2, JORDAN9:19;
A11: ( ((Gauge C,n) * i,j) `1 <= X `1 & X `1 <= ((Gauge C,n) * (i + 1),j) `1 ) by A1, A3, JORDAN9:19;
( ((Gauge C,n) * i,j) `2 <= X `2 & X `2 <= ((Gauge C,n) * i,(j + 1)) `2 ) by A1, A3, JORDAN9:19;
then A12: 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 A9, A10, A11, TOPREAL6:104;
((((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 A7, A8, XREAL_1:9;
then A13: dist p,X <= (r / 4) + (r / 4) by A2, A12, XXREAL_0:2;
2 * (r / 4) < r by A2, Lm4;
then dist X,p < r by A13, XXREAL_0:2;
then dist x',q < r by A2, TOPREAL6:def 1;
hence x in Ball q,r by METRIC_1:12; :: thesis: verum