let a be complex number ; :: thesis: (- a) " = - (a " )
thus (- a) " = 1 / (- a) by Lm4
.= - (1 / a) by Th189
.= - (a " ) by Lm4 ; :: thesis: verum