theorem Th197: :: XXREAL_1:197

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