theorem Th130: :: XXREAL_1:130

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