theorem :: MEASURE6:51

for q3 being Real
for X being non empty Subset of REAL st X is bounded_below holds
lower_bound (q3 ++ X) = q3 + (lower_bound X)