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