theorem :: XXREAL_1:420

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