let p, q, r, s be ExtReal; ( p <= r & s < q implies [.r,s.] c= [.p,q.[ )
assume that
A1:
p <= r
and
A2:
s < q
; [.r,s.] c= [.p,q.[
let t be ExtReal; MEMBERED:def 8 ( not t in [.r,s.] or t in [.p,q.[ )
assume A3:
t in [.r,s.]
; t in [.p,q.[
then A4:
r <= t
by Th1;
A5:
t <= s
by A3, Th1;
A6:
p <= t
by A1, A4, XXREAL_0:2;
t < q
by A2, A5, XXREAL_0:2;
hence
t in [.p,q.[
by A6, Th3; verum