let a, b, c, x be Real; :: thesis: |.((b * ((a - x) - a)) / c).| = |.((b * ((a + x) - a)) / c).|
thus |.((b * ((a - x) - a)) / c).| = |.((- (x * b)) * (1 / c)).| by XCMPLX_1:99
.= |.(- ((x * b) * (1 / c))).|
.= |.(- ((x * b) / c)).| by XCMPLX_1:99
.= |.((b * ((a + x) - a)) / c).| by COMPLEX1:52 ; :: thesis: verum