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