theorem :: XXREAL_1:409

for s being Real holds [.s,+infty.] \ [.s,+infty.[ = {+infty}