let I, J be Subset of REAL; :: thesis: ( 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 ) ; :: thesis: ( 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 ; :: thesis: 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;
A7: now :: thesis: not s = -infty
assume s = -infty ; :: thesis: contradiction
then s < r by XREAL_0:def 1, XXREAL_0:12;
then J = {} by A3, XXREAL_1:27;
hence contradiction by A9; :: thesis: verum
end;
per cases ( s = +infty or ( s in REAL & r <= s ) or ( s in REAL & r > s ) ) by A7, XXREAL_0:14;
suppose A8: s = +infty ; :: thesis: 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 )
reconsider K = [.p,r.[ as Subset of REAL ;
reconsider L = {} as Subset of REAL by XBOOLE_1:2;
take K ; :: thesis: 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 ; :: thesis: ( K is right_open_interval & L is right_open_interval & K misses L & I \ J = K \/ L )
( p in REAL & r in REAL ) by XREAL_0:def 1;
hence K is right_open_interval by NUMBERS:31; :: thesis: ( L is right_open_interval & K misses L & I \ J = K \/ L )
thus L is right_open_interval by INTERVAL01; :: thesis: ( K misses L & I \ J = K \/ L )
thus K misses L ; :: thesis: I \ J = K \/ L
thus I \ J = K \/ L by A8, A5, XXREAL_1:215; :: thesis: verum
end;
suppose B1: ( s in REAL & r <= s ) ; :: thesis: 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 reconsider s1 = s as Real ;
reconsider K = [.p,r.[ as Subset of REAL ;
reconsider L = [.s1,q.[ as Subset of REAL ;
take K ; :: thesis: 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 ; :: thesis: ( K is right_open_interval & L is right_open_interval & K misses L & I \ J = K \/ L )
r in REAL by XREAL_0:def 1;
hence ( K is right_open_interval & L is right_open_interval ) by NUMBERS:31; :: thesis: ( K misses L & I \ J = K \/ L )
thus K misses L by B1, XXREAL_1:96; :: thesis: I \ J = K \/ L
thus I \ J = K \/ L by A9, A2, A3, XXREAL_1:198; :: thesis: verum
end;
suppose C1: ( s in REAL & r > s ) ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( K is right_open_interval & L is right_open_interval & K misses L & I \ J = K \/ L )
thus K is right_open_interval ; :: thesis: ( L is right_open_interval & K misses L & I \ J = K \/ L )
thus L is right_open_interval by INTERVAL01; :: thesis: ( K misses L & I \ J = K \/ L )
thus K misses L ; :: thesis: I \ J = K \/ L
thus I \ J = K \/ L by C3, C2, A5, XXREAL_1:162; :: thesis: verum
end;
end;