theorem Th13: :: MESFUNC5:13

for X being non empty set
for f being PartFunc of X,ExtREAL st f is nonpositive holds
f is () by Th8;