theorem
Th17
:
:: SUPINF_2:18
for
X
being non
empty
set
for
Y
,
Z
being non
empty
Subset
of
ExtREAL
for
F
being
Function
of
X
,
Y
for
G
being
Function
of
X
,
Z
holds
(
inf
F
)
+
(
inf
G
)
<=
inf
(
F
+
G
)