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