theorem :: XXREAL_1:138

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