theorem :: JORDAN1C:18

for C being Simple_closed_curve
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