let p, q, r, s be ExtReal; ( s <= p implies [.r,s.] misses ].p,q.[ )
assume A1:
s <= p
; [.r,s.] misses ].p,q.[
let t be ExtReal; MEMBERED:def 20 ( not t in [.r,s.] or not t in ].p,q.[ )
assume
t in [.r,s.]
; not t in ].p,q.[
then
t <= s
by Th1;
then
t <= p
by A1, XXREAL_0:2;
hence
not t in ].p,q.[
by Th4; verum