let I, J be Subset of REAL; ( I is right_open_interval & J is left_open_interval & I meets J implies ex K, L being Interval st
( K misses L & I \ J = K \/ L ) )
assume A1:
( I is right_open_interval & J is left_open_interval & I meets J )
; ex K, L being Interval st
( K misses L & I \ J = K \/ L )
then consider p being Real, q being R_eal such that
A2:
I = [.p,q.[
;
consider r being R_eal, s being Real such that
A3:
J = ].r,s.]
by A1;
( I <> {} & J <> {} )
by A1;
then A4:
( p <= q & r < s & q > r & s >= p )
by A1, A2, A3, XXREAL_1:27, XXREAL_1:26, XXREAL_1:274, XXREAL_1:279;
A7:
r <> +infty
by A1, A3, XXREAL_1:274, XXREAL_0:3;
per cases
( r = -infty or r in REAL )
by A7, XXREAL_0:14;
suppose B1:
r = -infty
;
ex K, L being Interval st
( K misses L & I \ J = K \/ L )
r < p
by B1, XREAL_0:def 1, XXREAL_0:12;
then A8:
(
[.p,r.] = {} &
].p,r.[ = {} )
by XXREAL_1:29, XXREAL_1:28;
reconsider K =
].p,r.[,
L =
].s,q.[ as
Subset of
REAL ;
(
p is
R_eal &
s is
R_eal )
by XXREAL_0:def 1;
then
(
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:306, A8;
verum end; end;