theorem Th189: :: XXREAL_1:189

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