theorem :: SUPINF_2:10

for X, Y being non empty Subset of ExtREAL st X is bounded_above & Y is bounded_above holds
sup (X + Y) <= (sup X) + (sup Y) by Th7;