theorem
Th27
:
:: SUPINF_2:28
for
X
being non
empty
set
for
Y
being non
empty
Subset
of
ExtREAL
for
F
being
Function
of
X
,
Y
st
Y
c=
REAL
holds
(
F
is
bounded_above
iff
sup
F
in
REAL
)