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