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
( p = s & A \/ B = [.r,q.] )
let p, q, r, s be R_eal; ( A = [.p,q.] & B = [.r,s.[ & A misses B & A \/ B is Interval implies ( p = s & A \/ B = [.r,q.] ) )
assume that
A1:
A = [.p,q.]
and
A2:
B = [.r,s.[
and
A3:
A misses B
and
A4:
A \/ B is Interval
; ( p = s & A \/ B = [.r,q.] )
A5:
( p <= q & r < s )
by A1, A2, XXREAL_1:27, 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:11, MEASURE6:15;
now not q < rassume A7:
q < r
;
contradictionthen consider x being
R_eal such that A8:
(
q < x &
x < r &
x in REAL )
by MEASURE5:2;
( not
x in A & not
x in B )
by A1, A2, A8, XXREAL_1:1, XXREAL_1:3;
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 A &
sup (A \/ B) = sup B )
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:
s <= p
by A1, A2, A3, Th5;
now not s < passume A11:
s < p
;
contradictionthen consider x being
R_eal such that A12:
(
s < x &
x < p &
x in REAL )
by MEASURE5:2;
( not
x in A & not
x in B )
by A1, A2, A12, XXREAL_1:1, XXREAL_1:3;
then A13:
not
x in A \/ B
by XBOOLE_0:def 3;
(
min (
(inf A),
(inf B))
= inf B &
max (
(sup A),
(sup B))
= sup A )
by A11, A6, A5, XXREAL_0:2, XXREAL_0:def 9, XXREAL_0:def 10;
then
(
inf (A \/ B) = inf B &
sup (A \/ B) = sup A )
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
p = s
by A10, XXREAL_0:1; A \/ B = [.r,q.]
hence
A \/ B = [.r,q.]
by A1, A2, A5, XXREAL_1:166; verum