take r = 1; :: thesis: r is positive
thus 0 < r by Lm4, Lm8; :: according to XXREAL_0:def 6 :: thesis: verum