theorem Th341: :: XXREAL_1:341

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