theorem :: XXREAL_1:223

for p, r, s, t being ExtReal st r <= s & s <= t holds
not r in ].s,t.[ \/ ].t,p.[