theorem Th329: :: XXREAL_1:329

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