let C be Simple_closed_curve; :: thesis: for n, i, j being Element of NAT
for p, q being Point of (TOP-REAL 2)
for r being real number st dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r & p in cell (Gauge C,n),i,j & q in cell (Gauge C,n),i,j & 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) holds
dist p,q < 2 * r
let n, i, j be Element of NAT ; :: thesis: for p, q being Point of (TOP-REAL 2)
for r being real number st dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r & p in cell (Gauge C,n),i,j & q in cell (Gauge C,n),i,j & 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) holds
dist p,q < 2 * r
set G = Gauge C,n;
let p, q be Point of (TOP-REAL 2); :: thesis: for r being real number st dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r & p in cell (Gauge C,n),i,j & q in cell (Gauge C,n),i,j & 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) holds
dist p,q < 2 * r
let r be real number ; :: thesis: ( dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r & p in cell (Gauge C,n),i,j & q in cell (Gauge C,n),i,j & 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) implies dist p,q < 2 * r )
assume that
A1: dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r and
A2: dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r and
A3: p in cell (Gauge C,n),i,j and
A4: q in cell (Gauge C,n),i,j and
A5: ( 1 <= i & i + 1 <= len (Gauge C,n) ) and
A6: ( 1 <= j & j + 1 <= width (Gauge C,n) ) ; :: thesis: dist p,q < 2 * r
A7: ( i <= i + 1 & j <= j + 1 & 1 <= i + 1 & 1 <= j + 1 ) by NAT_1:11;
then ( i <= len (Gauge C,n) & j <= width (Gauge C,n) ) by A5, A6, XXREAL_0:2;
then A8: ( [i,(j + 1)] in Indices (Gauge C,n) & [i,j] in Indices (Gauge C,n) & [(i + 1),j] in Indices (Gauge C,n) ) by A5, A6, A7, MATRIX_1:37;
A9: ( ((Gauge C,n) * i,j) `1 <= p `1 & p `1 <= ((Gauge C,n) * (i + 1),j) `1 & ((Gauge C,n) * i,j) `2 <= p `2 & p `2 <= ((Gauge C,n) * i,(j + 1)) `2 ) by A3, A5, A6, JORDAN9:19;
( ((Gauge C,n) * i,j) `1 <= q `1 & q `1 <= ((Gauge C,n) * (i + 1),j) `1 & ((Gauge C,n) * i,j) `2 <= q `2 & q `2 <= ((Gauge C,n) * i,(j + 1)) `2 ) by A4, A5, A6, JORDAN9:19;
then A10: dist p,q <= ((((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, TOPREAL6:104;
A11: (((Gauge C,n) * (i + 1),j) `1 ) - (((Gauge C,n) * i,j) `1 ) < r by A2, A8, Th2;
(((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 ) < r by A1, A8, Th3;
then ((((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 + r by A11, XREAL_1:10;
hence dist p,q < 2 * r by A10, XXREAL_0:2; :: thesis: verum