let I, J be Subset of REAL; :: thesis: ( I is closed_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 closed_interval & J is open_interval & I meets J ) ; :: thesis: ex K, L being Interval st
( K misses L & I \ J = K \/ L )
then consider p, q being Real 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 & r < q & p < s ) by A1, A2, A3, XXREAL_1:29, XXREAL_1:28, XXREAL_1:89, XXREAL_1:93;
A7: ( r <> +infty & s <> -infty ) by A1, A3, XXREAL_1:89, XXREAL_1:93, 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 ( r in REAL & s in REAL ) ; :: thesis: ex K, L being Interval st
( K misses L & I \ J = K \/ L )

then reconsider r1 = r, s1 = s as Real ;
reconsider K = [.p,r1.], L = [.s1,q.] as Subset of REAL ;
( K is closed_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:300, XXREAL_1:278; :: thesis: verum

end;

suppose A8: ( r = -infty & s in REAL ) ; :: thesis: ex K, L being Interval st
( K misses L & I \ J = K \/ L )

r < p by A8, XREAL_0:def 1, XXREAL_0:12;
then A9: ( [.p,r.] = {} & ].p,r.[ = {} ) by XXREAL_1:28, XXREAL_1:29;
reconsider s1 = s as Real by A8;
reconsider K = ].p,r.[, L = [.s1,q.] as Subset of REAL ;
p 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:300, A9; :: thesis: verum

end;

suppose A10: ( r in REAL & s = +infty ) ; :: thesis: ex K, L being Interval st
( K misses L & I \ J = K \/ L )

then q < s by XREAL_0:def 1, XXREAL_0:9;
then A11: ( [.s,q.] = {} & ].s,q.[ = {} ) by XXREAL_1:28, XXREAL_1:29;
reconsider r1 = r as Real by A10;
reconsider K = [.p,r1.], L = ].s,q.[ as Subset of REAL ;
q is R_eal by XXREAL_0:def 1;
then ( K is closed_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:300, A11; :: thesis: verum

end;

suppose A13: ( r = -infty & s = +infty ) ; :: thesis: ex K, L being Interval st
( K misses L & I \ J = K \/ L )

( r < p & q < s ) by A13, XREAL_0:def 1, XXREAL_0:9, XXREAL_0:12;
then A12: ( [.p,r.] = {} & ].p,r.[ = {} & [.s,q.] = {} & ].s,q.[ = {} ) by XXREAL_1:28, XXREAL_1:29;
reconsider K = ].p,r.[, L = ].s,q.[ as Subset of REAL ;
( p 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:300, A12; :: thesis: verum

end;

end;