theorem Th37: :: JORDAN2C:50

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