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