let r, p, s, q be ext-real number ; :: thesis: ( r <= p & r <= s implies not [.r,s.] c= ].p,q.[ )
assume that
A1: r <= p and
A2: r <= s ; :: thesis: not [.r,s.] c= ].p,q.[
take r ; :: according to MEMBERED:def 8 :: thesis: ( r in [.r,s.] & not r in ].p,q.[ )
thus r in [.r,s.] by A2, Th1; :: thesis: not r in ].p,q.[
thus not r in ].p,q.[ by A1, Th4; :: thesis: verum