theorem :: XXREAL_1:421

for s being ExtReal holds [.-infty,s.] = {-infty} \/ ].-infty,s.] by Th130, XXREAL_0:5;