theorem :: XXREAL_1:87

for r, s being ExtReal holds [.r,s.[ misses {s}