-infty in {REAL,[0,REAL]} by TARSKI:def 2;
then -infty in ExtREAL by XBOOLE_0:def 3;
hence -infty is ext-real ; :: thesis: verum