theorem :: XXREAL_0:7

-infty < +infty by Lm7;