let a be Complex; :: thesis: (- a) " = - (a ")
thus (- a) " = 1 / (- a) by Lm4
.= - (1 / a) by Th188
.= - (a ") by Lm4 ; :: thesis: verum