theorem Th342: :: XXREAL_1:342

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