let A, B be non empty Interval; for p, q, r, s being R_eal st A = ].p,q.] & B = ].r,s.[ & A misses B & A \/ B is Interval holds
( q = r & A \/ B = ].p,s.[ )
let p, q, r, s be R_eal; ( A = ].p,q.] & B = ].r,s.[ & A misses B & A \/ B is Interval implies ( q = r & A \/ B = ].p,s.[ ) )
assume that
A1:
A = ].p,q.]
and
A2:
B = ].r,s.[
and
A3:
A misses B
and
A4:
A \/ B is Interval
; ( q = r & A \/ B = ].p,s.[ )
A5:
( p < q & r < s )
by A1, A2, XXREAL_1:26, XXREAL_1:28;
then A6:
( inf A = p & sup A = q & inf B = r & sup B = s )
by A1, A2, MEASURE6:8, MEASURE6:9, MEASURE6:13, MEASURE6:12;
now not s <= passume A7:
s <= p
;
contradictionthen
( not
s in A & not
s in B )
by A1, A2, XXREAL_1:2, XXREAL_1:4;
then A8:
not
s in A \/ B
by XBOOLE_0:def 3;
A9:
(
inf B < inf A &
sup B < sup A )
by A6, A7, A1, A2, XXREAL_1:26, XXREAL_1:28, XXREAL_0:2;
(
inf (A \/ B) = min (
(inf A),
(inf B)) &
sup (A \/ B) = max (
(sup A),
(sup B)) )
by XXREAL_2:9, XXREAL_2:10;
then
(
inf (A \/ B) < s &
s < sup (A \/ B) )
by A5, A6, A9, XXREAL_0:def 9, XXREAL_0:def 10;
hence
contradiction
by A8, A4, XXREAL_2:83;
verum end;
then A10:
q <= r
by A1, A2, A3, Th12;
now not q < rassume A11:
q < r
;
contradictionthen consider x being
R_eal such that A12:
(
q < x &
x < r &
x in REAL )
by MEASURE5:2;
( not
x in A & not
x in B )
by A1, A2, A12, XXREAL_1:2, XXREAL_1:4;
then A13:
not
x in A \/ B
by XBOOLE_0:def 3;
(
min (
(inf A),
(inf B))
= inf A &
max (
(sup A),
(sup B))
= sup B )
by A11, A6, A5, XXREAL_0:2, XXREAL_0:def 9, XXREAL_0:def 10;
then
(
inf (A \/ B) = inf A &
sup (A \/ B) = sup B )
by XXREAL_2:9, XXREAL_2:10;
then
(
inf (A \/ B) < x &
x < sup (A \/ B) )
by A6, A12, A1, A2, XXREAL_1:26, XXREAL_1:28, XXREAL_0:2;
hence
contradiction
by A13, A4, XXREAL_2:83;
verum end;
hence
q = r
by A10, XXREAL_0:1; A \/ B = ].p,s.[
hence
A \/ B = ].p,s.[
by A1, A2, A5, XXREAL_1:171; verum