theorem :: XXREAL_1:207

for r, s, t being ExtReal holds not s in ].r,s.[ \/ ].s,t.]