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