theorem Th92: :: XXREAL_3:92

for x, y being ExtReal holds - (x * y) = (- x) * y