theorem :: XXREAL_1:216

for p being ExtReal holds ].+infty,p.] = {}