theorem Th25: :: RCOMP_3:25

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