let a, b, c be ExtReal; :: thesis: ( a < b & b < c implies b in REAL )
assume A1: ( a < b & b < c ) ; :: thesis: b in REAL
( b in REAL or b = +infty or b = -infty ) by Lm10;
hence b in REAL by A1, Lm8, Lm9; :: thesis: verum