theorem Th8: :: SUPINF_2:9

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