let r be real number ; :: thesis: 0 <= r + (abs r)
A1: 0 <= abs r by COMPLEX1:46;
( (abs r) + (abs r) = r + (abs r) or (abs r) + r = (- r) + r ) by Def1;
hence 0 <= r + (abs r) by A1; :: thesis: verum