theorem :: XXREAL_1:288

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