theorem :: SUPINF_2:52

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