theorem :: XXREAL_3:99

for f being ExtReal holds (- f) " = - (f ")