let a, b be complex number ; :: thesis: (- a) / (- b) = a / b
- ((- a) / b) = a / b by Th191;
hence (- a) / (- b) = a / b by Th189; :: thesis: verum