theorem Th128: :: XXREAL_1:128

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