let a, b, c be Complex; :: thesis: ( b <> 0 implies c - (a / b) = ((c * b) - a) / b )
assume A1: b <> 0 ; :: thesis: c - (a / b) = ((c * b) - a) / b
thus c - (a / b) = - ((a / b) - c)
.= - ((a - (c * b)) / b) by A1, Th126
.= (- (a - (c * b))) / b by Lm17
.= ((c * b) - a) / b ; :: thesis: verum