theorem :: XXREAL_1:418

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