theorem :: XXREAL_3:76

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