let a, b, c be Real; :: thesis: ( b > 0 & c > 0 implies for x being Real st x in ['(a - c),(a + c)'] holds
0 <= b - |.((b * (x - a)) / c).| )
assume A1: ( b > 0 & c > 0 ) ; :: thesis: for x being Real st x in ['(a - c),(a + c)'] holds
0 <= b - |.((b * (x - a)) / c).|
let x be Real; :: thesis: ( x in ['(a - c),(a + c)'] implies 0 <= b - |.((b * (x - a)) / c).| )
assume A2: x in ['(a - c),(a + c)'] ; :: thesis: 0 <= b - |.((b * (x - a)) / c).|
A10a: ( a - c <= a & a <= a + c ) by XREAL_1:43, XREAL_1:29, A1;
x in [.(a - c),(a + c).] by INTEGRA5:def 3, XXREAL_0:2, A2, A10a;
then ( a - c <= x & x <= a + c ) by XXREAL_1:1;
then A3a: ( (a - c) + c <= x + c & x - x <= (a + c) - x ) by XREAL_1:13, XREAL_1:6;
then A3: ( c - (x - a) >= 0 & (c + x) - a >= a - a ) by XREAL_1:13;

per cases ( 0 <= (b * (x - a)) / c or (b * (x - a)) / c < 0 ) ;

suppose 0 <= (b * (x - a)) / c ; :: thesis: 0 <= b - |.((b * (x - a)) / c).|

then b - |.((b * (x - a)) / c).| = b - ((b * (x - a)) / c) by ABSVALUE:def 1
.= ((b * c) - (b * (x - a))) / c by XCMPLX_1:127, A1
.= (b * (c - (x - a))) / c ;
hence 0 <= b - |.((b * (x - a)) / c).| by A1, A3a; :: thesis: verum

end;

suppose (b * (x - a)) / c < 0 ; :: thesis: 0 <= b - |.((b * (x - a)) / c).|

then b - |.((b * (x - a)) / c).| = b - (- ((b * (x - a)) / c)) by ABSVALUE:def 1
.= ((b * (x - a)) / c) + b
.= ((b * c) + (b * (x - a))) / c by XCMPLX_1:113, A1
.= (b * ((c + x) - a)) / c ;
hence 0 <= b - |.((b * (x - a)) / c).| by A1, A3; :: thesis: verum

end;

end;