theorem Th401: :: XXREAL_1:401

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