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

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