let x be R_eal; :: thesis: ( -infty < x & x < +infty implies x is Real )
assume A1: ( -infty < x & x < +infty ) ; :: thesis: x is Real
( x in REAL or x in {-infty ,+infty } ) by XBOOLE_0:def 3, XXREAL_0:def 4;
hence x is Real by A1, TARSKI:def 2; :: thesis: verum