theorem :: XXREAL_1:384

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