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