theorem :: XXREAL_1:393

for r, s being ExtReal
for p being Real st r < s holds
].r,+infty.[ \ ].p,s.] = ].r,p.] \/ ].s,+infty.[