theorem :: XXREAL_1:202

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