theorem :: XXREAL_1:367

for p, r being ExtReal st r < p holds
].r,+infty.] \ {p} = ].r,p.[ \/ ].p,+infty.] by Th315, XXREAL_0:3;