for a, b being ExtReal st a in REAL & b >= a & not b in REAL holds
b = +infty