theorem :: XXREAL_1:345

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