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 t = r; :: according to MEMBERED:def 8 :: thesis: ( t in [.r,s.] & not t in [.p,q.] )
thus t in [.r,s.] by A2, Th1; :: thesis: not t in [.p,q.]
thus not t in [.p,q.] by A1, Th1; :: thesis: verum