let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL st f is nonpositive holds
f is without+infty
let f be PartFunc of X,ExtREAL; :: thesis: ( f is nonpositive implies f is without+infty )
assume f is nonpositive ; :: thesis: f is without+infty
then for x being set holds f . x < +infty by Th14;
hence f is without+infty by Def6; :: thesis: verum