for X being non empty interval Subset of REAL st X is bounded_below & not X is bounded_above & not lower_bound X in X holds
X = right_open_halfline (lower_bound X)