theorem Th12: :: RCOMP_3:12

for a being Real holds lower_bound (right_open_halfline a) = a