theorem Th328: :: XXREAL_1:328

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