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 Real; MEMBERED:def 21 ( 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 Th4;
then
t <= p
by A1, XXREAL_0:2;
hence
not t in ].p,q.[
by Th4; verum