theorem Th10: :: RCOMP_3:10

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