let a be Real; :: thesis: [.a,+infty.[ <> REAL
A1: a - 1 < a by XREAL_1:146;
a - 1 in REAL by XREAL_0:def 1;
hence [.a,+infty.[ <> REAL by A1, XXREAL_1:236; :: thesis: verum