reconsider g = - f as real-valued Function ;
(abs g) + g is nonnegative-yielding ;
then (abs g) - f is nonnegative-yielding by VALUED_1:def 9;
hence (abs f) - f is nonnegative-yielding by EUCLID:5; :: thesis: verum