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 Lm17
.= - 1 by A1, Lm5 ; :: thesis: verum