theorem Th9: :: RCOMP_3:9

for a being Real holds upper_bound (left_closed_halfline a) = a