theorem :: XXREAL_3:77

for x being ExtReal holds x / -infty = 0 ;