theorem :: XXREAL_1:343

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