theorem Th16: :: JORDAN1C:16

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