theorem :: XXREAL_1:291

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