theorem :: XXREAL_1:422

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