theorem
Th26
:
:: SUPINF_2:27
for
X
being non
empty
set
for
Y
being non
empty
Subset
of
ExtREAL
for
F
being
Function
of
X
,
Y
for
x
being
Element
of
X
holds
(
inf
F
<=
F
.
x
&
F
.
x
<=
sup
F
)