theorem Th167: :: XXREAL_1:167

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