theorem Th11: :: JORDAN1C:11

for n being Nat
for p being Point of (TOP-REAL 2)
for C being compact non vertical Subset of (TOP-REAL 2)
for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
I + 1 <= len (Gauge (C,n))