theorem Th173: :: XXREAL_1:173

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