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