let I, J be Subset of REAL; ( I is 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 open_interval & J is right_open_interval & I meets J )
; 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 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:27, XXREAL_1:28, XXREAL_1:94, XXREAL_1:273;
A7:
s <> -infty
by A1, A3, XXREAL_1:273, XXREAL_0:5;
per cases
( s = +infty or s in REAL )
by A7, XXREAL_0:14;
suppose
s = +infty
;
ex K, L being Interval st
( K misses L & I \ J = K \/ L )then A8:
(
[.s,q.[ = {} &
].s,q.[ = {} )
by XXREAL_0:3, XXREAL_1:27, XXREAL_1:28;
reconsider K =
].p,r.[,
L =
].s,q.[ as
Subset of
REAL ;
r 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
;
ex L being Interval st
( K misses L & I \ J = K \/ L )take
L
;
( K misses L & I \ J = K \/ L )thus
(
K misses L &
I \ J = K \/ L )
by A4, A2, A3, XXREAL_1:301, A8;
verum end; end;