theorem :: XXREAL_1:408

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