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