theorem :: XXREAL_1:368

for p, r being ExtReal st r <= p holds
[.r,+infty.] \ {p} = [.r,p.[ \/ ].p,+infty.]