let a, b, c, d be Real; :: thesis: ( b > 0 & c > 0 & d > 0 implies for x being Real st not x in ['(a - c),(a + c)'] holds
min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = 0 )
assume that
A1: b > 0 and
A2: c > 0 and
A3: d > 0 ; :: thesis: for x being Real st not x in ['(a - c),(a + c)'] holds
min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = 0
let x be Real; :: thesis: ( not x in ['(a - c),(a + c)'] implies min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = 0 )
assume not x in ['(a - c),(a + c)'] ; :: thesis: min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = 0
then min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = min (d,0) by FU710a, A1, A2
.= 0 by XXREAL_0:def 9, A3 ;
hence min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = 0 ; :: thesis: verum