for X, Y being Subset of REAL st X <> {} & X is bounded_below & Y <> {} & Y is bounded_below holds
lower_bound (X ++ Y) = (lower_bound X) + (lower_bound Y)