let x be ExtInt; :: thesis: -infty < x
( x is Integer or x = +infty ) by Def1;
then ( x in REAL or x = +infty ) by XREAL_0:def 1;
hence -infty < x by XXREAL_0:12; :: thesis: verum