theorem :: XXREAL_1:212

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