theorem Th183: :: XXREAL_1:183

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