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