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