let r be Real; :: thesis: 0 <= (- r) + |.r.|
- r >= - |.r.| by XREAL_1:24, COMPLEX1:76;
then (- r) + |.r.| >= (- |.r.|) + |.r.| by XREAL_1:7;
hence 0 <= (- r) + |.r.| ; :: thesis: verum