let a, b be Complex; :: thesis: (- a) / (- b) = a / b
- ((- a) / b) = a / b by Th190;
hence (- a) / (- b) = a / b by Th188; :: thesis: verum