theorem :: XXREAL_1:366

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