theorem Th402: :: XXREAL_1:402

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