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