let x be ext-real number ; :: thesis: ( x <> -infty & x <> +infty implies x is Real )
assume A1: ( x <> -infty & x <> +infty ) ; :: thesis: x is Real
x in ExtREAL by XXREAL_0:def 1;
then ( 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