theorem :: XXREAL_1:406

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