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