theorem Th184: :: XXREAL_1:184

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