theorem Th131: :: XXREAL_1:131

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