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