theorem Th404: :: XXREAL_1:404

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