theorem :: XXREAL_1:346

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