theorem :: XXREAL_1:203

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