let a, b be Complex; :: thesis: ( a / b = - 1 implies ( a = - b & b = - a ) )
assume A1: a / b = - 1 ; :: thesis: ( a = - b & b = - a )
then b <> 0 by Th49;
then a = (- 1) * b by A1, Lm3;
hence ( a = - b & b = - a ) ; :: thesis: verum