theorem Th123: :: SEQ_4:124

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