theorem :: XXREAL_1:365

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