theorem Th17: :: XXREAL_1:17

for r being ExtReal holds [.r,r.] = {r}