theorem Th45: :: JORDAN2C:60

for W being Subset of (Euclid 1)
for a being Real st W = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) } holds
not W is bounded