theorem Th8: :: MESFUNC5:8

for X being set
for F being PartFunc of X,ExtREAL holds
( F is nonpositive iff for n being object holds F . n <= 0. )