theorem :: XXREAL_1:294

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