theorem :: XXREAL_1:395

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