theorem Th24: :: RCOMP_3:24

for X being Subset of REAL st X is bounded_below holds
X c= right_closed_halfline (lower_bound X)