+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