theorem :: XXREAL_1:423

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