let a be Real; :: 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:234; :: thesis: verum