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