let r be real number ; :: thesis: 0 <= (- r) + (abs r)
r <= abs r by COMPLEX1:76;
then - r >= - (abs r) by XREAL_1:24;
then (- r) + (abs r) >= (- (abs r)) + (abs r) by XREAL_1:7;
hence 0 <= (- r) + (abs r) ; :: thesis: verum