theorem :: XXREAL_1:376

for p, s being ExtReal holds [.-infty,+infty.[ \ [.p,s.[ = [.-infty,p.[ \/ [.s,+infty.[ by Th327, XXREAL_0:3;