theorem :: XXREAL_1:296

for r being ExtReal
for s being Real holds ].r,+infty.[ \ ].s,+infty.[ = ].r,s.]