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, Th2;
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 Th2;
verum end; end;