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