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