theorem Th28: :: RCOMP_3:28
for X being interval Subset of REAL st not X is bounded_above & not X is bounded_below holds
X = REAL