theorem Th14: :: JORDAN1C:14

for C being Simple_closed_curve
for n being Nat
for p being Point of (TOP-REAL 2)
for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1))