for X, Y being non empty Subset of ExtREAL st X is bounded_below & Y is bounded_below holds
(inf X) + (inf Y) <= inf (X + Y) by Th8;