theorem :: XXREAL_1:206

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