theorem Th190: :: XXREAL_1:190
for r, s, t being ExtReal st s <= t holds
[.r,t.] \ [.s,t.] = [.r,s.[