- f = (- 1) (#) f by MESFUNC2:9;
hence - f is nonpositive by MESFUNC5:20; :: thesis: verum