let p, r, s, t be ExtReal; :: thesis: ( r <= s & s <= t implies not r in ].s,t.[ \/ ].t,p.[ )
assume that
A1: r <= s and
A2: s <= t ; :: thesis: not r in ].s,t.[ \/ ].t,p.[
assume r in ].s,t.[ \/ ].t,p.[ ; :: thesis: contradiction
then ( r in ].s,t.[ or r in ].t,p.[ ) by XBOOLE_0:def 3;
then ( ( s < r & r < t ) or ( t < r & r < p ) ) by Th4;
hence contradiction by A1, A2, XXREAL_0:2; :: thesis: verum