let p, q, r, s be ExtReal; :: 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, Th3; :: thesis: not t in ].p,q.]
thus not t in ].p,q.] by A1, Th2; :: thesis: verum