let a be real number ; :: thesis: ].-infty,a.[ <> REAL
A1: a + 1 > a by XREAL_1:29;
a + 1 in REAL by XREAL_0:def 1;
hence ].-infty,a.[ <> REAL by A1, XXREAL_1:233; :: thesis: verum