theorem Th44: :: JORDAN2C:59
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