a < a + 1 by XREAL_1:29;
hence not ].a,+infty.] is empty by XXREAL_0:3, XXREAL_1:2; :: thesis: verum