theorem :: XXREAL_1:412

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