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