theorem :: XXREAL_0:45

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