theorem :: XXREAL_1:351

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