theorem :: XXREAL_1:378

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