let r be real number ; :: thesis: 0 <= r + (abs r)
0 <= abs r by COMPLEX1:132;
then A1: 0 + (abs r) <= (abs r) + (abs r) by XREAL_1:8;
( (abs r) + (abs r) = r + (abs r) or (abs r) + r = (- r) + r ) by Th1;
hence 0 <= r + (abs r) by A1, COMPLEX1:132; :: thesis: verum