theorem :: XXREAL_1:208

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