f . (1 + 0) <= f . 0 by SEQM_3:def 9;
hence not difference f is positive by XREAL_1:47; :: thesis: verum