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, Th3; :: thesis: not r in ].p,q.[
thus not r in ].p,q.[ by A1, Th4; :: thesis: verum