let X be non empty set ; :: thesis: for f being PartFunc of , st f is nonpositive holds
f is without+infty
let f be PartFunc of ,; :: 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