theorem :: XXREAL_1:295

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