theorem :: XXREAL_0:8

not +infty in REAL by Lm0;