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 Th2, Th3; :: thesis: verum