let a be Complex; :: thesis: ( a <> 0 implies a / (- a) = - 1 )
assume A1: a <> 0 ; :: thesis: a / (- a) = - 1
thus a / (- a) = - (a / a) by Th188
.= - 1 by A1, Lm5 ; :: thesis: verum