theorem :: XXREAL_1:352

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