let I, J be Subset of REAL; :: thesis: ( I is 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 open_interval & J is left_open_interval & I meets J ) ; :: thesis: ex K, L being Interval st
( K misses L & I \ J = K \/ L )
then consider p, 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:28, XXREAL_1:26, XXREAL_1:276, XXREAL_1:91;
A7: r <> +infty by A1, A3, XXREAL_1:276, XXREAL_0:3;

per cases ( r = -infty or r in REAL ) by A7, XXREAL_0:14;

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

then A8: ( ].p,r.] = {} & ].p,r.[ = {} ) by XXREAL_0:5, XXREAL_1:26, XXREAL_1:28;
reconsider K = ].p,r.[, L = ].s,q.[ as Subset of REAL ;
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 ; :: 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:305, A8; :: thesis: verum

end;

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

then reconsider r1 = r as Real ;
reconsider K = ].p,r1.], L = ].s,q.[ as Subset of REAL ;
s is R_eal by XXREAL_0:def 1;
then ( K is left_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:305, XXREAL_1:91; :: thesis: verum

end;

end;