let s, r, t be ext-real number ; :: 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 Th3, Th4; :: thesis: verum