reconsider g = - f as real-valued nonnegative-yielding Function ;
delneg f = delpos g by DNF;
hence delneg f is empty-yielding ; :: thesis: verum