theorem Th38: :: XXREAL_2:38
inf {} = +infty