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