theorem :: XXREAL_1:205

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