:: deftheorem defines -infty XXREAL_0:def 3 :
-infty = [0,REAL];