:: deftheorem defines ExtREAL NUMBERS:def 5 :
ExtREAL = REAL \/ {REAL,[0,REAL]};