let a, b be Complex; :: thesis: - (a / b) = (- a) / b
thus - (a / b) = - (a * (b ")) by XCMPLX_0:def 9
.= (- a) * (b ")
.= (- a) / b by XCMPLX_0:def 9 ; :: thesis: verum