theorem :: XXREAL_1:287

for t being ExtReal
for s being Real holds [.-infty,t.[ \ [.-infty,s.[ = [.s,t.[