- f = (- 1) (#) f by VALUED_1:def 6;
hence - f is nonpositive-yielding ; :: thesis: verum