theorem :: XXREAL_1:170

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