theorem
Th38
:
:: SUPINF_2:39
for
X
being
set
for
F
being
PartFunc
of
X
,
ExtREAL
holds
(
F
is
nonnegative
iff for
n
being
Element
of
X
holds
0.
<=
F
.
n
)