theorem Th187: :: XXREAL_1:187

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