a - 1 < a by XREAL_1:146;
hence not ].-infty,a.[ is empty by XXREAL_1:233; :: thesis: verum