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

( 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