theorem Th185: :: XXREAL_1:185

for r, s, t being ExtReal st r < s holds
[.r,t.[ \ [.r,s.[ = [.s,t.[