theorem :: XXREAL_0:46

for a, b, c being ExtReal st a in REAL & a <= b & b < c holds
b in REAL