theorem :: XXREAL_1:411

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