theorem Th325: :: XXREAL_1:325

for p, q, s being ExtReal st p < q holds
[.-infty,q.[ \ ].p,s.[ = [.-infty,p.] \/ [.s,q.[ by Th298, XXREAL_0:5;