for a being Real holds ].-infty,a.[ <> REAL by XREAL_0:def 1, XXREAL_1:233;