take r = - 1; :: thesis: r is negative
thus 0 > r by Lm7, Lm13, XXREAL_0:def 5; :: according to XXREAL_0:def 7 :: thesis: verum