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