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