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