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