theorem Th12: :: MESFUNC5:12

for X being non empty set
for f being PartFunc of X,ExtREAL st f is nonnegative holds
f is () by SUPINF_2:51;