theorem Th7: :: SUPINF_2:8

for X, Y being non empty Subset of ExtREAL holds sup (X + Y) <= (sup X) + (sup Y)