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 and
A6: i + 1 <= len (Gauge C,n) and
A7: 1 <= j and
A8: j + 1 <= width (Gauge C,n) ; :: thesis: dist p,q < 2 * r
A9: p `1 <= ((Gauge C,n) * (i + 1),j) `1 by A3, A5, A6, A7, A8, JORDAN9:19;
A10: p `2 <= ((Gauge C,n) * i,(j + 1)) `2 by A3, A5, A6, A7, A8, JORDAN9:19;
A11: ((Gauge C,n) * i,j) `2 <= p `2 by A3, A5, A6, A7, A8, JORDAN9:19;
j <= j + 1 by NAT_1:11;
then A12: j <= width (Gauge C,n) by A8, XXREAL_0:2;
i <= i + 1 by NAT_1:11;
then A13: i <= len (Gauge C,n) by A6, XXREAL_0:2;
then A14: [i,j] in Indices (Gauge C,n) by A5, A7, A12, MATRIX_1:37;
A15: q `2 <= ((Gauge C,n) * i,(j + 1)) `2 by A4, A5, A6, A7, A8, JORDAN9:19;
A16: ((Gauge C,n) * i,j) `2 <= q `2 by A4, A5, A6, A7, A8, JORDAN9:19;
A17: q `1 <= ((Gauge C,n) * (i + 1),j) `1 by A4, A5, A6, A7, A8, JORDAN9:19;
A18: ((Gauge C,n) * i,j) `1 <= q `1 by A4, A5, A6, A7, A8, JORDAN9:19;
1 <= j + 1 by NAT_1:11;
then [i,(j + 1)] in Indices (Gauge C,n) by A5, A8, A13, MATRIX_1:37;
then A19: (((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 ) < r by A1, A14, Th3;
1 <= i + 1 by NAT_1:11;
then [(i + 1),j] in Indices (Gauge C,n) by A6, A7, A12, MATRIX_1:37;
then (((Gauge C,n) * (i + 1),j) `1 ) - (((Gauge C,n) * i,j) `1 ) < r by A2, A14, Th2;
then A20: ((((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 A19, XREAL_1:10;
((Gauge C,n) * i,j) `1 <= p `1 by A3, A5, A6, A7, A8, JORDAN9:19;
then 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, A11, A10, A18, A17, A16, A15, TOPREAL6:104;
hence dist p,q < 2 * r by A20, XXREAL_0:2; :: thesis: verum