theorem :: XXREAL_1:289

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