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:29;
then A6:
( inf A = p & sup A = q & inf B = r & sup B = s )
by A1, A2, MEASURE6:10, MEASURE6:14, MEASURE6:9, MEASURE6:13;
now not s < passume A7:
s < p
;
contradictionthen consider x being
R_eal such that A8:
(
s < x &
x < p &
x in REAL )
by MEASURE5:2;
( not
x in A & not
x in B )
by A1, A2, A8, XXREAL_1:1, XXREAL_1:2;
then A9:
not
x in A \/ B
by XBOOLE_0:def 3;
(
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) = inf B &
sup (A \/ B) = sup A )
by A5, A6, A7, XXREAL_0:2, XXREAL_0:def 9, XXREAL_0:def 10;
then
(
inf (A \/ B) < x &
x < sup (A \/ B) )
by A5, A6, A8, XXREAL_0:2;
hence
contradiction
by A9, A4, XXREAL_2:83;
verum end;
then A10:
q <= r
by A1, A2, A3, Th6;
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:1, XXREAL_1:2;
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, A5, A12, 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:167; verum