:: deftheorem defines ExtREAL XXREAL_0:def 4 :
ExtREAL = REAL \/ {+infty,-infty};