theorem Th91: :: XXREAL_3:91

for x being ExtReal holds (- 1) * x = - x