let a, b, c be ext-real number ; :: thesis: ( a < b & b < c implies b in REAL )
assume that
A1: a < b and
A2: b < c ; :: thesis: b in REAL
( b in REAL or b = +infty or b = -infty ) by Lm9;
hence b in REAL by A1, A2, Lm7, Lm8; :: thesis: verum