let A, B be non empty Interval; ( A is open_interval & B is open_interval & A \/ B is Interval implies ( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) ) )
assume that
A1:
A is open_interval
and
A2:
B is open_interval
and
A3:
A \/ B is Interval
; ( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )
ex a1, a2 being R_eal st A = ].a1,a2.[
by A1, MEASURE5:def 2;
then A4:
A = ].(inf A),(sup A).[
by XXREAL_2:78;
ex b1, b2 being R_eal st B = ].b1,b2.[
by A2, MEASURE5:def 2;
then A5:
B = ].(inf B),(sup B).[
by XXREAL_2:78;
A6:
inf (A \/ B) = min ((inf A),(inf B))
by XXREAL_2:9;
A7:
sup (A \/ B) = max ((sup A),(sup B))
by XXREAL_2:10;
per cases
( inf A <= inf B or inf A > inf B )
;
suppose A8:
inf A <= inf B
;
( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )then A9:
inf (A \/ B) = inf A
by A6, XXREAL_0:def 9;
per cases
( sup A <= sup B or sup A > sup B )
;
suppose A10:
sup A <= sup B
;
( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )then A11:
A \/ B = ].(inf A),(sup B).[ \ [.(sup A),(inf B).]
by A4, A5, A8, XXREAL_1:309;
A12:
sup (A \/ B) = sup B
by A7, A10, XXREAL_0:def 10;
A13:
now not sup A <= inf Bassume
sup A <= inf B
;
contradictionthen
not
[.(sup A),(inf B).] is
empty
by XXREAL_1:30;
then consider x being
ExtReal such that A14:
x in [.(sup A),(inf B).]
by MEMBERED:8;
(
sup A <= x &
x <= inf B )
by A14, XXREAL_1:1;
then
(
inf A < x &
x < sup B )
by A4, A5, XXREAL_1:28, XXREAL_0:2;
then
x in A \/ B
by A3, A9, A12, XXREAL_2:83;
hence
contradiction
by A11, A14, XBOOLE_0:def 5;
verum end; then
[.(sup A),(inf B).] = {}
by XXREAL_1:29;
hence
A \/ B is
open_interval
by A11, MEASURE5:def 2;
( A meets B & ( inf A < sup B or inf B < sup A ) )
].(inf B),(sup A).[ <> {}
by A13, XXREAL_1:33;
then consider y being
ExtReal such that A15:
y in ].(inf B),(sup A).[
by MEMBERED:8;
(
inf B < y &
y < sup A )
by A15, XXREAL_1:4;
then
(
inf A < y &
y < sup A &
inf B < y &
y < sup B )
by A8, A10, XXREAL_0:2;
then
(
y in A &
y in B )
by A4, A5, XXREAL_1:4;
hence
A meets B
by XBOOLE_0:3;
( inf A < sup B or inf B < sup A )thus
(
inf A < sup B or
inf B < sup A )
by A13;
verum end; end; end; suppose A16:
inf A > inf B
;
( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )then A17:
inf (A \/ B) = inf B
by A6, XXREAL_0:def 9;
per cases
( sup A <= sup B or sup A > sup B )
;
suppose A18:
sup A > sup B
;
( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )then A19:
A \/ B = ].(inf B),(sup A).[ \ [.(sup B),(inf A).]
by A4, A5, A16, XXREAL_1:309;
A20:
sup (A \/ B) = sup A
by A7, A18, XXREAL_0:def 10;
A21:
now not sup B <= inf Aassume
sup B <= inf A
;
contradictionthen
not
[.(sup B),(inf A).] is
empty
by XXREAL_1:30;
then consider x being
ExtReal such that A22:
x in [.(sup B),(inf A).]
by MEMBERED:8;
(
sup B <= x &
x <= inf A )
by A22, XXREAL_1:1;
then
(
inf B < x &
x < sup A )
by A4, A5, XXREAL_1:28, XXREAL_0:2;
then
x in A \/ B
by A3, A17, A20, XXREAL_2:83;
hence
contradiction
by A19, A22, XBOOLE_0:def 5;
verum end; then
[.(sup B),(inf A).] = {}
by XXREAL_1:29;
hence
A \/ B is
open_interval
by A19, MEASURE5:def 2;
( A meets B & ( inf A < sup B or inf B < sup A ) )
].(inf A),(sup B).[ <> {}
by A21, XXREAL_1:33;
then consider y being
ExtReal such that A23:
y in ].(inf A),(sup B).[
by MEMBERED:8;
(
inf A < y &
y < sup B )
by A23, XXREAL_1:4;
then
(
inf B < y &
y < sup B &
inf A < y &
y < sup A )
by A16, A18, XXREAL_0:2;
then
(
y in A &
y in B )
by A4, A5, XXREAL_1:4;
hence
A meets B
by XBOOLE_0:3;
( inf A < sup B or inf B < sup A )thus
(
inf A < sup B or
inf B < sup A )
by A21;
verum end; end; end; end;