thus 0 < +infty by Th9; :: according to XXREAL_0:def 6 :: thesis: verum