theorem Th21: :: JORDAN2C:34
for n being Nat
for A being Subset of (TOP-REAL n) holds
( A is bounded iff ex r being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r )