thus 0 > -infty by Th12; :: according to XXREAL_0:def 7 :: thesis: verum