theorem :: XXREAL_1:400

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