let r, s, t be ExtReal; :: thesis: not s in ].r,s.[ \/ ].s,t.[
assume s in ].r,s.[ \/ ].s,t.[ ; :: thesis: contradiction
then ( s in ].r,s.[ or s in ].s,t.[ ) by XBOOLE_0:def 3;
hence contradiction by Th4; :: thesis: verum