theorem Th195: :: XXREAL_1:195

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