theorem Th171: :: XXREAL_1:171

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