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 holds
not A \/ B is Interval
let p, q, r, s be R_eal; ( A = [.p,q.] & B = [.r,s.] & A misses B implies not A \/ B is Interval )
assume that
A1:
A = [.p,q.]
and
A2:
B = [.r,s.]
and
A3:
A misses B
; A \/ B is not Interval
A4:
( p <= q & r <= s )
by A1, A2, XXREAL_1:29;
A5:
( inf A = p & sup A = q & inf B = r & sup B = s )
by A1, A2, XXREAL_1:29, MEASURE6:10, MEASURE6:14;
per cases
( q < r or s < p )
by A1, A2, A3, Th4;
suppose A6:
q < r
;
A \/ B is not Intervalthen consider x being
R_eal such that A7:
(
q < x &
x < r &
x in REAL )
by MEASURE5:2;
( not
x in A & not
x in B )
by A1, A2, A7, XXREAL_1:1;
then A8:
not
x in A \/ B
by XBOOLE_0:def 3;
A9:
(
inf A < x &
x < sup B )
by A7, A4, A5, XXREAL_0:2;
now A \/ B is not Intervalassume A10:
A \/ B is
Interval
;
contradiction
(
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 A6, A4, A5, XXREAL_0:2, XXREAL_0:def 9, XXREAL_0:def 10;
hence
contradiction
by A8, A9, A10, XXREAL_2:83;
verum end; hence
A \/ B is not
Interval
;
verum end; suppose A11:
s < p
;
A \/ B is not Intervalthen 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;
then A13:
not
x in A \/ B
by XBOOLE_0:def 3;
A14:
(
inf B < x &
x < sup A )
by A12, A4, A5, XXREAL_0:2;
now A \/ B is not Intervalassume A15:
A \/ B is
Interval
;
contradiction
(
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 A11, A4, A5, XXREAL_0:2, XXREAL_0:def 9, XXREAL_0:def 10;
hence
contradiction
by A13, A14, A15, XXREAL_2:83;
verum end; hence
A \/ B is not
Interval
;
verum end; end;