theorem :: XXREAL_1:286

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