let r be Real; :: thesis: 0 <= r + |.r.|
A1: 0 <= |.r.| by COMPLEX1:46;
( |.r.| + |.r.| = r + |.r.| or |.r.| + r = (- r) + r ) by Def1;
hence 0 <= r + |.r.| by A1; :: thesis: verum