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