theorem :: XXREAL_1:290

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