theorem Th26: :: RCOMP_3:26

for X being Subset of REAL st X is bounded_below & not lower_bound X in X holds
X c= right_open_halfline (lower_bound X)