theorem :: XXREAL_1:293

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