let a, x be Real; :: thesis: a - |.x.| <= a
|.x.| >= 0 by COMPLEX1:46;
then (- |.x.|) + a <= 0 + a by XREAL_1:6;
hence a - |.x.| <= a ; :: thesis: verum