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