theorem Th9: :: MESFUNC5:9

for X being set
for F being PartFunc of X,ExtREAL st ( for n being set st n in dom F holds
F . n <= 0. ) holds
F is nonpositive