theorem :: XXREAL_1:379

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