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