let p, q, r, s be ExtReal; ( q < s & r < s implies not ].r,s.] c= [.p,q.] )
assume that
A1:
q < s
and
A2:
r < s
; not ].r,s.] c= [.p,q.]
per cases
( r <= q or q <= r )
;
suppose A3:
r <= q
;
not ].r,s.] c= [.p,q.]consider t being
ExtReal such that A4:
q < t
and A5:
t < s
by A1, XREAL_1:227;
take
t
;
MEMBERED:def 8 ( t in ].r,s.] & not t in [.p,q.] )
r < t
by A3, A4, XXREAL_0:2;
hence
t in ].r,s.]
by A5, Th2;
not t in [.p,q.]thus
not
t in [.p,q.]
by A4, Th1;
verum end; suppose A6:
q <= r
;
not ].r,s.] c= [.p,q.]consider t being
ExtReal such that A7:
r < t
and A8:
t < s
by A2, XREAL_1:227;
take
t
;
MEMBERED:def 8 ( t in ].r,s.] & not t in [.p,q.] )thus
t in ].r,s.]
by A7, A8, Th2;
not t in [.p,q.]
q < t
by A6, A7, XXREAL_0:2;
hence
not
t in [.p,q.]
by Th1;
verum end; end;