let I, J be Subset of REAL; ( I is right_open_interval & J is right_open_interval & I meets J implies ex K, L being Subset of REAL st
( K is right_open_interval & L is right_open_interval & K misses L & I \ J = K \/ L ) )
assume A1:
( I is right_open_interval & J is right_open_interval )
; ( not I meets J or ex K, L being Subset of REAL st
( K is right_open_interval & L is right_open_interval & 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 Real, s being R_eal such that
A3:
J = [.r,s.[
by A1;
assume A9:
I meets J
; ex K, L being Subset of REAL st
( K is right_open_interval & L is right_open_interval & K misses L & I \ J = K \/ L )
then A5:
I \ J = [.p,r.[ \/ [.s,q.[
by A2, A3, XXREAL_1:198;
A10:
( q > r & s > p )
by A2, A3, A9, XXREAL_1:96;
per cases
( s = +infty or ( s in REAL & r <= s ) or ( s in REAL & r > s ) )
by A7, XXREAL_0:14;
suppose C1:
(
s in REAL &
r > s )
;
ex K, L being Subset of REAL st
( K is right_open_interval & L is right_open_interval & K misses L & I \ J = K \/ L )C2:
(
min (
p,
s)
= p &
max (
r,
q)
= q )
by A2, A3, A9, XXREAL_1:96, XXREAL_0:def 9, XXREAL_0:def 10;
reconsider s1 =
s as
Real by C1;
s1 < q
by A2, A3, A9, XXREAL_1:96, C1, XXREAL_0:2;
then
(
s1 in [.p,r.[ &
s1 in [.s1,q.[ )
by A10, C1;
then C3:
[.p,r.[ meets [.s,q.[
by XBOOLE_0:def 4;
reconsider K =
[.p,q.[ as
Subset of
REAL ;
reconsider L =
{} as
Subset of
REAL by XBOOLE_1:2;
take
K
;
ex L being Subset of REAL st
( K is right_open_interval & L is right_open_interval & K misses L & I \ J = K \/ L )take
L
;
( K is right_open_interval & L is right_open_interval & K misses L & I \ J = K \/ L )thus
K is
right_open_interval
;
( L is right_open_interval & K misses L & I \ J = K \/ L )thus
L is
right_open_interval
by INTERVAL01;
( K misses L & I \ J = K \/ L )thus
K misses L
;
I \ J = K \/ Lthus
I \ J = K \/ L
by C3, C2, A5, XXREAL_1:162;
verum end; end;