let p, q, r, s be ExtReal; ( [.r,s.[ meets [.p,q.[ implies [.r,s.[ \/ [.p,q.[ = [.(min (r,p)),(max (s,q)).[ )
assume
[.r,s.[ meets [.p,q.[
; [.r,s.[ \/ [.p,q.[ = [.(min (r,p)),(max (s,q)).[
then consider u being ExtReal such that
A1:
u in [.r,s.[
and
A2:
u in [.p,q.[
;
let t be ExtReal; MEMBERED:def 14 ( ( not t in [.r,s.[ \/ [.p,q.[ or t in [.(min (r,p)),(max (s,q)).[ ) & ( not t in [.(min (r,p)),(max (s,q)).[ or t in [.r,s.[ \/ [.p,q.[ ) )
thus
( t in [.r,s.[ \/ [.p,q.[ implies t in [.(min (r,p)),(max (s,q)).[ )
( not t in [.(min (r,p)),(max (s,q)).[ or t in [.r,s.[ \/ [.p,q.[ )proof
assume
t in [.r,s.[ \/ [.p,q.[
;
t in [.(min (r,p)),(max (s,q)).[
then
(
t in [.r,s.[ or
t in [.p,q.[ )
by XBOOLE_0:def 3;
then A3:
( (
r <= t &
t < s ) or (
p <= t &
t < q ) )
by Th3;
then A4:
min (
r,
p)
<= t
by XXREAL_0:23;
t < max (
s,
q)
by A3, XXREAL_0:30;
hence
t in [.(min (r,p)),(max (s,q)).[
by A4, Th3;
verum
end;
A5:
r <= u
by A1, Th3;
A6:
u < s
by A1, Th3;
A7:
p <= u
by A2, Th3;
A8:
u < q
by A2, Th3;
assume A9:
t in [.(min (r,p)),(max (s,q)).[
; t in [.r,s.[ \/ [.p,q.[
then A10:
min (r,p) <= t
by Th3;
A11:
t < max (s,q)
by A9, Th3;