theorem :: XXREAL_1:380

for p, s being ExtReal holds [.-infty,+infty.] \ [.p,s.] = [.-infty,p.[ \/ ].s,+infty.] by Th332, XXREAL_0:3;