-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