:: deftheorem defines +infty XXREAL_0:def 2 :
+infty = REAL ;