theorem :: XXREAL_1:201

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