let p, q, r, s be ExtReal; ( r < p & r <= s implies not [.r,s.] c= [.p,q.] )
assume that
A1:
r < p
and
A2:
r <= s
; not [.r,s.] c= [.p,q.]
take t = r; MEMBERED:def 8 ( t in [.r,s.] & not t in [.p,q.] )
thus
t in [.r,s.]
by A2, Th1; not t in [.p,q.]
thus
not t in [.p,q.]
by A1, Th1; verum