let a be ExtReal; :: thesis: ( a in REAL or a = +infty or a = -infty )
a in ExtREAL by Def1;
then ( a in REAL or a in {+infty,-infty} ) by XBOOLE_0:def 3;
hence ( a in REAL or a = +infty or a = -infty ) by TARSKI:def 2; :: thesis: verum