theorem Th129: :: XXREAL_1:129

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