theorem Th182: :: XXREAL_1:182

for r, s, t being ExtReal st r <= s holds
[.r,t.] \ [.r,s.] = ].s,t.]