let a, b be ExtReal; :: thesis: ( a in REAL & b >= a & not b in REAL implies b = +infty )
assume that
A1: a in REAL and
A2: b >= a ; :: thesis: ( b in REAL or b = +infty )
assume A3: not b in REAL ; :: thesis: b = +infty
( b = -infty implies a = -infty ) by A2, Lm8;
hence b = +infty by A1, A3, Lm10; :: thesis: verum