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