theorem Th21: :: RCOMP_3:21

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