theorem Th39: :: JORDAN2C:52

for n being Nat
for a being Real st n >= 1 holds
(REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } <> {}