theorem
Th7
:
:: SUPINF_2:8
for
X
,
Y
being non
empty
Subset
of
ExtREAL
holds
sup
(
X
+
Y
)
<=
(
sup
X
)
+
(
sup
Y
)