theorem Th11: :: RCOMP_3:11

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