theorem
:: SUPINF_2:30
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
iff (
inf
F
in
REAL
&
sup
F
in
REAL
) )
by
Th27
,
Th28
;