let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL st f is nonnegative holds
f is ()
let f be PartFunc of X,ExtREAL; :: thesis: ( f is nonnegative implies f is () )
assume f is nonnegative ; :: thesis: f is ()
then for x being set holds -infty < f . x by SUPINF_2:51;
hence f is () by Def5; :: thesis: verum