theorem Th23: :: RCOMP_3:23

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