for X, Y being Subset of REAL st X is bounded_below & Y is bounded_below holds
X ++ Y is bounded_below