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 Th3;
then
t < p
by A1, XXREAL_0:2;
hence
not t in [.p,q.]
by Th1; verum