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