let I, J be Subset of REAL; ( I is open_interval & J is open_interval & I meets J implies ex K, L being Interval st
( K misses L & I \ J = K \/ L ) )
assume A1:
( I is open_interval & J is open_interval & I meets J )
; ex K, L being Interval st
( K misses L & I \ J = K \/ L )
then consider p, q being R_eal such that
A2:
I = ].p,q.[
;
consider r, s being R_eal such that
A3:
J = ].r,s.[
by A1;
( I <> {} & J <> {} )
by A1;
then A4:
( p < q & r < s & p < s & r < q )
by A1, A2, A3, XXREAL_1:28, XXREAL_1:275;
A7:
( r <> +infty & s <> -infty )
by A1, A3, XXREAL_1:275, XXREAL_0:3, XXREAL_0:5;
per cases
( ( r in REAL & s in REAL ) or ( r = -infty & s in REAL ) or ( r in REAL & s = +infty ) or ( r = -infty & s = +infty ) )
by A7, XXREAL_0:14;
suppose A8:
(
r = -infty &
s in REAL )
;
ex K, L being Interval st
( K misses L & I \ J = K \/ L )then A9:
(
].p,r.] = {} &
].p,r.[ = {} )
by XXREAL_0:5, XXREAL_1:26, XXREAL_1:28;
reconsider s1 =
s as
Real by A8;
reconsider K =
].p,r.[,
L =
[.s1,q.[ as
Subset of
REAL ;
(
K is
open_interval &
L is
right_open_interval )
;
then reconsider K =
K,
L =
L as
Interval ;
take
K
;
ex L being Interval st
( K misses L & I \ J = K \/ L )take
L
;
( K misses L & I \ J = K \/ L )thus
(
K misses L &
I \ J = K \/ L )
by A4, A2, A3, XXREAL_1:297, A9;
verum end; suppose A10:
(
r in REAL &
s = +infty )
;
ex K, L being Interval st
( K misses L & I \ J = K \/ L )then A11:
(
[.s,q.[ = {} &
].s,q.[ = {} )
by XXREAL_0:3, XXREAL_1:27, XXREAL_1:28;
reconsider r1 =
r as
Real by A10;
reconsider K =
].p,r1.],
L =
].s,q.[ as
Subset of
REAL ;
(
K is
left_open_interval &
L is
open_interval )
;
then reconsider K =
K,
L =
L as
Interval ;
take
K
;
ex L being Interval st
( K misses L & I \ J = K \/ L )take
L
;
( K misses L & I \ J = K \/ L )thus
(
K misses L &
I \ J = K \/ L )
by A4, A2, A3, XXREAL_1:297, A11;
verum end; suppose
(
r = -infty &
s = +infty )
;
ex K, L being Interval st
( K misses L & I \ J = K \/ L )then A12:
(
].p,r.] = {} &
].p,r.[ = {} &
[.s,q.[ = {} &
].s,q.[ = {} )
by XXREAL_0:5, XXREAL_0:3, XXREAL_1:26, XXREAL_1:27, XXREAL_1:28;
reconsider K =
].p,r.[,
L =
].s,q.[ as
Subset of
REAL ;
(
K is
open_interval &
L is
open_interval )
;
then reconsider K =
K,
L =
L as
Interval ;
take
K
;
ex L being Interval st
( K misses L & I \ J = K \/ L )take
L
;
( K misses L & I \ J = K \/ L )thus
(
K misses L &
I \ J = K \/ L )
by A4, A2, A3, XXREAL_1:297, A12;
verum end;