theorem Th349: :: XXREAL_1:349

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