let x, y be ExtReal; :: thesis: - (x * y) = (- x) * y
thus - (x * y) = (- 1) * (x * y) by Th91
.= ((- 1) * x) * y by Th66
.= (- x) * y by Th91 ; :: thesis: verum