A1: - (- r) <= 0 by XXREAL_0:def 6;
assume - r < 0 ; :: according to XXREAL_0:def 7 :: thesis: contradiction
then (- r) + (- (- r)) < 0 by A1, Lm17;
hence contradiction ; :: thesis: verum