theorem
:: SUPINF_2:11
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
;