f . (1 + 0) >= f . 0 by SEQM_3:def 8;
hence not difference f is negative by XREAL_1:48; :: thesis: verum