theorem :: XXREAL_1:410

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