theorem Th47: :: BORSUK_5:48

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