theorem :: XXREAL_1:86

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