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, Lm9;

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, Lm9;

hence b = -infty by A1, A3, Lm10; :: thesis: verum