theorem :: SUPINF_2:51

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