theorem :: XXREAL_1:407

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