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