theorem Th403: :: XXREAL_1:403

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