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
r
; MEMBERED:def 8 ( r in [.r,s.[ & not r in ].p,q.[ )
thus
r in [.r,s.[
by A2, Th3; not r in ].p,q.[
thus
not r in ].p,q.[
by A1, Th4; verum